Labute's normal form at an odd prime with q = p

Let F = freeProP p (Fin n) be the free pro-p group on n generators, with p odd, and let r ∈ λ_1(F) = Φ(F) be a relator whose class ρ ∈ gr_1(F) has nondegenerate degree-one form and a nonzero p-power part. The normal form modulo λ_2(F) (TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordNeTwo) brings r to x₁^p (x₁, x₂) ⋯ (x_{n-1}, x_n) modulo λ_2(F); the p-power part rules out the alternative q = 0, because p-power coordinates transform linearly under a change of basis. For odd p and a class with a p-power part whose derivatives span gr_0(F), which is the nondegeneracy of the form, the basis-modification map δ_ρ is onto every gr_{m+1}(F) (TauCeti.freeProP.range_basisModificationDelta_eq_top_of_odd), and the successive-approximation theorem turns the congruence modulo λ_2(F) into an equality: a continuous automorphism of F carries r to the normal-form word exactly.

For a Demushkin group G ≅ ⟨x₁, …, x_n ∣ r⟩ at an odd prime whose relator has a p-power part, this is Labute's Theorem 3 in the case q = p: G is presented by the single relator x₁^p (x₁, x₂) ⋯ (x_{n-1}, x_n). The p-power part of the class of r in gr_1(F) is nonzero exactly when the q-invariant of the presented group is p (TauCeti.demushkinQ_presentedProP_eq_iff_exists_degreeOneBasis_repr_inl_ne_zero). The other cases of that theorem with q ≠ 2, the relators without p-power part, where q ≠ p, are treated in TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.NeTwo, which also states the theorem for the presented group and intrinsically for a Demushkin group with q ≠ 2; the dyadic relators with q = 2 are not treated here.

Main results

• TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_odd: a continuous automorphism of F carries r to x₁^p (x₁, x₂) ⋯ (x_{n-1}, x_n).

References

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

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_odd {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hp : Odd p) (r : ↥(pLowerCentralSeries p (freeProP p (Fin n)) 1)) (hnd : (degreeOneForm (gradedMk p (freeProP p (Fin n)) 1 r)).Nondegenerate) (hc : ∃ (i : Fin n), ((degreeOneBasis p (Fin n)).repr (gradedMk p (freeProP p (Fin n)) 1 r)) (Sum.inl i) ≠ 0) : ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), e ↑r = demushkinWordNeTwo p n (freeProPGen p n)

Labute's normal form for odd p and q = p (Labute, Theorem 3, the case q = p). Let F be the free pro-p group on n generators with p odd, and let r ∈ λ_1(F) be a relator whose class in gr_1(F) has nondegenerate degree-one form and a nonzero p-power part. Then a continuous automorphism of F carries r to x₁^p (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n).