H²(G_K, μₙ) is the n-torsion of the cohomological Brauer group

Let K be a field, Kˢ a separable closure, G_K = AbsoluteGaloisGroup K, and n a natural number invertible in K. The inclusion μₙ ⊆ (Kˢ)ˣ induces

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

and this map is injective with image the n-torsion of H²(G_K, (Kˢ)ˣ). Both facts are read off the long exact sequence of the Kummer sequence 1 → μₙ → (Kˢ)ˣ → (Kˢ)ˣ → 1 (TauCeti.kummerShortExact):

H¹(G_K, (Kˢ)ˣ) →δ¹→ H²(G_K, μₙ) → H²(G_K, (Kˢ)ˣ) →n→ H²(G_K, (Kˢ)ˣ).

• Injectivity is exactness at H²(G_K, μₙ) together with Hilbert 90, H¹(G_K, (Kˢ)ˣ) = 0 (TauCeti.subsingleton_H1_unitsCoeff).
• The image is exactness at H²(G_K, (Kˢ)ˣ), once the map induced by the n-th power map of (Kˢ)ˣ is recognised as multiplication by n on H² (TauCeti.explicitCoeff2_kummerShortExact_proj).

The argument runs in the explicit low-degree model, where the long exact sequence lives, and the result is transported to Mathlib's continuousCohomology 2 through the comparison TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology and its naturality in coefficient maps, TauCeti.ContCohomology.explicitH2AddEquivContinuousCohomology_coeffMap.

This is how the n-torsion subgroup of the Brauer group is seen cohomologically: for a local field the local invariant identifies the n-torsion of H²(G_K, (Kˢ)ˣ) with (1/n)ℤ/ℤ, and composing with the injection here gives H²(G_K, μₙ) ≃ ℤ/n.

Main definitions

• TauCeti.kummerCoeffToUnits: the inclusion μₙ ⊆ (Kˢ)ˣ as a morphism of canonical coefficient objects.
• TauCeti.h2KummerToUnits: the induced map H²(G_K, μₙ) → H²(G_K, (Kˢ)ˣ) on Mathlib's continuous cohomology.

Main results

• TauCeti.explicitCoeff2_kummerShortExact_incl_injective and TauCeti.mem_range_explicitCoeff2_kummerShortExact_incl_iff: injectivity and the image, on the explicit model.
• TauCeti.explicitCoeff2_kummerShortExact_restrict_incl_injective and TauCeti.mem_range_explicitCoeff2_kummerShortExact_restrict_incl_iff: the corresponding statements for subgroups; injectivity requires the subgroup to be closed.
• TauCeti.explicitCor2_kummerCoeff_bijective_of_unitsCoeff_bijective: bijectivity of corestriction on roots-of-unity coefficients, assuming bijectivity on units coefficients.
• TauCeti.h2KummerToUnits_injective: H²(G_K, μₙ) → H²(G_K, (Kˢ)ˣ) is injective.
• TauCeti.h2KummerToUnits_range: its image is the n-torsion.

References

• J.-P. Serre, Galois Cohomology, Chapter II, §5.2, Theorem 2 and its proof.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (6.2.1) and the exact sequence following it.

The explicit model

@[simp]

theorem TauCeti.explicitCoeff2_kummerShortExact_proj (K : Type u) [Field K] {n : ℕ} (hn : IsUnit ↑n) (x : ContCohomology.H2 (AbsoluteGaloisGroup K) (UnitsCoeff K)) : (ContCohomology.explicitCoeff2 (AbsoluteGaloisGroup K) (UnitsCoeff K) (kummerShortExact K n hn).projDistribMulActionHom ⋯) x = n • x

The map on explicit H² induced by the n-th power map of (Kˢ)ˣ is multiplication by n: in additive notation the power map is n • ·, and a coefficient map acts on cocycles by postcomposition.

theorem TauCeti.explicitCoeff2_kummerShortExact_incl_injective (K : Type u) [Field K] {n : ℕ} (hn : IsUnit ↑n) : Function.Injective ⇑(ContCohomology.explicitCoeff2 (AbsoluteGaloisGroup K) (KummerCoeff K n) (kummerShortExact K n hn).inclDistribMulActionHom ⋯)

H²(G_K, μₙ) → H²(G_K, (Kˢ)ˣ) is injective, on the explicit model.

theorem TauCeti.mem_range_explicitCoeff2_kummerShortExact_incl_iff (K : Type u) [Field K] {n : ℕ} (hn : IsUnit ↑n) (x : ContCohomology.H2 (AbsoluteGaloisGroup K) (UnitsCoeff K)) : x ∈ (ContCohomology.explicitCoeff2 (AbsoluteGaloisGroup K) (KummerCoeff K n) (kummerShortExact K n hn).inclDistribMulActionHom ⋯).range ↔ n • x = 0

The image of H²(G_K, μₙ) in H²(G_K, (Kˢ)ˣ) is the n-torsion, on the explicit model.

Subgroups

theorem TauCeti.explicitCoeff2_kummerShortExact_restrict_incl_injective (K : Type u) [Field K] {n : ℕ} (hn : IsUnit ↑n) (U : Subgroup (AbsoluteGaloisGroup K)) (hU : IsClosed ↑U) : Function.Injective ⇑(ContCohomology.explicitCoeff2 (↥U) (KummerCoeff K n) ((kummerShortExact K n hn).restrict U).inclDistribMulActionHom ⋯)

