The index-two cup--restriction exact sequence

For an open subgroup U of index two in a profinite group G, let χ_U be the associated class in H¹(G, 𝔽₂). This file identifies the degree-one connecting map of the coinduced coefficient sequence with cup product by χ_U. The long exact sequence then gives

H¹(G, 𝔽₂) --χ_U ⌣ -→ H²(G, 𝔽₂) --res→ H²(U, 𝔽₂).

Main results

• OpenSubgroup.indexTwoDelta0_one: the degree-zero connecting morphism sends 1 to the subgroup character.
• OpenSubgroup.indexTwoDelta1_eq_cup_character: the degree-one connecting morphism is cup product by the subgroup character.
• OpenSubgroup.exact_cup_res2_of_index_two: the displayed sequence is exact.

References

• J. Kr. Arason, Cohomologische Invarianten quadratischer Formen, J. Algebra 36 (1975), 448--491.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.6.5).

theorem OpenSubgroup.indexTwoDelta0_one {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) : (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((TopModuleCat.Hom.hom ((TauCeti.DiscreteCoind.indexTwoShortExact G (↑U) (↑(TauCeti.trivialF2 G)) hU ⋯ ⋯).delta 0)) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) (TauCeti.cohomF2.one G))) = U.indexTwoCharacterClass hU

The degree-zero connecting map of the index-two coinduced sequence sends 1 to the subgroup character. The unit class of H⁰(G, 𝔽₂) is sent to χ_U ∈ H¹(G, 𝔽₂); the transports identify the discrete coefficient module with trivialF2 G.

theorem OpenSubgroup.indexTwoDelta1_eq_cup_character {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) (x : ↑(continuousCohomology 1 (TauCeti.ofDiscreteModule ℤ G ↑(TauCeti.trivialF2 G))).toModuleCat) : (TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) ((TopModuleCat.Hom.hom ((TauCeti.DiscreteCoind.indexTwoShortExact G (↑U) (↑(TauCeti.trivialF2 G)) hU ⋯ ⋯).delta 1)) x) = (((TauCeti.trivialF2TopPairing G).cup 1 1) (U.indexTwoCharacterClass hU)) ((TopModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) x)

The connecting map of the index-two coinduced sequence is cup product by the subgroup character. This is the canonical continuous-cohomology form of the explicit cochain identity. The transports identify the discrete coefficient module with trivialF2 G.

theorem OpenSubgroup.exact_cup_res2_of_index_two {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (U : OpenSubgroup G) (hU : (↑U).index = 2) : Function.Exact ⇑(((TauCeti.trivialF2TopPairing G).cup 1 1) (U.indexTwoCharacterClass hU)) ⇑(CategoryTheory.ConcreteCategory.hom (TauCeti.trivialF2ResMap G (↑U) 2))

The index-two cup--restriction sequence is exact in degree two. A class in H²(G, 𝔽₂) restricts to zero on an open subgroup U of index two exactly when it is the cup product of the character class χ_U with a class in H¹(G, 𝔽₂).