Labute's normal form for the dyadic Demushkin groups of even rank with image {±1}

Let G be a Demushkin group at p = 2 of even rank n whose canonical character has image {±1}. This is the endpoint f = ∞ of the even-rank dyadic family of Labute's classification: G is presented on n generators by the single relator

x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n),

the normal-form word TauCeti.demushkinWordNeTwo 2 n; in particular two such groups of the same rank are topologically isomorphic. This file proves it.

Since -1 is a value of the canonical character and -1 ∉ 1 + 4ℤ₂, the q-invariant of G is 2 (TauCeti.demushkinQ_eq_two_of_neg_one_mem_range_demushkinCharacter), so Labute's Theorem 3 for q = 2 and even rank, IsDemushkin.exists_continuousMulEquiv_apply_eq_padicPow_mul_labuteComm_mul_demushkinWordNeTwo, carries a relator r ∈ Φ(F) of G to x₁^{2+α} (x₁, x₂) x₃^{q} (x₃, x₄) ⋯ (x_{n-1}, x_n) with α ∈ 4ℤ₂ and q ∈ {0} ∪ {2^f : f ≥ 2}. The character table of that word (TauCeti.IsDemushkin.eq_zero_and_eq_zero_of_range_demushkinCharacter_eq_zpowers_neg_one) shows that the image {±1} forces α = 0, and q = 0 as soon as the factor x₃^q is present, which leaves exactly the endpoint word.

Main results

• freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_range_eq_zpowers_neg_one: a relator in Φ(F) of the free pro-2 group on an even number of generators presenting a Demushkin group with image {±1} is carried to x₁² (x₁, x₂) ⋯ (x_{n-1}, x_n) by a continuous automorphism of F.
• TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_eq_zpowers_neg_one: Labute's Theorem 2 at the endpoint, two such relators are carried to each other by a continuous automorphism of F.
• nonempty_continuousMulEquiv_presentedProP_demushkinWordNeTwo_of_range_eq_zpowers_neg_one, in the namespace TauCeti.IsDemushkin: the intrinsic form, such a Demushkin group is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁² (x₁, x₂) ⋯ (x_{n-1}, x_n)⟩ on n = demushkinRank hG generators.
• IsDemushkin.nonempty_continuousMulEquiv_of_even_demushkinRank_of_range_eq_zpowers_neg_one: uniqueness, two Demushkin groups at p = 2 of the same even rank whose canonical characters have image {±1} are topologically isomorphic.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §3, Theorems 2, 3 and 4 and the corollary to Theorem 4.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.9.19).

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_range_eq_zpowers_neg_one {n : ℕ} (hn : Even n) {r : freeProP 2 (Fin n)} (hr : r ∈ proPFrattini 2 (freeProP 2 (Fin n))) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})) (hA : (demushkinCharacter hG).range = Subgroup.zpowers (-1)) : ∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), e r = demushkinWordNeTwo 2 n (freeProPGen 2 n)

Labute's normal form for the dyadic Demushkin groups of even rank with image {±1} (Labute, Theorem 3 and the corollary to Theorem 4). Let r ∈ Φ(F) be a relator of the free pro-2 group on an even number n of generators presenting a Demushkin group G = ⟨x₁, …, x_n ∣ r⟩ whose canonical character has image {±1}. Then a continuous automorphism of F carries r to x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_eq_zpowers_neg_one {n : ℕ} (hn : Even n) {r r' : freeProP 2 (Fin n)} (hr : r ∈ proPFrattini 2 (freeProP 2 (Fin n))) (hr' : r' ∈ proPFrattini 2 (freeProP 2 (Fin n))) (hG : IsDemushkin 2 (presentedProP 2 (Fin n) {r})) (hG' : IsDemushkin 2 (presentedProP 2 (Fin n) {r'})) (hA : (demushkinCharacter hG).range = Subgroup.zpowers (-1)) (hA' : (demushkinCharacter hG').range = Subgroup.zpowers (-1)) : ∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), e r = r'

Labute's Theorem 2 at the even-rank dyadic endpoint. Let r, r' ∈ Φ(F) be relators of the free pro-2 group on an even number n of generators presenting Demushkin groups whose canonical characters both have image {±1}. Then a continuous automorphism of F carries r to r'; in particular the closed normal closures of r and r' are carried to each other.

theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_presentedProP_demushkinWordNeTwo_of_range_eq_zpowers_neg_one {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (hn : Even (demushkinRank hG)) (hA : (demushkinCharacter hG).range = Subgroup.zpowers (-1)) : Nonempty (G ≃ₜ* presentedProP 2 (Fin (demushkinRank hG)) {demushkinWordNeTwo 2 (demushkinRank hG) (freeProPGen 2 (demushkinRank hG))})

Labute's normal form for a dyadic Demushkin group of even rank with image {±1}, intrinsic form. A Demushkin group G at p = 2 of even rank whose canonical character has image {±1} is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n)⟩ on n = demushkinRank hG generators.

theorem TauCeti.IsDemushkin.nonempty_continuousMulEquiv_of_even_demushkinRank_of_range_eq_zpowers_neg_one {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hG : IsDemushkin 2 G) (hH : IsDemushkin 2 H) (hn : demushkinRank hG = demushkinRank hH) (heven : Even (demushkinRank hG)) (hA : (demushkinCharacter hG).range = Subgroup.zpowers (-1)) (hB : (demushkinCharacter hH).range = Subgroup.zpowers (-1)) : Nonempty (G ≃ₜ* H)

Uniqueness of the dyadic Demushkin groups of even rank with image {±1} (Labute, Theorems 2 and 3). Two Demushkin groups at p = 2 of the same even rank whose canonical characters both have image {±1} are topologically isomorphic.