The relator words of the Demushkin normal forms

Labute's classification of Demushkin groups puts every finite-rank Demushkin group in one of three normal forms, each a pro-p group presented on n generators x₁, …, xₙ by a single relator word. This file presents these forms by the words

• x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n), for q ≠ 2 and n even;
• x₁² x₂^{2^f} (x₂, x₃)(x₄, x₅) ⋯ (x_{n-1}, x_n), for q = 2 and n odd;
• x₁^{2+α} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), for q = 2 and n even,

where (x, y) = x⁻¹y⁻¹xy is Labute's commutator. In the two q = 2 forms Labute also allows f = ∞, meaning that the factor x₂^{2^f}, resp. x₃^{2^f}, is absent. The first word above takes a natural number q, and the two q = 2 words take a natural-number level f; two f = ∞ forms have words of their own, with no level: the odd form x₁² (x₂, x₃)(x₄, x₅) ⋯ (x_{n-1}, x_n) is demushkinWordTwoOddTop, and the even form of rank two, x₁^{2+α} (x₁, x₂), where x₃ = 1 makes the even word read the same for every f, is demushkinWordTwoRankTwo. The even f = ∞ form of rank at least four is not presented here. This file defines the commutator and the five words on an arbitrary tuple x : ℕ → H of group elements, so that the same word can be read in a free pro-p group and in any group that receives it. Read on the ℕ-indexed generators TauCeti.freeProPGen and TauCeti.presentedProPGen, which are 1 out of range, the words carry no index-bound side conditions.

Under the conditions p ∣ q for the first word, 0 < f for the second, 2 ∣ a together with 0 < f for the third, 2 ∣ a for the rank-two word, and no condition for the odd word at f = ∞, each word is a product of p-th powers and commutators, so it lies in the pro-p Frattini subgroup of every topological group, in particular of the free pro-p group. Hence, under the same conditions, the presentation of a normal form on n generators is minimal: the presented group has topological generator rank exactly n.

Main definitions

• TauCeti.labuteComm: Labute's commutator (x, y) = x⁻¹y⁻¹xy.
• TauCeti.demushkinWordNeTwo, TauCeti.demushkinWordTwoOdd, TauCeti.demushkinWordTwoEven: the three normal-form relator words, on an arbitrary tuple; TauCeti.demushkinWordTwoOddTop: the odd word at level f = ∞, x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n); TauCeti.demushkinWordTwoRankTwo: the even word of rank two, x₁^{2+α} (x₁, x₂), with no level; TauCeti.demushkinWordTwoOdd_eq_demushkinWordTwoOddTop reads the odd word as the odd word at f = ∞ when x₂^{2^f} = 1, TauCeti.demushkinWordTwoEven_two reads the even word at rank two as the rank-two word, TauCeti.demushkinWordTwoRankTwo_eq_demushkinWordNeTwo reads the rank-two word as the q ≠ 2 word at q = 2 + α, and TauCeti.demushkinWordTwoOdd_one and TauCeti.demushkinWordTwoOddTop_one read the two odd words at rank one as x₁².

Main results

• TauCeti.demushkinWordNeTwo_presentedProPGen_eq_one and its four companions: the generators of the normal-form presentation satisfy its defining relation.
• TauCeti.demushkinWordNeTwo_mem_proPFrattini, TauCeti.demushkinWordTwoOdd_mem_proPFrattini, TauCeti.demushkinWordTwoEven_mem_proPFrattini, TauCeti.demushkinWordTwoRankTwo_mem_proPFrattini, TauCeti.demushkinWordTwoOddTop_mem_proPFrattini: each word lies in the pro-p Frattini subgroup, for p ∣ q, resp. 0 < f, resp. 2 ∣ a and 0 < f, resp. 2 ∣ a, resp. always.
• TauCeti.topologicalGeneratorRankNat_presentedProP_demushkinWordNeTwo and its four companions: under the same conditions, the normal-form presentation on n generators, resp. on two generators, is minimal.
• TauCeti.map_demushkinWordNeTwo_eq_one and its four companions: a character into a commutative group kills the word as soon as its values on the generators carrying a power have trivial power: χ(x₁)^q = 1, resp. χ(x₁)² = 1 and χ(x₂)^{2^f} = 1, resp. χ(x₁)^{2+a} = 1 and χ(x₃)^{2^f} = 1, resp. χ(x₁)^{2+a} = 1, resp. χ(x₁)² = 1.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, Theorems 1–4.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Theorem 3.9.19.

Labute's commutator

def TauCeti.labuteComm {H : Type u_1} [Group H] (x y : H) : H

