Local maximal pro-p Galois groups are Demushkin groups

Let K be a nonarchimedean local field containing a primitive pth root of unity, for a prime p. Then the maximal pro-p quotient G_K(p) of its absolute Galois group is a Demushkin group: it is pro-p, H¹(G_K(p), 𝔽_p) is finite, H²(G_K(p), 𝔽_p) is one-dimensional, and the cup-product pairing on H¹(G_K(p), 𝔽_p) is perfect. All four clauses are read off from G_K through inflation, which is an isomorphism in degrees one and two.

When moreover K is a finite extension of ℚ_[p], the rank of this Demushkin group, its number of topological generators, is [K : ℚ_[p]] + 2; this is the rank at which Labute's classification of Demushkin groups is applied to G_K(p).

The other invariant entering that classification is the canonical character of the Demushkin group, the unique continuous character G_K(p) → ℤ_pˣ with Labute's prescription property. For G_K(p) it is the cyclotomic orientation, the character through which the p-adic cyclotomic character of G_K factors, because the cyclotomic orientation has the prescription property by Kummer theory. In particular the canonical character and the cyclotomic character have the same image in ℤ_pˣ.

Main results

• TauCeti.isDemushkin_absoluteGaloisGroupProP_of_mu: G_K(p) is a Demushkin group when K contains a primitive pth root of unity.
• TauCeti.demushkinRank_absoluteGaloisGroupProP: its rank is [K : ℚ_[p]] + 2.
• TauCeti.demushkinCharacter_absoluteGaloisGroupProP: its canonical character is the cyclotomic orientation.
• TauCeti.range_demushkinCharacter_absoluteGaloisGroupProP: the image of its canonical character is the image of the cyclotomic character.

References

• S. P. Demushkin, The group of a maximal p-extension of a local field, Izv. Akad. Nauk SSSR Ser. Mat. 25 (1961), 329–346.
• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132.
• J.-P. Serre, Galois Cohomology, Chapter II, §5.6, Theorem 4.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (7.5.11).

theorem TauCeti.isDemushkin_absoluteGaloisGroupProP_of_mu (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : IsDemushkin p (absoluteGaloisGroupProP p K)

Demushkin's theorem: the maximal pro-p quotient G_K(p) of the absolute Galois group of a nonarchimedean local field K containing a primitive pth root of unity is a Demushkin group.

theorem TauCeti.demushkinRank_absoluteGaloisGroupProP (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) : demushkinRank ⋯ = Module.finrank ℚ_[p] K + 2

The rank of the Demushkin group G_K(p) is [K : ℚ_[p]] + 2 for a finite extension K of ℚ_[p] containing a primitive pth root of unity.

theorem TauCeti.demushkinCharacter_absoluteGaloisGroupProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : demushkinCharacter ⋯ = cyclotomicOrientation p K hmu

The canonical character of the Demushkin group G_K(p) is the cyclotomic orientation: the unique continuous character G_K(p) → ℤ_pˣ with the prescription property is the character through which the p-adic cyclotomic character of G_K factors, for a nonarchimedean local field K containing a primitive pth root of unity.

@[simp]

theorem TauCeti.range_demushkinCharacter_absoluteGaloisGroupProP (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hmu : ∃ (ζ : K), IsPrimitiveRoot ζ p) : (↑(demushkinCharacter ⋯)).range = (localCyclotomicCharacter p K).range

The image of the canonical character of G_K(p) is the image of the cyclotomic character of G_K, for a nonarchimedean local field K containing a primitive pth root of unity.