The strict cohomological dimension of the absolute Galois group of a local field

For a nonarchimedean local field K and a prime ℓ invertible in K, this file proves

scd_ℓ G_K = 2

(strictCohomologicalDimensionAt_absoluteGaloisGroup_eq_two_of_isUnit), and in particular scd_ℓ G_K = 2 for every prime ℓ when K has characteristic zero (strictCohomologicalDimensionAt_absoluteGaloisGroup_eq_two).

The lower bound is cd_ℓ G_K ≤ scd_ℓ G_K with cd_ℓ G_K = 2. For the upper bound, the criterion TauCeti.strictCohomologicalDimensionAt_le_iff_forall_openSubgroup (NSW (3.3.4)) asks, besides cd_ℓ G_K ≤ 2, that the ℓ-primary component of H³(U, ℤ) vanish for every open subgroup U of G_K (primaryComponent_h3_int_eq_bot_of_isOpen). The subgroup U is the absolute Galois group of a finite extension E of K, again a local field, and:

• H²(G_E, ℤ/n) is killed by the exponent of μₙ(E) (nsmul_H2_zmod_eq_zero). By local Tate duality, H²(G_E, ℤ/n) embeds into the dual of H⁰(G_E, Hom(ℤ/n, μₙ)) = Hom(ℤ/n, μₙ(E)) (TauCeti.ClassFieldTheory.dualityMap2_kummerCoeff_bijective). Since the ℓ-power roots of unity of E form a finite group of some order ℓᵐ (TauCeti.finite_pPowerRootsOfUnity), ℓᵐ kills H²(G_E, ℤ/ℓᵏ) for every k.
• H³(U, ℤ/ℓᵐ) = 0, because cd_ℓ U ≤ cd_ℓ G_K = 2.

These two facts give the vanishing of the ℓ-primary part of H³(U, ℤ) through the integral Bockstein sequences 0 → ℤ → ℤ → ℤ/ℓᵏ → 0 (TauCeti.primaryComponent_continuousCohomology_int_eq_bot). This is the argument of NSW, which identifies H³(U, ℤ)(ℓ) with H²(U, ℚ_ℓ/ℤ_ℓ), the dual of the inverse limit of the μ_{ℓᵏ}(E) under ℓ-th powers, which vanishes because μ_{ℓ^∞}(E) is finite.

Main results

• TauCeti.ClassFieldTheory.nsmul_H2_zmod_eq_zero: e • H²(G_K, ℤ/n) = 0 whenever e kills μₙ(K), for n invertible in K.
• TauCeti.ClassFieldTheory.primaryComponent_h3_int_eq_bot_of_isOpen: the ℓ-primary component of H³(U, ℤ) vanishes for every open subgroup U of G_K.
• TauCeti.ClassFieldTheory.strictCohomologicalDimensionAt_absoluteGaloisGroup_eq_two_of_isUnit: scd_ℓ G_K = 2 for ℓ invertible in K.
• TauCeti.ClassFieldTheory.strictCohomologicalDimensionAt_absoluteGaloisGroup_eq_two: scd_ℓ G_K = 2 for a local field K of characteristic zero and every prime ℓ.
• TauCeti.ClassFieldTheory.strictCohomologicalDimensionAt_galSeparableClosure_eq_two: the same on AbsoluteGaloisGroup K = Gal(Kˢ/K).

References

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

H² with trivial cyclic coefficients

theorem TauCeti.ClassFieldTheory.nsmul_H2_zmod_eq_zero {K : Type} [Field K] {n e : ℕ} [DistribMulAction (AbsoluteGaloisGroup K) (ZMod n)] (htriv : ∀ (g : AbsoluteGaloisGroup K) (m : ZMod n), g • m = m) [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [ContinuousSMul (AbsoluteGaloisGroup K) (ZMod n)] (hn : IsUnit ↑n) (he : ∀ (ζ : Kˣ), ζ ^ n = 1 → ζ ^ e = 1) (y : ContCohomology.H2 (AbsoluteGaloisGroup K) (ZMod n)) : e • y = 0

H²(G_K, ℤ/n) is killed by the exponent of μₙ(K). For n invertible in the local field K and G_K acting trivially on ℤ/n, if e kills every nth root of unity of K, then e kills H²(G_K, ℤ/n).

Open subgroups

theorem TauCeti.ClassFieldTheory.primaryComponent_h3_int_eq_bot_of_isOpen {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : IsUnit ↑ℓ) (U : Subgroup (Field.absoluteGaloisGroup K)) (hU : IsOpen ↑U) : AddCommGroup.primaryComponent (↑(continuousCohomology 3 (TopRep.of (ContRepresentation.trivial ℤ (↥U) (ULift.{0, 0} ℤ)))).toModuleCat) ℓ = ⊥

The ℓ-primary part of H³(U, ℤ) vanishes for every open subgroup U of G_K, the integers carrying the trivial action, for a prime ℓ invertible in the local field K.

The strict cohomological dimension

theorem TauCeti.ClassFieldTheory.strictCohomologicalDimensionAt_absoluteGaloisGroup_eq_two_of_isUnit {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : IsUnit ↑ℓ) : strictCohomologicalDimensionAt ℓ (Field.absoluteGaloisGroup K) = 2

scd_ℓ G_K = 2 for a nonarchimedean local field K and a prime ℓ invertible in K (NSW (7.2.5)).

theorem TauCeti.ClassFieldTheory.strictCohomologicalDimensionAt_absoluteGaloisGroup_eq_two {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : strictCohomologicalDimensionAt ℓ (Field.absoluteGaloisGroup K) = 2

scd_ℓ G_K = 2 for every prime ℓ and every nonarchimedean local field K of characteristic zero, that is every finite extension of some ℚ_p (NSW (7.2.5)): every prime is invertible in K.

theorem TauCeti.ClassFieldTheory.strictCohomologicalDimensionAt_galSeparableClosure_eq_two {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : strictCohomologicalDimensionAt ℓ (AbsoluteGaloisGroup K) = 2

scd_ℓ Gal(Kˢ/K) = 2 for every prime ℓ and every nonarchimedean local field K of characteristic zero: strictCohomologicalDimensionAt_absoluteGaloisGroup_eq_two, read on AbsoluteGaloisGroup K = Gal(Kˢ/K) through the restriction isomorphism absoluteGaloisGroupRestrictEquiv.