The orientation image of a Demushkin group of even rank

Labute's existence theorem (Theorem 1 with Remark 2, after Serre) says that a pair (n, A), with n even and A ≤ ℤ_pˣ a closed pro-p subgroup, is the pair of invariants (rank, Im χ) of a Demushkin group exactly when (A : A^p) < p ^ n as supernatural numbers. The realization half is proved in TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Existence for every p, and the necessity half there only for the Demushkin groups with q ≠ 2, where (A : A^p) ≤ p. This file proves the necessity half for the remaining groups, those at p = 2 with q(G) = 2, and so closes the even-rank existence theorem as an equivalence.

The only content is in rank two. For A a closed subgroup of ℤ_2ˣ the index (A : A²) is 1, 2 or 4, and the value 4 occurs exactly for the non-procyclic subgroups {±1} × U^(f), 2 ≤ f < ∞. So (A : A²) < 2 ^ n can fail for an even rank n ≥ 2 only at n = 2 with A = {±1} × U^(f), and the theorem to prove is that a Demushkin group of rank two has procyclic orientation image, which is proved at every prime. When q(G) ≠ 2 the image lies in 1 + pℤ_p, and in 1 + 4ℤ_2 at p = 2, every closed subgroup of which is procyclic. When q(G) = 2 Labute's exact normal form presents G as ⟨x₁, x₂ ∣ x₁^{2+α} (x₁, x₂)⟩ with α ∈ 4ℤ_2 (TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Even.Exact), and the canonical character of that presented group is trivial on x₁, so its image is the closed subgroup generated by χ(x₂) = -(1 + α)⁻¹.

Main results

• exists_topologicalClosure_zpowers_eq_range_demushkinCharacter_of_demushkinRank_eq_two, in the namespace TauCeti.IsDemushkin: the orientation image of a Demushkin group of rank two is procyclic, at every prime; hence at p = 2 it is not {±1} × U^(f) (TauCeti.IsDemushkin.range_demushkinCharacter_ne_unitsPlusMinus_of_demushkinRank_eq_two).
• TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_even_demushkinRank: the necessity half of the existence theorem for even rank, (A : A^p) < p ^ n for the image A of the canonical character of a Demushkin group of even rank n, at every prime.
• TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_even: the existence theorem of the classification for even rank, as an equivalence.

References

• J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106--132, Theorem 1 and Remark 2, and the remark after the corollary to Theorem 4.
• J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki 1962/63, exp. 252, Théorème 3.2.

theorem TauCeti.IsDemushkin.exists_topologicalClosure_zpowers_eq_range_demushkinCharacter_of_demushkinRank_eq_two {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} [hp : Fact (Nat.Prime p)] (hG : IsDemushkin p G) (hn : demushkinRank hG = 2) : ∃ (u : ℤ_[p]ˣ), (Subgroup.zpowers u).topologicalClosure = (demushkinCharacter hG).range

A Demushkin group of rank two has procyclic orientation image. When q(G) ≠ 2 the image lies in 1 + pℤ_p, and in 1 + 4ℤ_2 at p = 2, every closed subgroup of which is procyclic. When q(G) = 2, so p = 2, the group is ⟨x₁, x₂ ∣ x₁^{2+α} (x₁, x₂)⟩ with α ∈ 4ℤ_2, its canonical character is trivial on x₁, and the image is the closed subgroup generated by χ(x₂).

theorem TauCeti.IsDemushkin.range_demushkinCharacter_ne_unitsPlusMinus_of_demushkinRank_eq_two {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (hn : demushkinRank hG = 2) {f : ℕ} (hf : 2 ≤ f) : (demushkinCharacter hG).range ≠ unitsPlusMinus f

The non-procyclic family does not occur at rank two: the orientation image of a Demushkin group of rank two at p = 2 is not {±1} × U^(f), 2 ≤ f < ∞.

theorem TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_even_demushkinRank {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} [hp : Fact (Nat.Prime p)] (hG : IsDemushkin p G) (hn : Even (demushkinRank hG)) : ((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 even rank (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). For a Demushkin group G of even rank n, the image A of its canonical character has (A : A^p) < p ^ n as supernatural numbers. For q(G) ≠ 2 this is TauCeti.IsDemushkin.profiniteIndex_subgroupOf_map_powMonoidHom_range_lt_of_demushkinQ_ne_two. For q(G) = 2, so p = 2, the index (A : A²) is 1, 2 or 4, and it is 4 only for the non-procyclic images {±1} × U^(f), which do not occur at rank two; so (A : A²) ≤ 2 < 2 ^ n, or (A : A²) = 4 < 2 ^ n with n ≥ 4.

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

The existence theorem of the classification of Demushkin groups for even rank, as an equivalence (Labute, Theorem 1 and Remark 2; Serre, Theorem 3.2). Let n be even and let A ≤ ℤ_pˣ be a closed pro-p subgroup. Then (n, A) is the pair of invariants (rank, Im χ) of a Demushkin group, presented on n generators by one relator, exactly when (A : A^p) < p ^ n as supernatural numbers. At p = 2 the condition excludes exactly n = 0 and the non-procyclic images {±1} × U^(f) in rank two; at an odd prime it excludes exactly n = 0. Together with TauCeti.exists_isDemushkin_range_demushkinCharacter_eq_iff_of_odd, this is the full list of the pairs of invariants of Demushkin groups.