Labute's commutator (x, y) = x⁻¹y⁻¹xy, the convention in which the Demushkin normal-form relators are written. Mathlib's ⁅x, y⁆ = xyx⁻¹y⁻¹ is the other convention; the two are related by TauCeti.labuteComm_eq_commutatorElement_inv_inv, and generate the same subgroups.

Equations

• TauCeti.labuteComm x y = x⁻¹ * y⁻¹ * x * y

theorem TauCeti.labuteComm_def {H : Type u_1} [Group H] (x y : H) : labuteComm x y = x⁻¹ * y⁻¹ * x * y

The defining equation of TauCeti.labuteComm.

theorem TauCeti.labuteComm_eq_commutatorElement_inv_inv {H : Type u_1} [Group H] (x y : H) : labuteComm x y = ⁅x⁻¹, y⁻¹⁆

Labute's commutator is Mathlib's commutator of the inverses: (x, y) = ⁅x⁻¹, y⁻¹⁆.

@[simp]

theorem TauCeti.map_labuteComm {H : Type u_1} [Group H] {K : Type u_2} {F : Type u_3} [Group K] [FunLike F H K] [MonoidHomClass F H K] (f : F) (x y : H) : f (labuteComm x y) = labuteComm (f x) (f y)

A monoid homomorphism carries Labute's commutator to Labute's commutator.

theorem TauCeti.labuteComm_eq_one_iff_commute {H : Type u_1} [Group H] (x y : H) : labuteComm x y = 1 ↔ Commute x y

Labute's commutator is trivial exactly when the two elements commute.

theorem Commute.labuteComm_eq_one {H : Type u_1} [Group H] {x y : H} (h : Commute x y) : TauCeti.labuteComm x y = 1

Labute's commutator of two commuting elements is trivial.

@[simp]

theorem TauCeti.labuteComm_eq_one {A : Type u_2} [CommGroup A] (x y : A) : labuteComm x y = 1

Labute's commutator is trivial in a commutative group.

theorem TauCeti.labuteComm_mem_commutator {H : Type u_1} [Group H] (x y : H) : labuteComm x y ∈ commutator H

Labute's commutator lies in the commutator subgroup.

theorem TauCeti.labuteComm_mem_proPFrattini {H : Type u_1} [Group H] [TopologicalSpace H] {p : ℕ} (hp : Nat.Prime p) (x y : H) : labuteComm x y ∈ proPFrattini p H

Labute's commutator lies in the pro-p Frattini subgroup of a topological group.

theorem TauCeti.labuteComm_mem_of_mem_left {H : Type u_1} [Group H] {N : Subgroup H} [N.Normal] {x : H} (hx : x ∈ N) (y : H) : labuteComm x y ∈ N

Labute's commutator (x, y) = x⁻¹ (y⁻¹ x y) of an element x of a normal subgroup N with any y lies in N.

theorem TauCeti.labuteComm_mem_commutator_of_mem {H : Type u_1} [Group H] {N : Subgroup H} {x y : H} (hx : x ∈ N) (hy : y ∈ N) : labuteComm x y ∈ ⁅N, N⁆

Labute's commutator of two elements of a subgroup N lies in ⁅N, N⁆.

theorem TauCeti.list_prod_map_labuteComm_range_mem_commutator {H : Type u_1} [Group H] {N : Subgroup H} (m : ℕ) {a b : ℕ → H} (ha : ∀ i < m, a i ∈ N) (hb : ∀ i < m, b i ∈ N) : (List.map (fun (i : ℕ) => labuteComm (a i) (b i)) (List.range m)).prod ∈ ⁅N, N⁆

A product of Labute's commutators of elements of a subgroup N lies in ⁅N, N⁆.

The three normal-form words

def TauCeti.demushkinWordNeTwo {H : Type u_1} [Group H] (q n : ℕ) (x : ℕ → H) : H

The q ≠ 2 normal-form word x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n), on an arbitrary tuple x : ℕ → H, with x 0 playing the role of x₁. The classification uses it for n even; the word has n / 2 commutator factors.

Equations

• TauCeti.demushkinWordNeTwo q n x = x 0 ^ q * (List.map (fun (i : ℕ) => TauCeti.labuteComm (x (2 * i)) (x (2 * i + 1))) (List.range (n / 2))).prod

theorem TauCeti.demushkinWordNeTwo_def {H : Type u_1} [Group H] (q n : ℕ) (x : ℕ → H) : demushkinWordNeTwo q n x = x 0 ^ q * (List.map (fun (i : ℕ) => labuteComm (x (2 * i)) (x (2 * i + 1))) (List.range (n / 2))).prod

