Labute's normal form for q ≠ 2

Let F = freeProP p (Fin n) be the free pro-p group on n generators and let r ∈ Φ(F) be a relator presenting a Demushkin group G = ⟨x₁, …, x_n ∣ r⟩ with q-invariant q = q(G). Labute's Theorem 3 says that for q ≠ 2 a continuous automorphism of F carries r to the normal-form word x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n), so that G is presented by that word. The case q = p at an odd prime is proved in TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.OddPrime, where the basis-modification map δ_ρ is onto in every degree. This file proves the remaining cases q ≠ p, that is q = 0 and q = p^f with f ≥ 2, for every prime p including p = 2, and assembles the theorem for every q ≠ 2.

For q ≠ p every exponent sum of r is divisible by p ^ 2, so the class of r in gr_1(F) has no p-power part and the basis-modification map δ_ρ is no longer onto in every degree: the successive approximation cannot change the exponent vector of the relator, and has to be run with that vector held fixed. The normal form is therefore first proved for a relator whose exponent vector is already q e₁, with p ^ 2 ∣ q and nondegenerate degree-one form. The elementary automorphisms of TauCeti.Topology.Algebra.Group.Profinite.Free.ElementaryAutomorphism carry the exponent vector of any relator presenting a Demushkin group with q(G) ≠ p to q(G) e₁, which gives the theorem for q(G) ≠ p; together with the case q = p this is Labute's Theorem 3 for every q ≠ 2. The normal form is the input to the uniqueness theorem of TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Uniqueness: two Demushkin groups with the same rank and the same q-invariant q ≠ 2 are topologically isomorphic.

Main results

• TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_toAdd_exponentSum_eq: a relator with nondegenerate degree-one form and exponent vector q e₁, p ^ 2 ∣ q, is carried to x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) by a continuous automorphism of F.
• TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_demushkinQ_ne: a relator in Φ(F) presenting a Demushkin group with q(G) ≠ p is carried to x₁^{q(G)} (x₁, x₂) ⋯ (x_{n-1}, x_n).
• TauCeti.freeProP.exists_continuousMulEquiv_apply_demushkinWordNeTwo_zero_mul_eq: a relator (x₁, x₂) ⋯ (x_{n-1}, x_n) T with T ∈ λ_2(F) and n even presents a Demushkin group with q(G) ≠ p, and is carried to x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) with q = 0 or q = p^k, k ≥ 2.
• TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_demushkinQ_ne_two: Labute's Theorem 3 for q ≠ 2, the same for every q(G) ≠ 2.
• TauCeti.freeProP.exists_continuousMulEquiv_presentedProP_demushkinWordNeTwo_of_demushkinQ_ne_two and its intrinsic form IsDemushkin.exists_continuousMulEquiv_presentedProP_demushkinWordNeTwo_of_demushkinQ_ne_two: a Demushkin group with q(G) ≠ 2 is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁^{q(G)} (x₁, x₂) ⋯ (x_{n-1}, x_n)⟩ on n = demushkinRank hG generators.

References

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

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_toAdd_exponentSum_eq {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (r : ↥(pLowerCentralSeries p (freeProP p (Fin n)) 1)) (hnd : (degreeOneForm (gradedMk p (freeProP p (Fin n)) 1 r)).Nondegenerate) {q : ℕ} (hq : p ^ 2 ∣ q) (hv : ∀ (k : Fin n), Multiplicative.toAdd ((exponentSum p (Fin n)) ↑r) k = if ↑k = 0 then ↑q else 0) : ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), e ↑r = demushkinWordNeTwo q n (freeProPGen p n)

Labute's normal form for a relator with exponent vector q e₁, p ^ 2 ∣ q. Let F be the free pro-p group on n generators and let r ∈ λ_1(F) be a relator whose class in gr_1(F) has nondegenerate degree-one form, and whose exponent sums are q at x₁ and 0 at the other generators, for some q divisible by p ^ 2. Then a continuous automorphism of F carries r to x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_demushkinQ_ne {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} {r : freeProP p (Fin n)} (hr : r ∈ proPFrattini p (freeProP p (Fin n))) (hG : IsDemushkin p (presentedProP p (Fin n) {r})) (hq : demushkinQ hG ≠ p) : ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), e r = demushkinWordNeTwo (demushkinQ hG) n (freeProPGen p n)

