Documentation

TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Odd.Approximation

Labute's intermediate form for the dyadic relators of odd rank #

Let F = freeProP 2 (Fin n) be the free pro-2 group on an odd number n of generators and let r ∈ λ_1(F) be a relator with the class of x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) in gr_1(F), which is the normal form modulo λ_2(F) of the relators with q = 2 of odd rank. The dyadic span statement gr_{m+1}(F) = Im δ_ρ + T_{m+1}(ρ) of TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Two.Odd.Basic, whose tails are spanned by the 2-powers of the generators x₂, …, x_n, feeds the successive approximation with tails (TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_of_range_sup_gradedPowIterSpan_eq_top): a continuous automorphism of F carries r exactly to

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

with t_i in the closed procyclic subgroup generated by x_i and in λ_2(F). This is the intermediate form x₁² r₀(x) x₂^{α₂} ⋯ x_n^{α_n} of Labute's proof of Theorem 3 for q = 2, with 2-adic exponents α_i divisible by 4. The theorem of this module assumes only the degree-one class of r; it does not assume that r is the relator of a Demushkin group. The tail relator (x₂, x₃) ⋯ (x_{n-1}, x_n) t₂ ⋯ t_n is a word in the generators x₂, …, x_n alone. In Labute's proof, where r is the relator of a Demushkin group, this tail relator is again the relator of a Demushkin group, with q-invariant 2^f for some f ≥ 2 or f = ∞, and its normalisation to x₂^{2^f} (x₂, x₃) ⋯ is the case q ≠ 2 of the normal-form theorem. Neither of these two facts is proved here.

Main results #

References #

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordTwoOddTop_mul_padicPow {n : ℕ} (hn : Odd 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 ⟨demushkinWordTwoOddTop n (freeProPGen 2 n), ⋯⟩) :
∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)) (a : Fin n → ℤ_[2]), (∀ (i : Fin n), 4 ∣ a i) ∧ e ↑r = demushkinWordTwoOddTop n (freeProPGen 2 n) * (List.map (fun (i : Fin n) => ⋯.padicPow (of i) (a i)) (List.finRange n).tail).prod

Labute's intermediate form with explicit 2-adic exponents. Let n be odd 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_{n-1}, x_n) in gr_1(F). Then a continuous automorphism carries r to that word followed by 2-adic powers x_i ^ a_i of the remaining generators, where every exponent a_i is divisible by 4.