The existence theorem of the classification of Demushkin groups

The classification of Demushkin groups attaches to a Demushkin group G its rank n and the image A ≤ ℤ_pˣ of its canonical character, the unique continuous character with the prescription property (TauCeti.HasPrescriptionProperty). Labute's existence theorem (Theorem 1 with Remark 2, after Serre) says which pairs (n, A), with A a closed pro-p subgroup of ℤ_pˣ, occur:

1. n even and p ^ n > (A : A^p);
2. n odd with n ≥ 3, so p = 2, and A = {±1} × U^(f) with 2 ≤ f ≤ ∞;
3. n = 1 and A = {±1}.

This file proves the realization half for every pair of the three situations: each such pair is the pair of invariants of a Demushkin group, exhibited as a one-relator pro-p group ⟨x₁, …, xₙ ∣ r⟩ on n generators, presented by one of the normal-form words of TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Basic. The realizing group is Demushkin of rank n (TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.IsDemushkin), it has exactly one continuous character with the prescription property (TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Prescription), and the image of that character is A, which is what the statements here add: for each normal form, the image of every character with the prescription property, read off the forced values of that character. The pairs are matched to the words through the classification of the closed subgroups of ℤ_pˣ, the principal unit groups for odd p and Labute's four families U^(f), {±1} × U^(f), {±1}, U^[f] for p = 2:

A	realizing relator
1	(x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n), q = 0
U^(f) = 1 + p^f ℤ_p	x₁^{p^f} (x₁, x₂) ⋯ (x_{n-1}, x_n)
{±1}, n even	x₁² (x₁, x₂) ⋯ (x_{n-1}, x_n), q = 2
{±1} × U^(f), n even	x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), n ≥ 4
{±1} × U^(f), n odd	x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n)
{±1}, n odd, n ≥ 3	x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n), the level f = ∞
U^[g], n = 2	x₁^{2 + 2^g} (x₁, x₂)
U^[g], n ≥ 4	x₁^{2 + 2^g} (x₁, x₂) x₃^{2^{g+1}} (x₃, x₄) ⋯
{±1}, n = 1	x₁², the group ℤ/2

The condition p ^ n > (A : A^p) of the even case is exactly what excludes n = 0 and, at p = 2, the non-procyclic family {±1} × U^(f) in rank two, where (A : A²) = 4. In the odd case the endpoint f = ∞ is the row A = {±1} = {±1} × U^(∞), realized by the odd word at level f = ∞, and the rank-one situation is its instance n = 1, where that word reads x₁².

The converse half of the existence theorem, that no other pair occurs, is proved here for the Demushkin groups with q ≠ 2, which are those whose canonical character lands in 1 + 4ℤ_2 when p = 2 (TauCeti.demushkinQ_ne_two_iff_range_demushkinCharacter_le). It needs no normal form: the rank is even because the cup form is alternating (TauCeti.IsDemushkin.even_demushkinRank_of_demushkinQ_ne_two), and the image is 1 + qℤ_p or trivial (TauCeti.range_demushkinCharacter_eq_unitsPrincipal), with (A : A^p) ≤ p < p ^ n. On that locus the existence theorem is therefore an equivalence. For q = 2 the converse is Labute's Theorem 1 through the dyadic normal forms and is not proved here.

Main results