The Kummer coefficient inclusion is injective on H² of every closed subgroup of G_K.

theorem TauCeti.mem_range_explicitCoeff2_kummerShortExact_restrict_incl_iff (K : Type u) [Field K] {n : ℕ} (hn : IsUnit ↑n) (U : Subgroup (AbsoluteGaloisGroup K)) (x : ContCohomology.H2 (↥U) (UnitsCoeff K)) : x ∈ (ContCohomology.explicitCoeff2 (↥U) (KummerCoeff K n) ((kummerShortExact K n hn).restrict U).inclDistribMulActionHom ⋯).range ↔ n • x = 0

The image of the Kummer coefficient inclusion on H² of any subgroup of G_K is precisely its n-torsion. Unlike injectivity, this image statement does not require closedness.

theorem TauCeti.explicitCor2_kummerCoeff_bijective_of_unitsCoeff_bijective (K : Type u) [Field K] {n : ℕ} (hn : IsUnit ↑n) (U : Subgroup (AbsoluteGaloisGroup K)) [U.FiniteIndex] (hU : IsOpen ↑U) (hc : Function.Bijective ⇑(ContCohomology.explicitCor2 (AbsoluteGaloisGroup K) (UnitsCoeff K) U hU)) : Function.Bijective ⇑(ContCohomology.explicitCor2 (AbsoluteGaloisGroup K) (KummerCoeff K n) U hU)

If corestriction on H² with units coefficients is bijective, so is corestriction with roots-of-unity coefficients, for every exponent invertible in the field.

The canonical object

noncomputable def TauCeti.kummerCoeffToUnits (K : Type u) [Field K] (n : ℕ) : ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (KummerCoeff K n) ⟶ ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K)

The inclusion μₙ ⊆ (Kˢ)ˣ as a morphism of canonical coefficient objects over G_K.

Equations

• TauCeti.kummerCoeffToUnits K n = TauCeti.ofDiscreteModuleMap (TauCeti.kummerCoeffIncl K n).toIntLinearMap ⋯

@[simp]

theorem TauCeti.kummerCoeffToUnits_hom_apply (K : Type u) [Field K] (n : ℕ) (x : KummerCoeff K n) : (TopRep.Hom.hom (kummerCoeffToUnits K n)) x = (kummerCoeffIncl K n) x

The morphism kummerCoeffToUnits is the inclusion μₙ ⊆ (Kˢ)ˣ on elements.

noncomputable def TauCeti.h2KummerToUnits (K : Type u) [Field K] (n : ℕ) : continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (KummerCoeff K n)) ⟶ continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))

The map H²(G_K, μₙ) → H²(G_K, (Kˢ)ˣ) induced by the inclusion μₙ ⊆ (Kˢ)ˣ, on Mathlib's continuous cohomology. It is how the n-torsion subgroup of H² sits inside the cohomological Brauer group: injective (TauCeti.h2KummerToUnits_injective) with image the n-torsion (TauCeti.h2KummerToUnits_range) when n is invertible in K.

Equations

• TauCeti.h2KummerToUnits K n = TauCeti.ContinuousCohomology.coeffMap (TauCeti.kummerCoeffToUnits K n) 2

theorem TauCeti.h2KummerToUnits_def (K : Type u) [Field K] (n : ℕ) : h2KummerToUnits K n = ContinuousCohomology.coeffMap (kummerCoeffToUnits K n) 2

The defining equation of h2KummerToUnits: it is the coefficient map of the inclusion kummerCoeffToUnits K n.

theorem TauCeti.h2KummerToUnits_explicitH2AddEquivContinuousCohomology {K : Type u} [Field K] {n : ℕ} (hn : IsUnit ↑n) (x : ContCohomology.H2 (AbsoluteGaloisGroup K) (KummerCoeff K n)) : (TopModuleCat.Hom.hom (h2KummerToUnits K n)) ((ContCohomology.explicitH2AddEquivContinuousCohomology (AbsoluteGaloisGroup K) (KummerCoeff K n)) x) = (ContCohomology.explicitH2AddEquivContinuousCohomology (AbsoluteGaloisGroup K) (UnitsCoeff K)) ((ContCohomology.explicitCoeff2 (AbsoluteGaloisGroup K) (KummerCoeff K n) (kummerShortExact K n hn).inclDistribMulActionHom ⋯) x)

The comparison with the explicit model carries the explicit coefficient map of μₙ ⊆ (Kˢ)ˣ to h2KummerToUnits.

theorem TauCeti.h2KummerToUnits_injective {K : Type u} [Field K] {n : ℕ} (hn : IsUnit ↑n) : Function.Injective ⇑(TopModuleCat.Hom.hom (h2KummerToUnits K n))

H²(G_K, μₙ) → H²(G_K, (Kˢ)ˣ) is injective for n invertible in K.

theorem TauCeti.h2KummerToUnits_range {K : Type u} [Field K] {n : ℕ} (hn : IsUnit ↑n) (x : ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (UnitsCoeff K))).toModuleCat) : (∃ (y : ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (KummerCoeff K n))).toModuleCat), (TopModuleCat.Hom.hom (h2KummerToUnits K n)) y = x) ↔ n • x = 0

The image of H²(G_K, μₙ) in H²(G_K, (Kˢ)ˣ) is the n-torsion for n invertible in K.