Local maximal pro-p Galois groups without μ_p are free

Let K be a nonarchimedean local field not containing a primitive pth root of unity, for a prime p invertible in K. By local duality H²(G_K, 𝔽_p) is dual to H⁰(G_K, μ_p) = μ_p(K), so it vanishes. Inflation from the maximal pro-p quotient G_K(p) is injective in degree two, so H²(G_K(p), 𝔽_p) vanishes too, which for a pro-p group says cd_p G_K(p) ≤ 1. By Serre's theorem a finitely generated pro-p group of cohomological dimension at most one is free.

When moreover K is a finite extension of ℚ_[p], local duality and Kummer theory give #H¹(G_K, 𝔽_p) = #(Kˣ/(Kˣ)^p) = p ^ ([K : ℚ_[p]] + 1). So G_K(p) has [K : ℚ_[p]] + 1 generators, and it is the free pro-p group of that rank. This is Shafarevich's theorem; together with Demushkin's theorem for K ∋ μ_p it is the dichotomy of the local maximal pro-p Galois groups.

Main results

• TauCeti.subsingleton_cohomFp_two_absoluteGaloisGroupProP_of_not_mu and TauCeti.finrank_cohomFp_two_absoluteGaloisGroupProP_of_not_mu: H²(G_K(p), 𝔽_p) = 0.
• TauCeti.cohomologicalDimensionAt_absoluteGaloisGroupProP_le_one_of_not_mu: cd_p G_K(p) ≤ 1.
• TauCeti.finrank_cohomFp_one_absoluteGaloisGroupProP_of_not_mu: dim H¹(G_K(p), 𝔽_p) = [K : ℚ_[p]] + 1.
• TauCeti.finrank_cohomFp_one_absoluteGaloisGroupProP and TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroupProP: the Euler-characteristic identities dim H¹(G_K(p), 𝔽_p) = 1 + dim H²(G_K(p), 𝔽_p) + [K : ℚ_[p]] and d(G_K(p)) = 1 + dim H²(G_K(p), 𝔽_p) + [K : ℚ_[p]].
• TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroupProP_of_not_mu: G_K(p) has [K : ℚ_[p]] + 1 topological generators.
• TauCeti.nonempty_continuousMulEquiv_freeProP_of_not_mu: G_K(p) is the free pro-p group on [K : ℚ_[p]] + 1 generators.

References

• I. R. Shafarevich, On p-extensions, Mat. Sb. 20 (1947), 351–363.
• J.-P. Serre, Galois Cohomology, Chapter II, §5.6, Theorem 3.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (7.5.11).

theorem TauCeti.subsingleton_cohomFp_two_absoluteGaloisGroupProP_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ p) : Subsingleton ↑(cohomFp p (absoluteGaloisGroupProP p K) 2).toModuleCat

H²(G_K(p), 𝔽_p) vanishes for a nonarchimedean local field K containing no primitive pth root of unity, p being invertible in K: it injects into H²(G_K, 𝔽_p) by inflation.

theorem TauCeti.finrank_cohomFp_two_absoluteGaloisGroupProP_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ p) : Module.finrank (ZMod p) ↑(cohomFp p (absoluteGaloisGroupProP p K) 2).toModuleCat = 0

If a nonarchimedean local field K contains no primitive pth root of unity, with p invertible in K, then dim H²(G_K(p), 𝔽_p) = 0.

instance TauCeti.finite_cohomFp_two_absoluteGaloisGroupProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] : Finite ↑(cohomFp p (absoluteGaloisGroupProP p K) 2).toModuleCat

Degree-two cohomology of the maximal pro-p Galois group of a local field is finite when p is nonzero in the field, as it injects into H²(G_K, 𝔽_p) by inflation.

theorem TauCeti.finrank_cohomFp_two_absoluteGaloisGroupProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] : Module.finrank (ZMod p) ↑(cohomFp p (absoluteGaloisGroupProP p K) 2).toModuleCat = Module.finrank (ZMod p) ↑(cohomFp p (Field.absoluteGaloisGroup K) 2).toModuleCat

For a nonarchimedean local field K in which p is invertible, H²(G_K(p), 𝔽_p) and H²(G_K, 𝔽_p) have the same 𝔽_p-dimension: both are 1 when μ_p ⊆ K and 0 when μ_p ⊄ K.

theorem TauCeti.cohomologicalDimensionAt_absoluteGaloisGroupProP_le_one_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ p) : cohomologicalDimensionAt p (absoluteGaloisGroupProP p K) ≤ 1

cd_p G_K(p) ≤ 1 for a nonarchimedean local field K containing no primitive pth root of unity, p being invertible in K: for the pro-p group G_K(p) this is the vanishing of H²(G_K(p), 𝔽_p).

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroupProP_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [ValuativeExtension ℚ_[p] K] (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ p) : Module.finrank (ZMod p) ↑(cohomFp p (absoluteGaloisGroupProP p K) 1).toModuleCat = Module.finrank ℚ_[p] K + 1

If a finite compatible extension K of ℚ_[p] contains no primitive pth root of unity, then dim H¹(G_K(p), 𝔽_p) = [K : ℚ_[p]] + 1.

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroupProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [ValuativeExtension ℚ_[p] K] : Module.finrank (ZMod p) ↑(cohomFp p (absoluteGaloisGroupProP p K) 1).toModuleCat = 1 + Module.finrank (ZMod p) ↑(cohomFp p (absoluteGaloisGroupProP p K) 2).toModuleCat + Module.finrank ℚ_[p] K

The Euler-characteristic identity for G_K(p) over a finite compatible extension K of ℚ_[p]: dim H¹(G_K(p), 𝔽_p) = 1 + dim H²(G_K(p), 𝔽_p) + [K : ℚ_[p]].

theorem TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroupProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [ValuativeExtension ℚ_[p] K] (hfg : IsTopologicallyFinitelyGenerated (absoluteGaloisGroupProP p K)) : topologicalGeneratorRankNat (absoluteGaloisGroupProP p K) hfg = 1 + Module.finrank (ZMod p) ↑(cohomFp p (absoluteGaloisGroupProP p K) 2).toModuleCat + Module.finrank ℚ_[p] K

For a finite compatible extension K of ℚ_[p], the topological generator rank of G_K(p) is 1 + dim H²(G_K(p), 𝔽_p) + [K : ℚ_[p]]: [K : ℚ_[p]] + 2 when μ_p ⊆ K and [K : ℚ_[p]] + 1 when μ_p ⊄ K.

theorem TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroupProP_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [ValuativeExtension ℚ_[p] K] (hfg : IsTopologicallyFinitelyGenerated (absoluteGaloisGroupProP p K)) (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ p) : topologicalGeneratorRankNat (absoluteGaloisGroupProP p K) hfg = Module.finrank ℚ_[p] K + 1

If a finite compatible extension K of ℚ_[p] contains no primitive pth root of unity, its maximal pro-p Galois group has exactly [K : ℚ_[p]] + 1 topological generators.

theorem TauCeti.nonempty_continuousMulEquiv_freeProP_of_not_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [ValuativeExtension ℚ_[p] K] (hmu : ¬∃ (ζ : K), IsPrimitiveRoot ζ p) : Nonempty (absoluteGaloisGroupProP p K ≃ₜ* freeProP p (Fin (Module.finrank ℚ_[p] K + 1)))

Shafarevich's theorem. If a finite compatible extension K of ℚ_[p] contains no primitive pth root of unity, its maximal pro-p Galois group G_K(p) is the free pro-p group on [K : ℚ_[p]] + 1 generators.