Labute's normal form for q ≠ p (Labute, Theorem 3, the cases q = 0 and q = p^f with f ≥ 2). Let r ∈ Φ(F) be a relator of the free pro-p group on n generators presenting a Demushkin group G = ⟨x₁, …, x_n ∣ r⟩ with q-invariant q(G) ≠ p. Then a continuous automorphism of F carries r to x₁^{q(G)} (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_demushkinWordNeTwo_zero_mul_eq {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn : Even n) (hn0 : n ≠ 0) {T : freeProP p (Fin n)} (hT : T ∈ pLowerCentralSeries p (freeProP p (Fin n)) 2) : ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)) (q : ℕ), (q = 0 ∨ ∃ (k : ℕ), 2 ≤ k ∧ q = p ^ k) ∧ e (demushkinWordNeTwo 0 n (freeProPGen p n) * T) = demushkinWordNeTwo q n (freeProPGen p n)

A relator with the class of (x₁, x₂) ⋯ (x_{m-1}, x_m) is normalised by the case q ≠ p. Let m be even and positive and let T ∈ λ_2(F) in the free pro-p group F on m generators. Then (x₁, x₂) ⋯ (x_{m-1}, x_m) T presents a Demushkin group with q-invariant q ≠ p, and a continuous automorphism of F carries it to x₁^q (x₁, x₂) ⋯ (x_{m-1}, x_m), where q = 0 or q = p^k with k ≥ 2.

theorem TauCeti.freeProP.exists_continuousMulEquiv_apply_eq_demushkinWordNeTwo_of_demushkinQ_ne_two {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} {r : freeProP p (Fin n)} (hr : r ∈ proPFrattini p (freeProP p (Fin n))) (hG : IsDemushkin p (presentedProP p (Fin n) {r})) (hq : demushkinQ hG ≠ 2) : ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), e r = demushkinWordNeTwo (demushkinQ hG) n (freeProPGen p n)

Labute's normal form for q ≠ 2 (Labute, Theorem 3, the case q ≠ 2). Let r ∈ Φ(F) be a relator of the free pro-p group on n generators presenting a Demushkin group G = ⟨x₁, …, x_n ∣ r⟩ with q-invariant q(G) ≠ 2. Then a continuous automorphism of F carries r to x₁^{q(G)} (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.exists_continuousMulEquiv_presentedProP_demushkinWordNeTwo_of_demushkinQ_ne_two {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} {r : freeProP p (Fin n)} (hr : r ∈ proPFrattini p (freeProP p (Fin n))) (hG : IsDemushkin p (presentedProP p (Fin n) {r})) (hq : demushkinQ hG ≠ 2) : Nonempty (presentedProP p (Fin n) {r} ≃ₜ* presentedProP p (Fin n) {demushkinWordNeTwo (demushkinQ hG) n (freeProPGen p n)})

Labute's normal form for a one-relator Demushkin group with q ≠ 2. Let r ∈ Φ(F) be a relator of the free pro-p group on n generators presenting a Demushkin group with q-invariant q(G) ≠ 2. Then ⟨x₁, …, x_n ∣ r⟩ is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁^{q(G)} (x₁, x₂) ⋯ (x_{n-1}, x_n)⟩.

theorem TauCeti.IsDemushkin.exists_continuousMulEquiv_presentedProP_demushkinWordNeTwo_of_demushkinQ_ne_two {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsDemushkin p G) (hq : demushkinQ hG ≠ 2) : Nonempty (G ≃ₜ* presentedProP p (Fin (demushkinRank hG)) {demushkinWordNeTwo (demushkinQ hG) (demushkinRank hG) (freeProPGen p (demushkinRank hG))})

Labute's normal form for a Demushkin group with q ≠ 2, intrinsic form (Labute, Theorem 3, the case q ≠ 2). A Demushkin group G with q-invariant q(G) ≠ 2 is topologically isomorphic to ⟨x₁, …, x_n ∣ x₁^{q(G)} (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n)⟩ on n = demushkinRank hG generators.