Mod-two classes in the cohomological Brauer group

Let K be a field in which 2 is invertible. The coefficient identification TauCeti.kummerCoeffIsoTrivialF2 transports the Kummer-sequence map

H²(G_K, μ₂) → H²(G_K, (Kˢ)ˣ)

to a map from cohomology with trivial 𝔽₂ coefficients. This file names that transported map as TauCeti.h2MuToUnits and records the two properties inherited from the Kummer sequence: it is injective, and its image is exactly the 2-torsion of the cohomology with multiplicative coefficients.

The comparison theorem TauCeti.kummerCoeffIsoTrivialF2_hom_comp_h2MuToUnits characterizes the transport: moving a μ₂-class to trivial 𝔽₂ coefficients and then applying TauCeti.h2MuToUnits is the original map TauCeti.h2KummerToUnits at n = 2.

Main definitions

• TauCeti.h2MuToUnits: the map from H²(G_K, 𝔽₂) to cohomology with multiplicative coefficients.

Main results

• TauCeti.h2MuToUnits_injective: the map is injective.
• TauCeti.h2MuToUnits_range: its image is the 2-torsion.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, (6.2.1) and the exact sequence following it.

noncomputable def TauCeti.h2MuToUnits (K : Type u) [Field K] [Invertible 2] : continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K)) ⟶ continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))

The map from H²(G_K, 𝔽₂) to cohomology with multiplicative coefficients. It is the Kummer-sequence map TauCeti.h2KummerToUnits at n = 2, precomposed with the inverse of the image of the coefficient identification TauCeti.kummerCoeffIsoTrivialF2 under the continuous-cohomology functor TauCeti.ContinuousCohomology.continuousCohomologyFunctor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.kummerCoeffIsoTrivialF2_hom_comp_h2MuToUnits (K : Type u) [Field K] [Invertible 2] : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.coeffMap (kummerCoeffIsoTrivialF2 K).hom 2) (h2MuToUnits K) = h2KummerToUnits K 2

Transporting a μ₂-class to trivial 𝔽₂ coefficients before applying TauCeti.h2MuToUnits recovers the Kummer-sequence map at n = 2. This equation characterizes the coefficient transport used in TauCeti.h2MuToUnits.

@[simp]

theorem TauCeti.kummerCoeffIsoTrivialF2_hom_comp_h2MuToUnits_assoc (K : Type u) [Field K] [Invertible 2] {Z : TopModuleCat ℤ} (h : continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.coeffMap (kummerCoeffIsoTrivialF2 K).hom 2) (CategoryTheory.CategoryStruct.comp (h2MuToUnits K) h) = CategoryTheory.CategoryStruct.comp (h2KummerToUnits K 2) h

Transporting a μ₂-class to trivial 𝔽₂ coefficients before applying TauCeti.h2MuToUnits recovers the Kummer-sequence map at n = 2. This equation characterizes the coefficient transport used in TauCeti.h2MuToUnits.

theorem TauCeti.h2MuToUnits_def (K : Type u) [Field K] [Invertible 2] : h2MuToUnits K = CategoryTheory.CategoryStruct.comp (ContinuousCohomology.coeffMap (kummerCoeffIsoTrivialF2 K).inv 2) (h2KummerToUnits K 2)

The defining equation of TauCeti.h2MuToUnits: the coefficient map of the inverse of the coefficient identification TauCeti.kummerCoeffIsoTrivialF2, followed by the Kummer-sequence map TauCeti.h2KummerToUnits at n = 2.

theorem TauCeti.h2MuToUnits_injective (K : Type u) [Field K] [Invertible 2] : Function.Injective ⇑(TopModuleCat.Hom.hom (h2MuToUnits K))

The map H²(G_K, 𝔽₂) → H²(G_K, (Kˢ)ˣ) is injective.

@[simp]

theorem TauCeti.h2MuToUnits_range (K : Type u) [Field K] [Invertible 2] (x : ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))).toModuleCat) : (∃ (y : ↑(continuousCohomology 2 (trivialF2 (AbsoluteGaloisGroup K))).toModuleCat), (TopModuleCat.Hom.hom (h2MuToUnits K)) y = x) ↔ x + x = 0

The image of H²(G_K, 𝔽₂) in H²(G_K, (Kˢ)ˣ) is the 2-torsion.