• TauCeti.range_eq_unitsPrincipal_of_hasPrescriptionProperty_demushkinWordNeTwo, TauCeti.range_eq_bot_of_hasPrescriptionProperty_demushkinWordNeTwo, TauCeti.range_eq_zpowers_neg_one_of_hasPrescriptionProperty_demushkinWordNeTwo, TauCeti.range_eq_unitsPlusMinus_of_hasPrescriptionProperty_demushkinWordTwoOdd, TauCeti.range_eq_zpowers_neg_one_of_hasPrescriptionProperty_demushkinWordTwoOdd_one, TauCeti.range_eq_zpowers_neg_one_of_hasPrescriptionProperty_demushkinWordTwoOddTop, TauCeti.range_eq_unitsPlusMinus_of_hasPrescriptionProperty_demushkinWordTwoEven, TauCeti.range_eq_of_hasPrescriptionProperty_demushkinWordTwoEven_of_not_dvd, TauCeti.range_eq_of_hasPrescriptionProperty_demushkinWordTwoRankTwo_of_not_dvd: the image of the canonical character of each normal form, as the image of any character with the prescription property; the last two are the twisted subgroups U^[g] of the words whose exponent α has exact divisibility depth g, below the level f in the even-rank word on n ≥ 4 generators and with no level condition in rank two.
• TauCeti.exists_isDemushkin_range_eq_bot_of_even, TauCeti.exists_isDemushkin_range_eq_unitsPrincipal_of_even, TauCeti.exists_isDemushkin_range_eq_zpowers_neg_one_of_even, TauCeti.exists_isDemushkin_range_eq_unitsPlusMinus_of_even, TauCeti.exists_isDemushkin_range_eq_topologicalClosure_zpowers_of_even: each family of closed subgroups of ℤ_pˣ is realized in even rank by the normal form of the table.
• TauCeti.exists_isDemushkin_range_eq_of_even_of_lt: the existence theorem in even rank: for n even and A ≤ ℤ_pˣ closed and pro-p with (A : A^p) < p ^ n, a Demushkin group of rank n presented on n generators by one relator, whose unique character with the prescription property has image A.
• TauCeti.exists_isDemushkin_range_eq_unitsPlusMinus_of_odd: the existence theorem in odd rank n ≥ 3, for A = {±1} × U^(f) with 2 ≤ f < ∞.
• TauCeti.exists_isDemushkin_range_eq_zpowers_neg_one_of_odd: the existence theorem in odd rank at level f = ∞, for A = {±1} and every odd n.
• TauCeti.exists_isDemushkin_one_range_eq_zpowers_neg_one: the existence theorem in rank one, for A = {±1}, the instance n = 1 of the previous statement.
• TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_demushkinQ_ne_two: the necessity half for q ≠ 2: the image A of the canonical character of a Demushkin group of rank n with q ≠ 2 has (A : A^p) < p ^ n.
• TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff: the existence theorem for q ≠ 2 as an equivalence: for A ≤ ℤ_pˣ closed and pro-p, contained in 1 + 4ℤ_2 when p = 2, the pair (n, A) is realized exactly when n is even and (A : A^p) < p ^ n.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, Theorem 1, Theorem 4 and its corollary, and Remark 2.
• J.-P. Serre, Structure de certains pro-p-groupes, Séminaire Bourbaki 252 (1962/63), Theorem 3.2.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.9.10) and (3.9.19).

The image of the canonical character of each normal form

theorem TauCeti.range_eq_topologicalClosure_zpowers_of_hasPrescriptionProperty_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {q n : ℕ} {χ : presentedProP p (Fin n) {demushkinWordNeTwo q n (freeProPGen p n)} →ₜ* ℤ_[p]ˣ} (hq : p ∣ q) (hn : Even n) (hn₁ : 1 < n) (hχ : HasPrescriptionProperty χ) : χ.range = (Subgroup.zpowers (χ (presentedProPGen p n {demushkinWordNeTwo q n (freeProPGen p n)} 1))).topologicalClosure

The image of a character with the prescription property of the q ≠ 2 normal form is the closed subgroup generated by its value on x₂, for p ∣ q and n ≥ 2 even.

theorem TauCeti.range_eq_unitsPrincipal_of_hasPrescriptionProperty_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {q n : ℕ} {χ : presentedProP p (Fin n) {demushkinWordNeTwo q n (freeProPGen p n)} →ₜ* ℤ_[p]ˣ} (hn : Even n) (hn₁ : 1 < n) {f : ℕ} (hq : q = p ^ f) (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) (hχ : HasPrescriptionProperty χ) : χ.range = unitsPrincipal p f

The image of the canonical character of the q ≠ 2 normal form is U^(f) = 1 + qℤ_p, for q = p ^ f with f ≥ 1, and f ≥ 2 when p = 2, and n ≥ 2 even: any character with the prescription property takes x₂ to (1 - q)⁻¹, of exact level f.

