Finite generation and rank of local maximal pro-p Galois groups

For a nonarchimedean local field K of characteristic different from the prime p, its maximal pro-p Galois group is topologically finitely generated. Degree-one inflation identifies its continuous cohomology with that of the absolute Galois group, whose finiteness then gives finite generation by the pro-p Burnside basis theorem.

For a compatible extension of ℚ_[p] containing a primitive pth root of unity, the generator rank is [K : ℚ_[p]] + 2. This is the rank used in Demushkin presentations; its computation needs only degree-one cohomology, independently of degree-two local duality. In particular ℚ_p(μ_p) has generator rank p + 1.

References

• J.-P. Serre, Galois Cohomology, I §4.2 and II §5.2.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.9.1) and (7.5.11).

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

Degree-one cohomology of the maximal pro-p Galois group of a local field is finite when p is nonzero in the field. In particular it is finite-dimensional over 𝔽_p.

theorem TauCeti.isTopologicallyFinitelyGenerated_absoluteGaloisGroupProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [NeZero ↑p] : IsTopologicallyFinitelyGenerated (absoluteGaloisGroupProP p K)

The maximal pro-p Galois group of a local field of characteristic different from p is topologically finitely generated.

theorem TauCeti.finrank_cohomFp_one_absoluteGaloisGroupProP_of_exists_isPrimitiveRoot (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [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 + 2

If a compatible extension of ℚ_[p] contains μ_p, the first cohomology of its maximal pro-p Galois group has dimension [K : ℚ_[p]] + 2.

theorem TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroupProP_of_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [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 + 2

If a compatible extension of ℚ_[p] contains μ_p, its maximal pro-p Galois group has exactly [K : ℚ_[p]] + 2 topological generators. The finite-generation witness is explicit, so the natural-valued rank is never applied to an infinitely generated group.

theorem TauCeti.topologicalGeneratorRankNat_cyclotomic_prime_ratPadic (p : ℕ) [Fact (Nat.Prime p)] (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [ValuativeExtension ℚ_[p] K] [IsCyclotomicExtension {p} ℚ_[p] K] (hfg : IsTopologicallyFinitelyGenerated (absoluteGaloisGroupProP p K)) : topologicalGeneratorRankNat (absoluteGaloisGroupProP p K) hfg = p + 1

The maximal pro-p Galois group of ℚ_p(μ_p) has generator rank p + 1. The statement applies to any compatible local-field model of the cyclotomic extension.