Roots-of-unity cohomology inside the Brauer group

For a field F, this file transports the Kummer-sequence coefficient map

H²(Gal(Fˢ/F), μₙ) → H²(Gal(Fˢ/F), (Fˢ)ˣ)

to the coefficient objects for Field.absoluteGaloisGroup F used in local class field theory. The result is a map h2MuToBr from H²(G_F, muNRep n F) to the cohomological Brauer group Br F. When n is invertible in F, it is injective and its image is exactly the n-torsion of Br F.

Thus a local invariant Br F ≃+ ℚ/ℤ restricts along h2MuToBr to an identification of H²(G_F, μₙ) with the n-torsion of ℚ/ℤ, and hence with ZMod n.

Main definitions

• TauCeti.ClassFieldTheory.h2MuToBr: the Kummer coefficient map from roots-of-unity cohomology to Br F.

Main results

• TauCeti.ClassFieldTheory.h2MuToBr_injective: the map is injective when n is invertible in F.
• TauCeti.ClassFieldTheory.h2MuToBr_range: its image is then the n-torsion of Br F.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.2.1).

theorem TauCeti.ClassFieldTheory.instLocallyCompactSpaceAbsoluteGaloisGroup {K : Type u} [Field K] : LocallyCompactSpace (AbsoluteGaloisGroup K)

The absolute Galois group is locally compact, being compact and Hausdorff. Instance search does not find this within its default budget under the imports of this file, so it is assembled here from the Krull topology being Hausdorff.

noncomputable def TauCeti.ClassFieldTheory.h2MuToBr (n : ℕ) (F : Type u) [Field F] : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat →+ Br F

The Kummer coefficient map H²(G_F, μₙ) → Br F. It is the Kummer-sequence coefficient map on the separable-closure model, transported to muNRep n F and unitsRep F. It is injective when n is invertible in F (h2MuToBr_injective).

theorem TauCeti.ClassFieldTheory.h2MuToBr_apply (n : ℕ) (F : Type u) [Field F] (y : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat) : (h2MuToBr n F) y = (unitsRepH2Equiv F) ((ContCohomology.explicitH2AddEquivContinuousCohomology (AbsoluteGaloisGroup F) (UnitsCoeff F)).symm ((TopModuleCat.Hom.hom (h2KummerToUnits F n)) ((ContCohomology.explicitH2AddEquivContinuousCohomology (AbsoluteGaloisGroup F) (KummerCoeff F n)) ((muNRepH2Equiv n F).symm y))))

h2MuToBr is the inverse coefficient transport to the separable-closure model, followed by the Kummer-sequence map and the coefficient transport to Br F.

theorem TauCeti.ClassFieldTheory.h2MuToBr_muNRepH2Equiv (n : ℕ) (F : Type u) [Field F] (x : ContCohomology.H2 (AbsoluteGaloisGroup F) (KummerCoeff F n)) : (h2MuToBr n F) ((muNRepH2Equiv n F) x) = (unitsRepH2Equiv F) ((ContCohomology.explicitH2AddEquivContinuousCohomology (AbsoluteGaloisGroup F) (UnitsCoeff F)).symm ((TopModuleCat.Hom.hom (h2KummerToUnits F n)) ((ContCohomology.explicitH2AddEquivContinuousCohomology (AbsoluteGaloisGroup F) (KummerCoeff F n)) x)))

On a class in the separable-closure model, h2MuToBr is the Kummer-sequence map followed by the coefficient transport to Br F.

theorem TauCeti.ClassFieldTheory.h2MuToBr_muNRepH2Equiv_eq_explicitCoeff2 (n : ℕ) (F : Type u) [Field F] (x : ContCohomology.H2 (AbsoluteGaloisGroup F) (KummerCoeff F n)) : (h2MuToBr n F) ((muNRepH2Equiv n F) x) = (unitsRepH2Equiv F) ((ContCohomology.explicitCoeff2 (AbsoluteGaloisGroup F) (KummerCoeff F n) (kummerCoeffInclHom F n) ⋯) x)

On the explicit model, the Kummer-to-Brauer map is induced by the coefficient inclusion.

theorem TauCeti.ClassFieldTheory.h2MuToBr_injective (n : ℕ) (F : Type u) [Field F] (hn : IsUnit ↑n) : Function.Injective ⇑(h2MuToBr n F)

The map from roots-of-unity cohomology into the Brauer group is injective when n is invertible in F.

theorem TauCeti.ClassFieldTheory.h2MuToBr_range (n : ℕ) (F : Type u) [Field F] (hn : IsUnit ↑n) (x : Br F) : (∃ (y : ↑(continuousCohomology 2 (muNRep n F)).toModuleCat), (h2MuToBr n F) y = x) ↔ n • x = 0

The image of H²(G_F, μₙ) in Br F is the n-torsion, when n is invertible in F.