theorem TauCeti.range_eq_bot_of_hasPrescriptionProperty_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {q n : ℕ} {χ : presentedProP p (Fin n) {demushkinWordNeTwo q n (freeProPGen p n)} →ₜ* ℤ_[p]ˣ} (hn : Even n) (hn₁ : 1 < n) (hq : q = 0) (hχ : HasPrescriptionProperty χ) : χ.range = ⊥

The image of the canonical character of the q = 0 normal form is trivial, for n ≥ 2 even: the relator (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) has no p-power part, and any character with the prescription property takes x₂ to (1 - 0)⁻¹ = 1.

theorem TauCeti.range_eq_zpowers_neg_one_of_hasPrescriptionProperty_demushkinWordNeTwo {n : ℕ} {χ : presentedProP 2 (Fin n) {demushkinWordNeTwo 2 n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} (hn : Even n) (hn₁ : 1 < n) (hχ : HasPrescriptionProperty χ) : χ.range = Subgroup.zpowers (-1)

The image of the canonical character of the q = 2 even-rank form x₁² (x₁, x₂) ⋯ is {±1}, for n ≥ 2 even: any character with the prescription property takes x₂ to (1 - 2)⁻¹ = -1. This is the even-rank form with α = 0 and level f = ∞, whose image is the endpoint V^(∞) = {±1} of the table.

theorem TauCeti.range_eq_unitsPlusMinus_of_hasPrescriptionProperty_demushkinWordTwoOdd {f n : ℕ} (hf : 2 ≤ f) (hn : Odd n) (hn₂ : 2 < n) {χ : presentedProP 2 (Fin n) {demushkinWordTwoOdd f n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} (hχ : HasPrescriptionProperty χ) : χ.range = unitsPlusMinus f

The image of the canonical character of the q = 2, n odd normal form is {±1} × U^(f), for f ≥ 2 and n ≥ 3 odd: any character with the prescription property takes x₁ to -1 and x₃ to (1 - 2^f)⁻¹.

theorem TauCeti.range_eq_zpowers_neg_one_of_hasPrescriptionProperty_demushkinWordTwoOdd_one {f : ℕ} {χ : presentedProP 2 (Fin 1) {demushkinWordTwoOdd f 1 (freeProPGen 2 1)} →ₜ* ℤ_[2]ˣ} (hχ : HasPrescriptionProperty χ) : χ.range = Subgroup.zpowers (-1)

The image of the canonical character of ℤ/2 is {±1}: presented on one generator by x₁², which is the odd word at rank one for every level f, any character with the prescription property is the sign character χ(x₁) = -1.

theorem TauCeti.range_eq_zpowers_neg_one_of_hasPrescriptionProperty_demushkinWordTwoOddTop {n : ℕ} (hn : Odd n) {χ : presentedProP 2 (Fin n) {demushkinWordTwoOddTop n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} (hχ : HasPrescriptionProperty χ) : χ.range = Subgroup.zpowers (-1)

The image of the canonical character of the q = 2, n odd normal form at level f = ∞ is {±1}, for n odd: any character with the prescription property takes x₁ to -1 and every other generator to 1.

theorem TauCeti.range_eq_unitsPlusMinus_of_hasPrescriptionProperty_demushkinWordTwoEven {a f n : ℕ} (hf : 2 ≤ f) (hn : Even n) (hn₃ : 3 < n) (ha' : 2 ^ f ∣ ↑a) {χ : presentedProP 2 (Fin n) {demushkinWordTwoEven a f n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} (hχ : HasPrescriptionProperty χ) : χ.range = unitsPlusMinus f

The image of the canonical character of the q = 2, n even normal form when 2^f ∣ α is {±1} × U^(f), for f ≥ 2 and n ≥ 4 even: any character with the prescription property takes x₂ to -(1 + α)⁻¹ ∈ -U^(f) and x₄ to (1 - 2^f)⁻¹. This includes α = 0.

theorem TauCeti.range_eq_of_hasPrescriptionProperty_demushkinWordTwoEven_of_not_dvd {a f n g : ℕ} (hg : 2 ≤ g) (hag : 2 ^ g ∣ ↑a) (hag' : ¬2 ^ (g + 1) ∣ ↑a) (hgf : g < f) (hn : Even n) (hn₃ : 3 < n) {w : ℤ_[2]ˣ} (hw : ↑w = -1 + 2 ^ g) {χ : presentedProP 2 (Fin n) {demushkinWordTwoEven a f n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ} (hχ : HasPrescriptionProperty χ) : χ.range = (Subgroup.zpowers w).topologicalClosure

The image of the canonical character of the q = 2, n even normal form whose exponent α has exact divisibility depth g below the level f is the twisted subgroup U^[g], the closed subgroup generated by -1 + 2^g, for g ≥ 2 and n ≥ 4 even: any character with the prescription property takes x₂ to -(1 + α)⁻¹, which generates U^[g] because -(1 + α)⁻¹ has exact level g, and x₄ to (1 - 2^f)⁻¹ ∈ U^(f) ≤ U^(g+1) ≤ U^[g]. Neither α within its valuation nor the level f above g = v₂(α) is an invariant: every such pair presents a group with the same invariants.

theorem TauCeti.range_eq_of_hasPrescriptionProperty_demushkinWordTwoRankTwo_of_not_dvd {a g : ℕ} (hg : 2 ≤ g) (hag : 2 ^ g ∣ ↑a) (hag' : ¬2 ^ (g + 1) ∣ ↑a) {w : ℤ_[2]ˣ} (hw : ↑w = -1 + 2 ^ g) {χ : presentedProP 2 (Fin 2) {demushkinWordTwoRankTwo a (freeProPGen 2 2)} →ₜ* ℤ_[2]ˣ} (hχ : HasPrescriptionProperty χ) : χ.range = (Subgroup.zpowers w).topologicalClosure

The image of the canonical character of the rank-two q = 2 normal form whose exponent α has exact divisibility depth g is the twisted subgroup U^[g], the closed subgroup generated by -1 + 2^g, for g ≥ 2: any character with the prescription property takes x₂ to -(1 + α)⁻¹, which generates U^[g] because -(1 + α)⁻¹ has exact level g.

The existence theorem

Each family of closed subgroups of ℤ_pˣ is realized by one normal form; the existence theorem in even rank is the case analysis over the classification of the closed subgroups.

theorem TauCeti.exists_isDemushkin_range_eq_bot_of_even {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : Even n) (hn0 : n ≠ 0) : ∃ (r : freeProP p (Fin n)) (hG : IsDemushkin p (presentedProP p (Fin n) {r})), demushkinRank hG = n ∧ (∃! χ : presentedProP p (Fin n) {r} →ₜ* ℤ_[p]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP p (Fin n) {r} →ₜ* ℤ_[p]ˣ), HasPrescriptionProperty χ → χ.range = ⊥

The trivial subgroup is realized in every even rank n ≥ 2, by the relator (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) with q = 0, whose canonical character is trivial.

theorem TauCeti.exists_isDemushkin_range_eq_unitsPrincipal_of_even {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : Even n) (hn0 : n ≠ 0) {f : ℕ} (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) : ∃ (r : freeProP p (Fin n)) (hG : IsDemushkin p (presentedProP p (Fin n) {r})), demushkinRank hG = n ∧ (∃! χ : presentedProP p (Fin n) {r} →ₜ* ℤ_[p]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP p (Fin n) {r} →ₜ* ℤ_[p]ˣ), HasPrescriptionProperty χ → χ.range = unitsPrincipal p f

The principal unit group U^(f) = 1 + p^f ℤ_p is realized in every even rank n ≥ 2, for f ≥ 1, and f ≥ 2 when p = 2, by the relator x₁^{p^f} (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n).

theorem TauCeti.exists_isDemushkin_range_eq_zpowers_neg_one_of_even {n : ℕ} (hn : Even n) (hn0 : n ≠ 0) : ∃ (r : freeProP 2 (Fin n)) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})), demushkinRank hG = n ∧ (∃! χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ), HasPrescriptionProperty χ → χ.range = Subgroup.zpowers (-1)

The subgroup {±1} is realized in every even rank n ≥ 2, by the relator x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) with q = 2: the even dyadic form with α = 0 at level f = ∞.

theorem TauCeti.exists_isDemushkin_range_eq_unitsPlusMinus_of_even {n : ℕ} (hn : Even n) (hn₄ : 4 ≤ n) {f : ℕ} (hf : 2 ≤ f) : ∃ (r : freeProP 2 (Fin n)) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})), demushkinRank hG = n ∧ (∃! χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ), HasPrescriptionProperty χ → χ.range = unitsPlusMinus f