The defining equation of TauCeti.demushkinWordNeTwo.

@[simp]

theorem TauCeti.demushkinWordNeTwo_zero_two {H : Type u_1} [Group H] (x : ℕ → H) : demushkinWordNeTwo 0 2 x = labuteComm (x 0) (x 1)

At q = 0 and rank two the word is the single commutator (x₁, x₂), the surface relation of ℤ_p × ℤ_p.

theorem TauCeti.demushkinWordNeTwo_eq_pow_mul_labuteComm_mul {H : Type u_1} [Group H] (q : ℕ) {n : ℕ} (hn : 2 ≤ n) (x : ℕ → H) : demushkinWordNeTwo q n x = x 0 ^ q * labuteComm (x 0) (x 1) * demushkinWordNeTwo 0 (n - 2) fun (i : ℕ) => x (i + 2)

For n ≥ 2 the q ≠ 2 word splits off its first commutator factor: it is x₁^q (x₁, x₂) times the q = 0 word (x₃, x₄) ⋯ (x_{n-1}, x_n) on n - 2 letters, read on the tuple shifted by two. This is the shape of Labute's intermediate form for the dyadic relators of even rank, whose tail relator is a word in x₃, …, x_n.

def TauCeti.demushkinWordTwoOdd {H : Type u_1} [Group H] (f n : ℕ) (x : ℕ → H) : H

The q = 2, n odd normal-form word x₁² x₂^{2^f} (x₂, x₃)(x₄, x₅) ⋯ (x_{n-1}, x_n), on an arbitrary tuple x : ℕ → H, with x 0 playing the role of x₁. The parameter f is finite; the word has n / 2 commutator factors.

Equations

• TauCeti.demushkinWordTwoOdd f n x = x 0 ^ 2 * x 1 ^ 2 ^ f * (List.map (fun (i : ℕ) => TauCeti.labuteComm (x (2 * i + 1)) (x (2 * i + 2))) (List.range (n / 2))).prod

theorem TauCeti.demushkinWordTwoOdd_def {H : Type u_1} [Group H] (f n : ℕ) (x : ℕ → H) : demushkinWordTwoOdd f n x = x 0 ^ 2 * x 1 ^ 2 ^ f * (List.map (fun (i : ℕ) => labuteComm (x (2 * i + 1)) (x (2 * i + 2))) (List.range (n / 2))).prod

The defining equation of TauCeti.demushkinWordTwoOdd.

@[simp]

theorem TauCeti.demushkinWordTwoOdd_one {H : Type u_1} [Group H] (f : ℕ) (x : ℕ → H) (hx : x 1 = 1) : demushkinWordTwoOdd f 1 x = x 0 ^ 2

At rank one the odd word is x₁², whatever the level f: the factor x₂^{2^f} is 1 because the second generator is out of range, and the commutator product is empty.

def TauCeti.demushkinWordTwoOddTop {H : Type u_1} [Group H] (n : ℕ) (x : ℕ → H) : H

The q = 2, n odd normal-form word at Labute's level f = ∞, x₁² (x₂, x₃)(x₄, x₅) ⋯ (x_{n-1}, x_n), on an arbitrary tuple x : ℕ → H, with x 0 playing the role of x₁: the odd word with the factor x₂^{2^f} absent. It carries no level, and the word has n / 2 commutator factors. On a tuple with x₂^{2^f} = 1 it agrees with demushkinWordTwoOdd f n x (TauCeti.demushkinWordTwoOdd_eq_demushkinWordTwoOddTop).

Equations

• TauCeti.demushkinWordTwoOddTop n x = x 0 ^ 2 * (List.map (fun (i : ℕ) => TauCeti.labuteComm (x (2 * i + 1)) (x (2 * i + 2))) (List.range (n / 2))).prod

theorem TauCeti.demushkinWordTwoOddTop_def {H : Type u_1} [Group H] (n : ℕ) (x : ℕ → H) : demushkinWordTwoOddTop n x = x 0 ^ 2 * (List.map (fun (i : ℕ) => labuteComm (x (2 * i + 1)) (x (2 * i + 2))) (List.range (n / 2))).prod

The defining equation of TauCeti.demushkinWordTwoOddTop.

theorem TauCeti.demushkinWordTwoOdd_eq_demushkinWordTwoOddTop {H : Type u_1} [Group H] (f n : ℕ) {x : ℕ → H} (hx : x 1 ^ 2 ^ f = 1) : demushkinWordTwoOdd f n x = demushkinWordTwoOddTop n x

