The classes of the Demushkin normal-form words in degree one

Let H be a profinite group, p a prime and λ_k = λ_k(H) its lower p-series, with graded pieces gr_k(H) = λ_k ⧸ λ_{k+1}. The three normal-form relator words of the classification of Demushkin groups,

• x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) for p ∣ q,
• x₁² x₂^{2^f} (x₂, x₃)(x₄, x₅) ⋯ (x_{n-1}, x_n) for f ≥ 2,
• x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) for 4 ∣ a and f ≥ 2,

together with the odd word at level f = ∞, x₁² (x₂, x₃)(x₄, x₅) ⋯ (x_{n-1}, x_n), read on any tuple x : ℕ → H, are products of p-th powers and Labute commutators (x, y) = x⁻¹y⁻¹xy, so they lie in λ_1(H), the pro-p Frattini subgroup; for this membership alone the weaker hypotheses f ≥ 1 and 2 ∣ a suffice, and the classes are computed under these weaker hypotheses. This file computes their classes in gr_1(H): the class of a Labute commutator is the bracket of the degree-zero classes, the class of a p-th power g ^ (p c) is c times the p-power class π ⟦g⟧, and so the class of a normal-form word is the sum of the brackets of its commutator pairs, plus (q / p) • π ξ₁ for the first word, π ξ₁ + 2^{f-1} • π ξ₂ for the odd dyadic word, (1 + a/2) • π ξ₁ + 2^{f-1} • π ξ₃ for the even one and π ξ₁ for the odd word at f = ∞, where ξ_i ∈ gr_0(H) is the class of x_i. The factors x₂^{2^f} and x₃^{2^f} with f ≥ 2, and x₁^a with 4 ∣ a, are fourth powers and lie in λ_2, so under the normal-form hypotheses they do not contribute; in particular the odd word at a finite level f ≥ 2 and the odd word at f = ∞ have the same class.

These are the classes of the normal-form relators modulo λ_2 (Labute, Proposition 4); the theorem that a relator whose degree-one form is nondegenerate is carried into one of them by a change of basis of the free pro-p group is proved in TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.DegreeOneForm.

Main results

• TauCeti.demushkinWordNeTwo_mem_pLowerCentralSeries_one, TauCeti.demushkinWordTwoOdd_mem_pLowerCentralSeries_one, TauCeti.demushkinWordTwoEven_mem_pLowerCentralSeries_one, TauCeti.demushkinWordTwoOddTop_mem_pLowerCentralSeries_one: the words lie in λ_1.
• TauCeti.gradedMk_labuteComm: the class of (x, y) in gr_1(H) is the bracket [ξ, η] of the classes of x and y.
• TauCeti.gradedMk_demushkinWordNeTwo, TauCeti.gradedMk_demushkinWordTwoOdd, TauCeti.gradedMk_demushkinWordTwoEven, TauCeti.gradedMk_demushkinWordTwoOddTop: the classes of the four words in gr_1(H); TauCeti.gradedMk_demushkinWordTwoOdd_eq_gradedMk_demushkinWordTwoOddTop: for f ≥ 2 the odd word and the odd word at f = ∞ have the same class.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, Proposition 4.

The words lie in λ_1

theorem TauCeti.demushkinWordNeTwo_mem_pLowerCentralSeries_one {p : ℕ} [Fact (Nat.Prime p)] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {q : ℕ} (hq : p ∣ q) (n : ℕ) (x : ℕ → H) : demushkinWordNeTwo q n x ∈ pLowerCentralSeries p H 1

For p ∣ q, the q ≠ 2 normal-form word lies in λ_1.