The subgroup {±1} × U^(f) is realized in every even rank n ≥ 4, for f ≥ 2, by the relator x₁² (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n): the even dyadic form with α = 0.

theorem TauCeti.exists_isDemushkin_range_eq_topologicalClosure_zpowers_of_even {n : ℕ} (hn : Even n) (hn0 : n ≠ 0) {g : ℕ} (hg : 2 ≤ g) {w : ℤ_[2]ˣ} (hw : ↑w = -1 + 2 ^ g) : ∃ (r : freeProP 2 (Fin n)) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})), demushkinRank hG = n ∧ (∃! χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ), HasPrescriptionProperty χ → χ.range = (Subgroup.zpowers w).topologicalClosure

The twisted subgroup U^[g], generated by -1 + 2^g, is realized in every even rank n ≥ 2, for g ≥ 2: by the relator x₁^{2 + 2^g} (x₁, x₂) in rank two, and by x₁^{2 + 2^g} (x₁, x₂) x₃^{2^{g+1}} (x₃, x₄) ⋯ (x_{n-1}, x_n) in rank n ≥ 4; these are the even dyadic forms with α = 2^g and v₂(α) < f.

theorem TauCeti.exists_isDemushkin_range_eq_of_even_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {A : Subgroup ℤ_[p]ˣ} (hA : IsClosed ↑A) (hAp : IsProP p ↥A) (hn : Even n) (hlt : ((Subgroup.map (powMonoidHom p) A).subgroupOf A).profiniteIndex < Supernatural.primePower ⟨p, ⋯⟩ ↑n) : ∃ (r : freeProP p (Fin n)) (hG : IsDemushkin p (presentedProP p (Fin n) {r})), demushkinRank hG = n ∧ (∃! χ : presentedProP p (Fin n) {r} →ₜ* ℤ_[p]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP p (Fin n) {r} →ₜ* ℤ_[p]ˣ), HasPrescriptionProperty χ → χ.range = A