The odd word at a finite level f is the odd word at level f = ∞ on every tuple whose second entry has trivial 2^f-th power, in particular when the second generator is out of range.

@[simp]

theorem TauCeti.demushkinWordTwoOddTop_one {H : Type u_1} [Group H] (x : ℕ → H) : demushkinWordTwoOddTop 1 x = x 0 ^ 2

At rank one the odd word at level f = ∞ is x₁²: the commutator product is empty.

theorem TauCeti.demushkinWordTwoOdd_eq_sq_mul_demushkinWordNeTwo {H : Type u_1} [Group H] (f m : ℕ) (x : ℕ → H) : demushkinWordTwoOdd f (2 * m + 1) x = x 0 ^ 2 * demushkinWordNeTwo (2 ^ f) (2 * m) fun (i : ℕ) => x (i + 1)

The odd word x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{2m}, x_{2m+1}) on 2m + 1 letters is x₁² times the q ≠ 2 word x₂^{2^f} (x₂, x₃) ⋯ (x_{2m}, x_{2m+1}) on the 2m letters x₂, …, x_{2m+1}, read on the tuple shifted by one.

theorem TauCeti.demushkinWordTwoOddTop_eq_sq_mul_demushkinWordNeTwo {H : Type u_1} [Group H] (m : ℕ) (x : ℕ → H) : demushkinWordTwoOddTop (2 * m + 1) x = x 0 ^ 2 * demushkinWordNeTwo 0 (2 * m) fun (i : ℕ) => x (i + 1)

The odd word at level f = ∞, x₁² (x₂, x₃) ⋯ (x_{2m}, x_{2m+1}) on 2m + 1 letters, is x₁² times the q ≠ 2 word at q = 0, (x₂, x₃) ⋯ (x_{2m}, x_{2m+1}), on the 2m letters x₂, …, x_{2m+1}, read on the tuple shifted by one.

def TauCeti.demushkinWordTwoEven {H : Type u_1} [Group H] (a f n : ℕ) (x : ℕ → H) : H

The q = 2, n even normal-form word x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), on an arbitrary tuple x : ℕ → H, with x 0 playing the role of x₁. The exponent 2 + a is a natural number standing for Labute's 2 + α, α ∈ 4ℤ₂: on an arbitrary group only natural powers make sense, and no normal form is lost, because the presented pro-2 group is determined up to isomorphism by n and the image of its orientation (Labute, Theorem 2), which depends on α only through v₂(α): it is {±1} × U^(f) for v₂(α) ≥ f and U^[v₂(α)] otherwise (corollary to Labute's Theorem 4), so a = 0 and a = 2^g with 2 ≤ g < f already realize every class. The word has n / 2 - 1 commutator factors after (x₁, x₂).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.demushkinWordTwoEven_def {H : Type u_1} [Group H] (a f n : ℕ) (x : ℕ → H) : demushkinWordTwoEven a f n x = x 0 ^ (2 + a) * labuteComm (x 0) (x 1) * x 2 ^ 2 ^ f * (List.map (fun (i : ℕ) => labuteComm (x (2 * i + 2)) (x (2 * i + 3))) (List.range (n / 2 - 1))).prod

The defining equation of TauCeti.demushkinWordTwoEven.

def TauCeti.demushkinWordTwoRankTwo {H : Type u_1} [Group H] (a : ℕ) (x : ℕ → H) : H

The q = 2 normal-form word of rank two, x₁^{2+a} (x₁, x₂), on an arbitrary tuple x : ℕ → H, with x 0 playing the role of x₁. It is the n = 2 member of the even family with the factor x₃^{2^f} absent, Labute's level f = ∞, so it carries no level: on a tuple with x 2 = 1 it agrees with demushkinWordTwoEven a f 2 x for every f (TauCeti.demushkinWordTwoEven_two).

Equations

• TauCeti.demushkinWordTwoRankTwo a x = x 0 ^ (2 + a) * TauCeti.labuteComm (x 0) (x 1)

theorem TauCeti.demushkinWordTwoRankTwo_def {H : Type u_1} [Group H] (a : ℕ) (x : ℕ → H) : demushkinWordTwoRankTwo a x = x 0 ^ (2 + a) * labuteComm (x 0) (x 1)

The defining equation of TauCeti.demushkinWordTwoRankTwo.

@[simp]

theorem TauCeti.demushkinWordTwoEven_two {H : Type u_1} [Group H] (a f : ℕ) (x : ℕ → H) (hx : x 2 = 1) : demushkinWordTwoEven a f 2 x = demushkinWordTwoRankTwo a x

