Labute's normal form for the dyadic Demushkin groups of even rank

Let F = freeProP 2 (Fin n) be the free pro-2 group on an even number n of generators and let r ∈ Φ(F) be a relator presenting a Demushkin group G = ⟨x₁, …, x_n ∣ r⟩ with q(G) = 2. Labute's Theorem 3 says that a continuous automorphism of F carries r to one of the words

x₁^{2+α} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), 2 ≤ f < ∞, or x₁^{2+α} (x₁, x₂) (x₃, x₄) ⋯ (x_{n-1}, x_n), the value f = ∞,

with a 2-adic exponent α ∈ 4ℤ₂, so that G is presented by that word. This file proves it, by Labute's route (pp. 118–119). Since q(G) = 2, the cup form of G is not alternating, and the normal form modulo λ_2(F) carries the class of r to that of x₁² (x₁, x₂) ⋯ (x_{n-1}, x_n) (TauCeti.IsDemushkin.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoEven); the successive approximation with tails then carries r itself to the intermediate form x₁^{2+α} (x₁, x₂) · ((x₃, x₄) ⋯ (x_{n-1}, x_n) x₃^{α₃} ⋯ x_n^{α_n}) with 2-adic exponents divisible by 4 (TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_padicPow_mul_labuteComm_mul). At rank n = 2 there is no tail relator and the theorem is proved. For n ≥ 4, the tail relator r' = (x₃, x₄) ⋯ (x_{n-1}, x_n) x₃^{α₃} ⋯ x_n^{α_n} is a word in x₃, …, x_n alone. Read in the free pro-2 group on those n - 2 ≥ 2 generators, r' has the class of (x₃, x₄) ⋯ (x_{n-1}, x_n) in gr_1, so it presents a Demushkin group whose q-invariant is not 2, and the normal-form theorem for q ≠ 2 (TauCeti.freeProP.exists_continuousMulEquiv_apply_demushkinWordNeTwo_zero_mul_eq) carries r' to x₃^{q'} (x₃, x₄) ⋯ (x_{n-1}, x_n) with q' = 0 or q' = 2^f, f ≥ 2. Extending that automorphism to F by fixing x₁ and x₂ (TauCeti.freeProP.finSuccExtend, twice) gives the theorem.

The exponent α is a genuine 2-adic integer, so the normal form is written with the 2-adic power x₁ ^ (2 + α) of TauCeti.IsProP.padicPow rather than as the word TauCeti.demushkinWordTwoEven, whose exponent is a natural number. The parameters α and f are not identified here: by the corollary to Labute's Theorem 4, the image of the canonical character of G is {±1} × U^(f) when 2^f ∣ α and the twisted subgroup U^[v₂(α)] otherwise, which is how the classification pins them, and this file proves only the existence of the normal form.

Main results

• exists_continuousMulEquiv_apply_eq_padicPow_mul_labuteComm_mul_demushkinWordNeTwo, in the namespace TauCeti.freeProP: a relator of F with the class of x₁² (x₁, x₂) ⋯ (x_{n-1}, x_n) in gr_1(F), n even, is carried by a continuous automorphism of F to x₁^{2+α} (x₁, x₂) x₃^{q'} (x₃, x₄) ⋯ (x_{n-1}, x_n) with 4 ∣ α in ℤ₂ and q' = 0 or q' = 2^f for some f ≥ 2.
• exists_continuousMulEquiv_apply_eq_padicPow_mul_labuteComm_mul_demushkinWordNeTwo, in the namespace TauCeti.IsDemushkin: Labute's Theorem 3 for q = 2 and even rank, the previous statement for a relator in Φ(F) presenting a Demushkin group with q = 2 on an even number of generators.
• exists_continuousMulEquiv_presentedProP_padicPow_mul_labuteComm_mul_demushkinWordNeTwo, in the namespace TauCeti.IsDemushkin: a Demushkin group at p = 2 of even rank n with q = 2 is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁^{2+α} (x₁, x₂) x₃^{q'} (x₃, x₄) ⋯ (x_{n-1}, x_n)⟩ for such α and q'.

References

• J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, §3, Theorem 3, case (3).
• J.-P. Serre, Galois Cohomology, Chapter I, §4.5.

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_padicPow_mul_labuteComm_mul_demushkinWordNeTwo {n : ℕ} (hn : Even n) (hn0 : 0 < n) (r : ↥(pLowerCentralSeries 2 (freeProP 2 (Fin n)) 1)) (h : gradedMk 2 (freeProP 2 (Fin n)) 1 r = gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordNeTwo 2 n (freeProPGen 2 n), ⋯⟩) : ∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)) (α : ℤ_[2]) (q : ℕ), 4 ∣ α ∧ (q = 0 ∨ ∃ (f : ℕ), 2 ≤ f ∧ q = 2 ^ f) ∧ e ↑r = ⋯.padicPow (freeProPGen 2 n 0) (2 + α) * labuteComm (freeProPGen 2 n 0) (freeProPGen 2 n 1) * demushkinWordNeTwo q (n - 2) fun (i : ℕ) => freeProPGen 2 n (i + 2)

The exact form of the dyadic relators of even rank. Let n ≥ 2 be even and let r ∈ λ_1(F) be a relator of the free pro-2 group F on n generators with the class of x₁² (x₁, x₂) (x₃, x₄) ⋯ (x_{n-1}, x_n) in gr_1(F). Then a continuous automorphism of F carries r to x₁^{2+α} (x₁, x₂) x₃^{q} (x₃, x₄) ⋯ (x_{n-1}, x_n), where α ∈ ℤ₂ is divisible by 4 and q = 0, Labute's level f = ∞, or q = 2^f for some f ≥ 2. The last factor is the q ≠ 2 word x₃^{q} (x₃, x₄) ⋯ (x_{n-1}, x_n) on n - 2 letters, read on the generators shifted by two. The theorem assumes only the degree-one class of r, not that r is the relator of a Demushkin group.

theorem TauCeti.IsDemushkin.exists_continuousMulEquiv_apply_eq_padicPow_mul_labuteComm_mul_demushkinWordNeTwo {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})) (hq : demushkinQ hG = 2) : ∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)) (α : ℤ_[2]) (q : ℕ), 4 ∣ α ∧ (q = 0 ∨ ∃ (f : ℕ), 2 ≤ f ∧ q = 2 ^ f) ∧ e r = ⋯.padicPow (freeProPGen 2 n 0) (2 + α) * labuteComm (freeProPGen 2 n 0) (freeProPGen 2 n 1) * demushkinWordNeTwo q (n - 2) fun (i : ℕ) => freeProPGen 2 n (i + 2)