The existence theorem of the classification of Demushkin groups, even rank (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). Let n be even and let A ≤ ℤ_pˣ be a closed pro-p subgroup with (A : A^p) < p ^ n as supernatural numbers. Then there is a Demushkin group of rank n, presented on n generators by a single relator r, which has exactly one continuous character with the prescription property, and that character has image A.

The hypothesis (A : A^p) < p ^ n excludes n = 0 and, at p = 2, the subgroups {±1} × U^(f) in rank two, where (A : A²) = 4; every other closed pro-p subgroup is realized in every even rank n ≥ 2. The pro-p hypothesis on A is used for odd p, where it places A inside the principal units 1 + pℤ_p; every closed subgroup of ℤ_2ˣ is pro-2.

theorem TauCeti.exists_isDemushkin_range_eq_unitsPlusMinus_of_odd {n : ℕ} (hn : Odd n) (hn₃ : 3 ≤ n) {f : ℕ} (hf : 2 ≤ f) : ∃ (r : freeProP 2 (Fin n)) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})), demushkinRank hG = n ∧ (∃! χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ), HasPrescriptionProperty χ → χ.range = unitsPlusMinus f

The existence theorem of the classification of Demushkin groups, odd rank n ≥ 3 (Labute, Theorem 1; Serre, Theorem 3.2). For n ≥ 3 odd and 2 ≤ f < ∞, there is a Demushkin group of rank n, presented on n generators by the single relator x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n), which has exactly one continuous character with the prescription property, and that character has image {±1} × U^(f). Here p = 2, the only prime with Demushkin groups of odd rank.

