The cohomology class of an index-two character

An open subgroup U of index two in a topological group G determines a continuous character G → Multiplicative (ZMod 2), equal to one precisely on U. This file places that character in canonical continuous cohomology with trivial 𝔽₂ coefficients.

The definition is the class TauCeti.ContCohomology.homClass of the continuous character, which uses the explicit degree-one comparison: the multiplicative character is first viewed as a continuous additive 1-cocycle by TauCeti.ContCohomology.evensHomCocycle, then its explicit class is transported to Mathlib's canonical continuous cohomology object. This is the character class that appears in the index-two exact sequence and in the norm-of-restriction identity for the Evens norm.

Main definition

• OpenSubgroup.indexTwoCharacterClass: the class in H¹(G, 𝔽₂) of the character whose kernel is U.

Reference

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I, §§5–6, for the index-two character in restriction–corestriction sequences.

theorem OpenSubgroup.continuousSMul_trivialF2_character {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ContinuousSMul G ↑(TauCeti.trivialF2 G)

noncomputable def OpenSubgroup.indexTwoCharacterClass {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (hU : (↑U).index = 2) : ↑(continuousCohomology 1 (TauCeti.trivialF2 G)).toModuleCat

The class of the character of an index-two open subgroup. It is the class TauCeti.ContCohomology.homClass of the continuous character Subgroup.indexTwoCharacter, whose kernel is the subgroup.

Equations

• U.indexTwoCharacterClass hU = TauCeti.ContCohomology.homClass G ((↑U).indexTwoCharacter hU) ⋯

theorem OpenSubgroup.indexTwoCharacterClass_def {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenSubgroup G) (hU : (↑U).index = 2) : U.indexTwoCharacterClass hU = (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((TauCeti.ContCohomology.explicitH1AddEquivContinuousCohomology G ↑(TauCeti.trivialF2 G)) ↑(TauCeti.ContCohomology.evensHomCocycle ((↑U).indexTwoCharacter hU) ⋯))

The index-two character class is obtained from the explicit class of the continuous character by the degree-one comparison and the canonical identification of trivial coefficients.

theorem OpenSubgroup.indexTwoCharacterClass_congr {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U V : OpenSubgroup G} (hUV : U = V) (hU : (↑U).index = 2) (hV : (↑V).index = 2) : U.indexTwoCharacterClass hU = V.indexTwoCharacterClass hV

The index-two character class depends only on the open subgroup, not on the proof that its index is two.