The third cohomology of the roots of unity of a local field

Let K be a nonarchimedean local field with separable closure Kˢ and G_K = Gal(Kˢ/K), and let n be invertible in K. This file proves that

H³(V, μₙ) = 0

for every closed subgroup V of G_K (subsingleton_h3_kummerCoeff_of_isClosed). Applied to a Sylow pro-ℓ subgroup, for a prime ℓ invertible in K, it is the input of the bound cd_ℓ G_K ≤ 2.

For an open subgroup V, with fixed field E a finite extension of K, the Kummer sequence 1 → μₙ → (Kˢ)ˣ → (Kˢ)ˣ → 1 restricted to V gives the exact sequence

H²(V, (Kˢ)ˣ) --n--> H²(V, (Kˢ)ˣ) --δ--> H³(V, μₙ) → H³(V, (Kˢ)ˣ).

The last group is H³(G_E, (Eˢ)ˣ) = 0 (TauCeti.ClassFieldTheory.subsingleton_h3_unitsRep for E, read on V through G_E ≃ₜ* V), and the first map is onto because H²(V, (Kˢ)ˣ) is isomorphic to ℚ/ℤ by the local invariant of V (TauCeti.ClassFieldTheory.subgroupInvMap), which is divisible. Hence H³(V, μₙ) = 0 (subsingleton_h3_kummerCoeff_of_isOpen). For a closed subgroup, every class of H³(V, μₙ) is restricted from an open subgroup containing V (TauCeti.ContinuousCohomology.exists_openSubgroup_le_resLE_eq).

In degree two, by contrast, H²(G_K, μₙ) ≅ ℤ/n by the local invariant (TauCeti.ClassFieldTheory.h2MuEquivZMod), so it is nonzero for n > 1 (nontrivial_h2_kummerCoeff), which is the input of the bound cd_ℓ G_K ≥ 2.

Main results

• TauCeti.ClassFieldTheory.subsingleton_h3_unitsCoeff_of_isOpen: H³(V, (Kˢ)ˣ) = 0 for an open subgroup V of G_K.
• TauCeti.ClassFieldTheory.surjective_coeffMap_unitsCoeffPow_two: the n-th power map is onto on H²(V, (Kˢ)ˣ).
• TauCeti.ClassFieldTheory.nontrivial_h2_kummerCoeff: H²(G_K, μₙ) ≠ 0 for n > 1.
• TauCeti.ClassFieldTheory.subsingleton_h3_kummerCoeff_of_isOpen, TauCeti.ClassFieldTheory.subsingleton_h3_kummerCoeff_of_isClosed: H³(V, μₙ) = 0 for an open, respectively closed, subgroup V of G_K.

References

• J.-P. Serre, Galois Cohomology, Ch. II, §5.3, Prop. 12.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (7.1.8).

theorem TauCeti.ClassFieldTheory.instLocallyCompactSpaceAbsoluteGaloisGroup_1 (K : Type) [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, as in TauCeti.Algebra.CrossedProduct.CupProduct.

theorem TauCeti.ClassFieldTheory.subsingleton_h3_unitsCoeff_of_isOpen (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (V : Subgroup (AbsoluteGaloisGroup K)) (hV : IsOpen ↑V) : Subsingleton ↑(continuousCohomology 3 (ofDiscreteModule ℤ (↥V) (UnitsCoeff K))).toModuleCat

H³(V, (Kˢ)ˣ) = 0 for an open subgroup V of G_K. The subgroup is the absolute Galois group of its fixed field E, a finite extension of K and hence a nonarchimedean local field, and H³(G_E, (Eˢ)ˣ) = 0.

theorem TauCeti.ClassFieldTheory.surjective_coeffMap_unitsCoeffPow_two {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (V : Subgroup (AbsoluteGaloisGroup K)) (hV : IsOpen ↑V) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap ((kummerShortExact K n hn).restrict V).proj.toIntLinearMap ⋯) 2))

The n-th power map is onto on H²(V, (Kˢ)ˣ) for an open subgroup V of G_K: the local invariant of V identifies H²(V, (Kˢ)ˣ) with the divisible group ℚ/ℤ, and the map is multiplication by n.

theorem TauCeti.ClassFieldTheory.subsingleton_h3_kummerCoeff_of_isOpen {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (V : Subgroup (AbsoluteGaloisGroup K)) (hV : IsOpen ↑V) : Subsingleton ↑(continuousCohomology 3 (ofDiscreteModule ℤ (↥V) (KummerCoeff K n))).toModuleCat

H³(V, μₙ) = 0 for an open subgroup V of G_K, for n invertible in K: by the Kummer sequence, H³(V, μₙ) sits between the cokernel of n on H²(V, (Kˢ)ˣ), which vanishes, and H³(V, (Kˢ)ˣ) = 0.

theorem TauCeti.ClassFieldTheory.subsingleton_h3_kummerCoeff_of_isClosed {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (V : Subgroup (AbsoluteGaloisGroup K)) (hV : IsClosed ↑V) : Subsingleton ↑(continuousCohomology 3 (ofDiscreteModule ℤ (↥V) (KummerCoeff K n))).toModuleCat

H³(V, μₙ) = 0 for a closed subgroup V of G_K, for n invertible in K: every class of H³(V, μₙ) is restricted from an open subgroup containing V, where H³ vanishes.

theorem TauCeti.ClassFieldTheory.nontrivial_h2_kummerCoeff {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) (h1 : 1 < n) : Nontrivial ↑(continuousCohomology 2 (ofDiscreteModule ℤ (AbsoluteGaloisGroup K) (KummerCoeff K n))).toModuleCat

H²(G_K, μₙ) is nonzero for 1 < n invertible in K: the local invariant identifies it with ℤ/n (h2MuEquivZMod).