theorem TauCeti.demushkinWordTwoOdd_mem_pLowerCentralSeries_one {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {f : ℕ} (hf : 0 < f) (n : ℕ) (x : ℕ → H) : demushkinWordTwoOdd f n x ∈ pLowerCentralSeries 2 H 1

For f ≥ 1, the q = 2, n odd normal-form word lies in λ_1.

theorem TauCeti.demushkinWordTwoOddTop_mem_pLowerCentralSeries_one {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (n : ℕ) (x : ℕ → H) : demushkinWordTwoOddTop n x ∈ pLowerCentralSeries 2 H 1

The q = 2, n odd normal-form word at level f = ∞ lies in λ_1.

theorem TauCeti.demushkinWordTwoEven_mem_pLowerCentralSeries_one {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {a f : ℕ} (ha : 2 ∣ a) (hf : 0 < f) (n : ℕ) (x : ℕ → H) : demushkinWordTwoEven a f n x ∈ pLowerCentralSeries 2 H 1

For a even and f ≥ 1, the q = 2, n even normal-form word lies in λ_1.

The classes of commutators and of the words

theorem TauCeti.gradedMk_labuteComm {p : ℕ} {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (x y : H) (h : labuteComm x y ∈ pLowerCentralSeries p H 1) : gradedMk p H 1 ⟨labuteComm x y, h⟩ = ((gradedBracket p H 0 0) (gradedMkZero p H x)) (gradedMkZero p H y)

The class of a Labute commutator (x, y) = x⁻¹ y⁻¹ x y in gr_1(H) is the bracket of the classes of x and y: it is the group commutator ⁅x⁻¹, y⁻¹⁆, and the bracket is bilinear.

theorem TauCeti.gradedMk_list_prod_labuteComm {p : ℕ} [Fact (Nat.Prime p)] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (N : ℕ) (a b : ℕ → H) (h : (List.map (fun (i : ℕ) => labuteComm (a i) (b i)) (List.range N)).prod ∈ pLowerCentralSeries p H 1) : gradedMk p H 1 ⟨(List.map (fun (i : ℕ) => labuteComm (a i) (b i)) (List.range N)).prod, h⟩ = ∑ i ∈ Finset.range N, ((gradedBracket p H 0 0) (gradedMkZero p H (a i))) (gradedMkZero p H (b i))

The class in gr_1(H) of a product of Labute commutators is the sum of the brackets.

theorem TauCeti.gradedMk_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {q : ℕ} (hq : p ∣ q) (n : ℕ) (x : ℕ → H) : gradedMk p H 1 ⟨demushkinWordNeTwo q n x, ⋯⟩ = (q / p) • gradedPow p H 0 (gradedMkZero p H (x 0)) + ∑ i ∈ Finset.range (n / 2), ((gradedBracket p H 0 0) (gradedMkZero p H (x (2 * i)))) (gradedMkZero p H (x (2 * i + 1)))

The class of the q ≠ 2 normal-form word x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) in gr_1, for p ∣ q: (q / p) • π ξ₁ + [ξ₁, ξ₂] + ⋯ + [ξ_{n-1}, ξ_n].

theorem TauCeti.gradedMk_demushkinWordTwoOdd {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {f : ℕ} (hf : 0 < f) (n : ℕ) (x : ℕ → H) : gradedMk 2 H 1 ⟨demushkinWordTwoOdd f n x, ⋯⟩ = gradedPow 2 H 0 (gradedMkZero 2 H (x 0)) + 2 ^ (f - 1) • gradedPow 2 H 0 (gradedMkZero 2 H (x 1)) + ∑ i ∈ Finset.range (n / 2), ((gradedBracket 2 H 0 0) (gradedMkZero 2 H (x (2 * i + 1)))) (gradedMkZero 2 H (x (2 * i + 2)))

The class of the q = 2, n odd normal-form word x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) in gr_1, for f ≥ 1: π ξ₁ + 2^{f-1} π ξ₂ + [ξ₂, ξ₃] + ⋯ + [ξ_{n-1}, ξ_n]. The factor x₂^{2^f} contributes π ξ₂ when f = 1 and nothing when f ≥ 2, being then a fourth power, hence in λ_2.

theorem TauCeti.gradedMk_demushkinWordTwoOddTop {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (n : ℕ) (x : ℕ → H) : gradedMk 2 H 1 ⟨demushkinWordTwoOddTop n x, ⋯⟩ = gradedPow 2 H 0 (gradedMkZero 2 H (x 0)) + ∑ i ∈ Finset.range (n / 2), ((gradedBracket 2 H 0 0) (gradedMkZero 2 H (x (2 * i + 1)))) (gradedMkZero 2 H (x (2 * i + 2)))

The class of the q = 2, n odd normal-form word at level f = ∞ x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) in gr_1: π ξ₁ + [ξ₂, ξ₃] + ⋯ + [ξ_{n-1}, ξ_n].

theorem TauCeti.gradedMk_demushkinWordTwoOdd_eq_gradedMk_demushkinWordTwoOddTop {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {f : ℕ} (hf : 2 ≤ f) (n : ℕ) (x : ℕ → H) : gradedMk 2 H 1 ⟨demushkinWordTwoOdd f n x, ⋯⟩ = gradedMk 2 H 1 ⟨demushkinWordTwoOddTop n x, ⋯⟩

For f ≥ 2 the odd word and the odd word at f = ∞ have the same class in gr_1: the factor x₂^{2^f} is a fourth power and lies in λ_2. This is the sense in which x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) is the normal form of x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) modulo λ_2.

theorem TauCeti.gradedMk_demushkinWordTwoEven {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {a f : ℕ} (ha : 2 ∣ a) (hf : 0 < f) (n : ℕ) (x : ℕ → H) : gradedMk 2 H 1 ⟨demushkinWordTwoEven a f n x, ⋯⟩ = (1 + a / 2) • gradedPow 2 H 0 (gradedMkZero 2 H (x 0)) + ((gradedBracket 2 H 0 0) (gradedMkZero 2 H (x 0))) (gradedMkZero 2 H (x 1)) + 2 ^ (f - 1) • gradedPow 2 H 0 (gradedMkZero 2 H (x 2)) + ∑ i ∈ Finset.range (n / 2 - 1), ((gradedBracket 2 H 0 0) (gradedMkZero 2 H (x (2 * i + 2)))) (gradedMkZero 2 H (x (2 * i + 3)))

The class of the q = 2, n even normal-form word x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) in gr_1, for a even and f ≥ 1: (1 + a/2) π ξ₁ + [ξ₁, ξ₂] + 2^{f-1} π ξ₃ + [ξ₃, ξ₄] + ⋯ + [ξ_{n-1}, ξ_n]. For 4 ∣ a and f ≥ 2 the factors x₁^a and x₃^{2^f} are fourth powers, hence in λ_2, and the class is π ξ₁ + [ξ₁, ξ₂] + [ξ₃, ξ₄] + ⋯ + [ξ_{n-1}, ξ_n].

theorem TauCeti.gradedMk_demushkinWordTwoEven_eq_gradedMk_demushkinWordNeTwo {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {a f : ℕ} (ha : 2 ∣ a) (hf : 2 ≤ f) {n : ℕ} (hn : 2 ≤ n) (x : ℕ → H) : gradedMk 2 H 1 ⟨demushkinWordTwoEven a f n x, ⋯⟩ = gradedMk 2 H 1 ⟨demushkinWordNeTwo (2 + a) n x, ⋯⟩

For f ≥ 2 the even-rank dyadic word has the class of the q ≠ 2 word with q = 2 + a: the factor x₃^{2^f} is a fourth power, hence lies in λ_2, so for n ≥ 2 and a even the classes in gr_1 of x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) and of x₁^{2+a} (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) agree.