At rank 2 the even word is the rank-two word: the factor x₃^{2^f} is 1 because the third generator is out of range, and the commutator product beyond (x₁, x₂) is empty.

theorem TauCeti.demushkinWordTwoRankTwo_eq_demushkinWordNeTwo {H : Type u_1} [Group H] (a : ℕ) (x : ℕ → H) : demushkinWordTwoRankTwo a x = demushkinWordNeTwo (2 + a) 2 x

The rank-two word x₁^{2+a} (x₁, x₂) is the q ≠ 2 word at q = 2 + a on two generators, where that word has the single commutator factor (x₁, x₂): Labute's level f = ∞ of the even family at rank two is the q ≠ 2 form with q = 2 + α.

theorem TauCeti.demushkinWordNeTwo_mem {H : Type u_1} [Group H] {N : Subgroup H} [N.Normal] (q n : ℕ) {x : ℕ → H} (h₀ : x 0 ^ q ∈ N) (hx : ∀ i < n / 2, x (2 * i) ∈ N) : demushkinWordNeTwo q n x ∈ N

The q ≠ 2 word lies in a normal subgroup N as soon as its power factor x₁^q and the left entries x₁, x₃, …, x_{2m-1} of its m = n / 2 commutator factors do: a commutator with left entry in N lies in N.

theorem TauCeti.demushkinWordTwoOdd_mem {H : Type u_1} [Group H] {N : Subgroup H} [N.Normal] (f n : ℕ) {x : ℕ → H} (h₀ : x 0 ^ 2 ∈ N) (h₁ : x 1 ^ 2 ^ f ∈ N) (hx : ∀ i < n / 2, x (2 * i + 1) ∈ N) : demushkinWordTwoOdd f n x ∈ N

The q = 2, n odd word lies in a normal subgroup N as soon as its power factors x₁², x₂^{2^f} and the left entries x₂, x₄, …, x_{2m} of its m = n / 2 commutator factors do: a commutator with left entry in N lies in N.

theorem TauCeti.demushkinWordTwoOddTop_mem {H : Type u_1} [Group H] {N : Subgroup H} [N.Normal] (n : ℕ) {x : ℕ → H} (h₀ : x 0 ^ 2 ∈ N) (hx : ∀ i < n / 2, x (2 * i + 1) ∈ N) : demushkinWordTwoOddTop n x ∈ N

The q = 2, n odd word at level f = ∞ lies in a normal subgroup N as soon as its power factor x₁² and the left entries x₂, x₄, …, x_{2m} of its m = n / 2 commutator factors do: a commutator with left entry in N lies in N.

theorem TauCeti.demushkinWordTwoEven_mem {H : Type u_1} [Group H] {N : Subgroup H} [N.Normal] (a f n : ℕ) {x : ℕ → H} (h₀ : x 0 ∈ N) (h₂ : x 2 ^ 2 ^ f ∈ N) (hx : ∀ i < n / 2 - 1, x (2 * i + 2) ∈ N) : demushkinWordTwoEven a f n x ∈ N

The q = 2, n even word lies in a normal subgroup N as soon as x₁, the left entry of its first commutator (x₁, x₂), its power factor x₃^{2^f} and the left entries x₃, x₅, …, x_{2m-1} of its m - 1 = n / 2 - 1 further commutator factors do: a commutator with left entry in N lies in N. For n ≤ 3 there is no further commutator, and the last hypothesis is vacuous.

theorem TauCeti.demushkinWordTwoRankTwo_mem {H : Type u_1} [Group H] {N : Subgroup H} [N.Normal] (a : ℕ) {x : ℕ → H} (h₀ : x 0 ∈ N) : demushkinWordTwoRankTwo a x ∈ N

The rank-two q = 2 word lies in a normal subgroup N as soon as x₁, the left entry of its commutator (x₁, x₂), does.

@[simp]

theorem TauCeti.map_demushkinWordNeTwo {H : Type u_1} [Group H] {K : Type u_2} {F : Type u_3} [Group K] [FunLike F H K] [MonoidHomClass F H K] (φ : F) (q n : ℕ) (x : ℕ → H) : φ (demushkinWordNeTwo q n x) = demushkinWordNeTwo q n (⇑φ ∘ x)

A homomorphism reads the q ≠ 2 word on the image tuple.

@[simp]

theorem TauCeti.map_demushkinWordTwoOdd {H : Type u_1} [Group H] {K : Type u_2} {F : Type u_3} [Group K] [FunLike F H K] [MonoidHomClass F H K] (φ : F) (f n : ℕ) (x : ℕ → H) : φ (demushkinWordTwoOdd f n x) = demushkinWordTwoOdd f n (⇑φ ∘ x)