Labute's normal form for q = 2 and even rank (Labute, Theorem 3, case (3)). 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⟩ with q(G) = 2. Then a continuous automorphism of F carries r to x₁^{2+α} (x₁, x₂) x₃^{q'} (x₃, x₄) ⋯ (x_{n-1}, x_n), where α ∈ ℤ₂ is divisible by 4 and q' = 0, Labute's level f = ∞, or q' = 2^f for some f ≥ 2. The last factor is the q ≠ 2 word x₃^{q'} (x₃, x₄) ⋯ (x_{n-1}, x_n) on n - 2 letters, read on the generators shifted by two.

theorem TauCeti.IsDemushkin.exists_continuousMulEquiv_presentedProP_padicPow_mul_labuteComm_mul_demushkinWordNeTwo {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin 2 G) (hn : Even (demushkinRank hG)) (hq : demushkinQ hG = 2) : ∃ (α : ℤ_[2]) (q : ℕ), 4 ∣ α ∧ (q = 0 ∨ ∃ (f : ℕ), 2 ≤ f ∧ q = 2 ^ f) ∧ Nonempty (G ≃ₜ* presentedProP 2 (Fin (demushkinRank hG)) {⋯.padicPow (freeProPGen 2 (demushkinRank hG) 0) (2 + α) * labuteComm (freeProPGen 2 (demushkinRank hG) 0) (freeProPGen 2 (demushkinRank hG) 1) * demushkinWordNeTwo q (demushkinRank hG - 2) fun (i : ℕ) => freeProPGen 2 (demushkinRank hG) (i + 2)})

Labute's normal form for a Demushkin group of even rank with q = 2, intrinsic form (Labute, Theorem 3, case (3)). A Demushkin group G at p = 2 of even rank n = demushkinRank hG with q(G) = 2 is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁^{2+α} (x₁, x₂) x₃^{q'} (x₃, x₄) ⋯ (x_{n-1}, x_n)⟩ for some α ∈ 4ℤ₂ and some q' which is 0 or 2^f with f ≥ 2.