The 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

cd_ℓ G_K = 2

(cohomologicalDimensionAt_absoluteGaloisGroup_eq_two_of_isUnit), and in particular cd_ℓ G_K = 2 for every prime ℓ when K has characteristic zero, that is when K is a finite extension of some ℚ_p (cohomologicalDimensionAt_absoluteGaloisGroup_eq_two).

• cd_ℓ G_K ≤ 2. By the Sylow equality TauCeti.IsProPSylow.cohomologicalDimensionAt_eq, it suffices to bound a Sylow pro-ℓ subgroup P of G_K, and by the pro-ℓ test TauCeti.IsProP.cohomologicalDimensionAt_le_iff_subsingleton_cohomFp it suffices that H³(P, ℤ/ℓ) = 0. The group P acts trivially on μ_ℓ: its image under the cyclotomic character G_K → (ℤ/ℓ)ˣ is an ℓ-group in a group of order ℓ - 1 (TauCeti.smul_kummerCoeff_eq_self_of_isProP). So μ_ℓ is a trivial P-module of order ℓ, and H³(P, ℤ/ℓ) ≅ H³(P, μ_ℓ), which vanishes because P is closed (TauCeti.ClassFieldTheory.subsingleton_h3_kummerCoeff_of_isClosed).
• cd_ℓ G_K ≥ 2. The group H²(G_K, μ_ℓ) ≅ ℤ/ℓ is nonzero (TauCeti.ClassFieldTheory.nontrivial_h2_kummerCoeff), and μ_ℓ is ℓ-primary.

Both bounds are proved on Tau Ceti's Gal(Kˢ/K) and read on Mathlib's Field.absoluteGaloisGroup K through TauCeti.absoluteGaloisGroupRestrictEquiv and TauCeti.cohomologicalDimensionAt_congr.

Main results

• TauCeti.ClassFieldTheory.cohomologicalDimensionAt_absoluteGaloisGroup_le_two, TauCeti.ClassFieldTheory.two_le_cohomologicalDimensionAt_absoluteGaloisGroup: the two bounds on Gal(Kˢ/K).
• TauCeti.ClassFieldTheory.cohomologicalDimensionAt_absoluteGaloisGroup_eq_two_of_isUnit: cd_ℓ G_K = 2 for ℓ invertible in K.
• TauCeti.ClassFieldTheory.cohomologicalDimensionAt_absoluteGaloisGroup_eq_two: cd_ℓ G_K = 2 for a local field K of characteristic zero and every prime ℓ.

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)(i).

theorem TauCeti.ClassFieldTheory.cohomologicalDimensionAt_absoluteGaloisGroup_le_two {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : IsUnit ↑ℓ) : cohomologicalDimensionAt ℓ (AbsoluteGaloisGroup K) ≤ 2

cd_ℓ Gal(Kˢ/K) ≤ 2 for a prime ℓ invertible in K: a Sylow pro-ℓ subgroup P fixes μ_ℓ, so H³(P, ℤ/ℓ) ≅ H³(P, μ_ℓ) = 0.

theorem TauCeti.ClassFieldTheory.two_le_cohomologicalDimensionAt_absoluteGaloisGroup {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : IsUnit ↑ℓ) : 2 ≤ cohomologicalDimensionAt ℓ (AbsoluteGaloisGroup K)

cd_ℓ Gal(Kˢ/K) ≥ 2 for a prime ℓ invertible in K: H²(G_K, μ_ℓ) ≅ ℤ/ℓ is nonzero.

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

cd_ℓ G_K = 2 for a nonarchimedean local field K and a prime ℓ invertible in K.

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

cd_ℓ 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.1.8)(i); Serre, Galois Cohomology, II §5.3): every prime is invertible in K.