A homomorphism reads the q = 2, n odd word on the image tuple.

@[simp]

theorem TauCeti.map_demushkinWordTwoOddTop {H : Type u_1} [Group H] {K : Type u_2} {F : Type u_3} [Group K] [FunLike F H K] [MonoidHomClass F H K] (φ : F) (n : ℕ) (x : ℕ → H) : φ (demushkinWordTwoOddTop n x) = demushkinWordTwoOddTop n (⇑φ ∘ x)

A homomorphism reads the q = 2, n odd word at level f = ∞ on the image tuple.

@[simp]

theorem TauCeti.map_demushkinWordTwoEven {H : Type u_1} [Group H] {K : Type u_2} {F : Type u_3} [Group K] [FunLike F H K] [MonoidHomClass F H K] (φ : F) (a f n : ℕ) (x : ℕ → H) : φ (demushkinWordTwoEven a f n x) = demushkinWordTwoEven a f n (⇑φ ∘ x)

A homomorphism reads the q = 2, n even word on the image tuple.

@[simp]

theorem TauCeti.map_demushkinWordTwoRankTwo {H : Type u_1} [Group H] {K : Type u_2} {F : Type u_3} [Group K] [FunLike F H K] [MonoidHomClass F H K] (φ : F) (a : ℕ) (x : ℕ → H) : φ (demushkinWordTwoRankTwo a x) = demushkinWordTwoRankTwo a (⇑φ ∘ x)

A homomorphism reads the rank-two q = 2 word on the image tuple.

@[simp]

theorem TauCeti.demushkinWordNeTwo_eq_of_commGroup {A : Type u_4} [CommGroup A] (q n : ℕ) (x : ℕ → A) : demushkinWordNeTwo q n x = x 0 ^ q

In a commutative group the q ≠ 2 word is x₁^q.

@[simp]

theorem TauCeti.demushkinWordTwoOdd_eq_of_commGroup {A : Type u_4} [CommGroup A] (f n : ℕ) (x : ℕ → A) : demushkinWordTwoOdd f n x = x 0 ^ 2 * x 1 ^ 2 ^ f

In a commutative group the q = 2, n odd word is x₁² x₂^{2^f}.

@[simp]

theorem TauCeti.demushkinWordTwoOddTop_eq_of_commGroup {A : Type u_4} [CommGroup A] (n : ℕ) (x : ℕ → A) : demushkinWordTwoOddTop n x = x 0 ^ 2

In a commutative group the q = 2, n odd word at level f = ∞ is x₁².

@[simp]

theorem TauCeti.demushkinWordTwoEven_eq_of_commGroup {A : Type u_4} [CommGroup A] (a f n : ℕ) (x : ℕ → A) : demushkinWordTwoEven a f n x = x 0 ^ (2 + a) * x 2 ^ 2 ^ f

In a commutative group the q = 2, n even word is x₁^{2+a} x₃^{2^f}.

@[simp]

theorem TauCeti.demushkinWordTwoRankTwo_eq_of_commGroup {A : Type u_4} [CommGroup A] (a : ℕ) (x : ℕ → A) : demushkinWordTwoRankTwo a x = x 0 ^ (2 + a)

In a commutative group the rank-two q = 2 word is x₁^{2+a}.