theorem TauCeti.exists_isDemushkin_range_eq_zpowers_neg_one_of_odd {n : ℕ} (hn : Odd n) : ∃ (r : freeProP 2 (Fin n)) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})), demushkinRank hG = n ∧ (∃! χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP 2 (Fin n) {r} →ₜ* ℤ_[2]ˣ), HasPrescriptionProperty χ → χ.range = Subgroup.zpowers (-1)

The existence theorem of the classification of Demushkin groups, odd rank at level f = ∞ (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). For n odd, there is a Demushkin group of rank n, presented on n generators by the single relator x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n), which has exactly one continuous character with the prescription property, and that character has image {±1} = {±1} × U^(∞). Here p = 2, the only prime with Demushkin groups of odd rank.

theorem TauCeti.exists_isDemushkin_one_range_eq_zpowers_neg_one : ∃ (r : freeProP 2 (Fin 1)) (hG : IsDemushkin 2 (presentedProP 2 (Fin 1) {r})), demushkinRank hG = 1 ∧ (∃! χ : presentedProP 2 (Fin 1) {r} →ₜ* ℤ_[2]ˣ, HasPrescriptionProperty χ) ∧ ∀ (χ : presentedProP 2 (Fin 1) {r} →ₜ* ℤ_[2]ˣ), HasPrescriptionProperty χ → χ.range = Subgroup.zpowers (-1)

The existence theorem of the classification of Demushkin groups, rank one (Labute, Remark 2 (iii); NSW (3.9.10)). There is a Demushkin group of rank 1, presented on one generator by the single relator x₁², namely ℤ/2, which has exactly one continuous character with the prescription property, and that character has image {±1}. This is the instance n = 1 of the odd-rank statement at level f = ∞, whose relator word reads x₁² at rank one.

The necessity half for q ≠ 2

theorem TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_demushkinQ_ne_two {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (hq2 : demushkinQ hG ≠ 2) : ((Subgroup.map (powMonoidHom p) (demushkinCharacter hG).range).subgroupOf (demushkinCharacter hG).range).profiniteIndex < Supernatural.primePower ⟨p, ⋯⟩ ↑(demushkinRank hG)

The necessity half of the existence theorem for q ≠ 2 (Labute, Theorem 1). For a Demushkin group G of rank n with q(G) ≠ 2, the image A of its canonical character has (A : A^p) < p ^ n. Indeed A is trivial, with (A : A^p) = 1, or the principal unit group 1 + qℤ_p, with (A : A^p) = p, while n ≥ 2. Together with the parity of the rank (TauCeti.IsDemushkin.even_demushkinRank_of_demushkinQ_ne_two), this places (n, A) in the first situation of the existence theorem.

theorem TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {A : Subgroup ℤ_[p]ˣ} (hA : IsClosed ↑A) (hAp : IsProP p ↥A) (hA₂ : p = 2 → A ≤ unitsPrincipal p 2) : (∃ (r : freeProP p (Fin n)) (hG : IsDemushkin p (presentedProP p (Fin n) {r})), demushkinRank hG = n ∧ (demushkinCharacter hG).range = A) ↔ Even n ∧ ((Subgroup.map (powMonoidHom p) A).subgroupOf A).profiniteIndex < Supernatural.primePower ⟨p, ⋯⟩ ↑n

The existence theorem of the classification for q ≠ 2, as an equivalence (Labute, Theorem 1 and Remark 2; Demushkin and Serre). Let A ≤ ℤ_pˣ be a closed pro-p subgroup, contained in 1 + 4ℤ_2 when p = 2; these are the possible images of the canonical characters of the Demushkin groups with q ≠ 2 (TauCeti.demushkinQ_ne_two_iff_range_demushkinCharacter_le). Then (n, A) is the pair of invariants of a Demushkin group, presented on n generators by one relator, exactly when n is even and (A : A^p) < p ^ n. Together with TauCeti.IsDemushkin.nonempty_continuousMulEquiv_of_range_demushkinCharacter_eq, this classifies the Demushkin groups with q ≠ 2 by their rank and the image of their canonical character.