theorem TauCeti.map_demushkinWordNeTwo_eq_one {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (q n : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ q = 1) : χ (demushkinWordNeTwo q n x) = 1

A character into a commutative group whose value on x₁ has trivial q-th power kills the q ≠ 2 word.

theorem TauCeti.map_demushkinWordTwoOdd_eq_one {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (f n : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ 2 = 1) (h₁ : χ (x 1) ^ 2 ^ f = 1) : χ (demushkinWordTwoOdd f n x) = 1

A character into a commutative group whose value on x₁ squares to 1 and whose value on x₂ has trivial 2^f-th power kills the q = 2, n odd word.

theorem TauCeti.map_demushkinWordTwoOddTop_eq_one {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (n : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ 2 = 1) : χ (demushkinWordTwoOddTop n x) = 1

A character into a commutative group whose value on x₁ squares to 1 kills the q = 2, n odd word at level f = ∞.

theorem TauCeti.map_demushkinWordTwoEven_eq_one {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (a f n : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ (2 + a) = 1) (h₂ : χ (x 2) ^ 2 ^ f = 1) : χ (demushkinWordTwoEven a f n x) = 1

A character into a commutative group whose value on x₁ has trivial (2 + a)-th power and whose value on x₃ has trivial 2^f-th power kills the q = 2, n even word.

theorem TauCeti.map_demushkinWordTwoRankTwo_eq_one {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (a : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ (2 + a) = 1) : χ (demushkinWordTwoRankTwo a x) = 1

A character into a commutative group whose value on x₁ has trivial (2 + a)-th power kills the rank-two q = 2 word.

theorem TauCeti.demushkinWordNeTwo_mem_ker {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (q n : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ q = 1) : demushkinWordNeTwo q n x ∈ (↑χ).ker

The q ≠ 2 word lies in the kernel of a character into a commutative group whose value on x₁ has trivial q-th power.

theorem TauCeti.demushkinWordTwoOdd_mem_ker {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (f n : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ 2 = 1) (h₁ : χ (x 1) ^ 2 ^ f = 1) : demushkinWordTwoOdd f n x ∈ (↑χ).ker

The q = 2, n odd word lies in the kernel of a character into a commutative group whose value on x₁ squares to 1 and whose value on x₂ has trivial 2^f-th power.

theorem TauCeti.demushkinWordTwoOddTop_mem_ker {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (n : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ 2 = 1) : demushkinWordTwoOddTop n x ∈ (↑χ).ker

The q = 2, n odd word at level f = ∞ lies in the kernel of a character into a commutative group whose value on x₁ squares to 1.

theorem TauCeti.demushkinWordTwoEven_mem_ker {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (a f n : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ (2 + a) = 1) (h₂ : χ (x 2) ^ 2 ^ f = 1) : demushkinWordTwoEven a f n x ∈ (↑χ).ker

The q = 2, n even word lies in the kernel of a character into a commutative group whose value on x₁ has trivial (2 + a)-th power and whose value on x₃ has trivial 2^f-th power.

theorem TauCeti.demushkinWordTwoRankTwo_mem_ker {A : Type u_4} [CommGroup A] {G : Type u_5} [Group G] {F' : Type u_6} [FunLike F' G A] [MonoidHomClass F' G A] (χ : F') (a : ℕ) {x : ℕ → G} (h₀ : χ (x 0) ^ (2 + a) = 1) : demushkinWordTwoRankTwo a x ∈ (↑χ).ker

The rank-two q = 2 word lies in the kernel of a character into a commutative group whose value on x₁ has trivial (2 + a)-th power.

The generators of a normal-form presentation satisfy the relation

@[simp]

theorem TauCeti.demushkinWordNeTwo_presentedProPGen_eq_one (p q n : ℕ) : demushkinWordNeTwo q n (presentedProPGen p n {demushkinWordNeTwo q n (freeProPGen p n)}) = 1

The ℕ-indexed generators of the q ≠ 2 normal-form presentation satisfy its defining relation x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) = 1.

@[simp]

theorem TauCeti.demushkinWordTwoOdd_presentedProPGen_eq_one (p f n : ℕ) : demushkinWordTwoOdd f n (presentedProPGen p n {demushkinWordTwoOdd f n (freeProPGen p n)}) = 1

The ℕ-indexed generators of the q = 2, n odd normal-form presentation satisfy its defining relation x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) = 1.

@[simp]

theorem TauCeti.demushkinWordTwoOddTop_presentedProPGen_eq_one (p n : ℕ) : demushkinWordTwoOddTop n (presentedProPGen p n {demushkinWordTwoOddTop n (freeProPGen p n)}) = 1

The ℕ-indexed generators of the q = 2, n odd normal-form presentation at level f = ∞ satisfy its defining relation x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) = 1.

@[simp]

theorem TauCeti.demushkinWordTwoEven_presentedProPGen_eq_one (p a f n : ℕ) : demushkinWordTwoEven a f n (presentedProPGen p n {demushkinWordTwoEven a f n (freeProPGen p n)}) = 1

The ℕ-indexed generators of the q = 2, n even normal-form presentation satisfy its defining relation x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) = 1.

@[simp]

theorem TauCeti.demushkinWordTwoRankTwo_presentedProPGen_eq_one (p a : ℕ) : demushkinWordTwoRankTwo a (presentedProPGen p 2 {demushkinWordTwoRankTwo a (freeProPGen p 2)}) = 1

The ℕ-indexed generators of the rank-two q = 2 normal-form presentation satisfy its defining relation x₁^{2+a} (x₁, x₂) = 1.

The words lie in the Frattini subgroup

theorem TauCeti.demushkinWordNeTwo_mem_proPFrattini {H : Type u_1} [Group H] [TopologicalSpace H] {p q : ℕ} (hp : Nat.Prime p) (hq : p ∣ q) (n : ℕ) (x : ℕ → H) : demushkinWordNeTwo q n x ∈ proPFrattini p H

For p ∣ q, the q ≠ 2 word lies in the pro-p Frattini subgroup: x₁^q is a p-th power and the remaining factors are commutators. This covers q = 0.

theorem TauCeti.demushkinWordTwoOdd_mem_proPFrattini {H : Type u_1} [Group H] [TopologicalSpace H] {f : ℕ} (hf : 0 < f) (n : ℕ) (x : ℕ → H) : demushkinWordTwoOdd f n x ∈ proPFrattini 2 H

For f ≥ 1, the q = 2, n odd word lies in the pro-2 Frattini subgroup: x₁² and x₂^{2^f} are squares and the remaining factors are commutators.

theorem TauCeti.demushkinWordTwoOddTop_mem_proPFrattini {H : Type u_1} [Group H] [TopologicalSpace H] (n : ℕ) (x : ℕ → H) : demushkinWordTwoOddTop n x ∈ proPFrattini 2 H

The q = 2, n odd word at level f = ∞ lies in the pro-2 Frattini subgroup: x₁² is a square and the remaining factors are commutators.

theorem TauCeti.demushkinWordTwoEven_mem_proPFrattini {H : Type u_1} [Group H] [TopologicalSpace H] {a f : ℕ} (ha : 2 ∣ a) (hf : 0 < f) (n : ℕ) (x : ℕ → H) : demushkinWordTwoEven a f n x ∈ proPFrattini 2 H

For a even and f ≥ 1, the q = 2, n even word lies in the pro-2 Frattini subgroup: x₁^{2+a} and x₃^{2^f} are squares and the remaining factors are commutators.

theorem TauCeti.demushkinWordTwoRankTwo_mem_proPFrattini {H : Type u_1} [Group H] [TopologicalSpace H] {a : ℕ} (ha : 2 ∣ a) (x : ℕ → H) : demushkinWordTwoRankTwo a x ∈ proPFrattini 2 H

For a even, the rank-two q = 2 word lies in the pro-2 Frattini subgroup: x₁^{2+a} is a square and (x₁, x₂) is a commutator.

The normal-form presentations are minimal

theorem TauCeti.topologicalGeneratorRankNat_presentedProP_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {q : ℕ} (hq : p ∣ q) (n : ℕ) : topologicalGeneratorRankNat (presentedProP p (Fin n) {demushkinWordNeTwo q n (freeProPGen p n)}) ⋯ = n

The q ≠ 2 normal-form presentation is minimal: for p ∣ q, the pro-p group presented on n generators by x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) has topological generator rank n.

theorem TauCeti.topologicalGeneratorRankNat_presentedProP_demushkinWordTwoOdd {f : ℕ} (hf : 0 < f) (n : ℕ) : topologicalGeneratorRankNat (presentedProP 2 (Fin n) {demushkinWordTwoOdd f n (freeProPGen 2 n)}) ⋯ = n

The q = 2, n odd normal-form presentation is minimal: for f ≥ 1, the pro-2 group presented on n generators by x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) has topological generator rank n.

theorem TauCeti.topologicalGeneratorRankNat_presentedProP_demushkinWordTwoOddTop (n : ℕ) : topologicalGeneratorRankNat (presentedProP 2 (Fin n) {demushkinWordTwoOddTop n (freeProPGen 2 n)}) ⋯ = n

The q = 2, n odd normal-form presentation at level f = ∞ is minimal: the pro-2 group presented on n generators by x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) has topological generator rank n.

theorem TauCeti.topologicalGeneratorRankNat_presentedProP_demushkinWordTwoEven {a f : ℕ} (ha : 2 ∣ a) (hf : 0 < f) (n : ℕ) : topologicalGeneratorRankNat (presentedProP 2 (Fin n) {demushkinWordTwoEven a f n (freeProPGen 2 n)}) ⋯ = n

The q = 2, n even normal-form presentation is minimal: for a even and f ≥ 1, the pro-2 group presented on n generators by x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) has topological generator rank n.

theorem TauCeti.topologicalGeneratorRankNat_presentedProP_demushkinWordTwoRankTwo {a : ℕ} (ha : 2 ∣ a) : topologicalGeneratorRankNat (presentedProP 2 (Fin 2) {demushkinWordTwoRankTwo a (freeProPGen 2 2)}) ⋯ = 2

The rank-two q = 2 normal-form presentation is minimal: for a even, the pro-2 group presented on two generators by x₁^{2+a} (x₁, x₂) has topological generator rank 2.