Engel conditions on involutions

DefinitionInvolution-generated 2-groups with the Engel condition on involutions#✓fully proved

A group \(G\) has this property when every element of \(G\) has order a power of \(2\), \(G\) is generated by its involutions, and \([[x, u], u] = 1\) for every \(x \in G\) and every involution \(u \in G\), where \([x, u] = x^{-1} u^{-1} x u\).

def IsInvolutionEngelTwoGroup (G : Type) [Group G] : Prop :=
  IsPGroup 2 G ∧ Subgroup.closure {u : G | orderOf u = 2} = ⊤ ∧
    ∀ x u : G, orderOf u = 2 →
      (x⁻¹ * u⁻¹ * x * u)⁻¹ * u⁻¹ * (x⁻¹ * u⁻¹ * x * u) * u = 1
Used by 1

DefinitionKourovka Problem 18.57 on the derived length of involution-generated 2-groups#✓fully proved

The proposition (Kourovka 18.57, D. V. Lytkina) that there is a natural number \(d\) such that \(G^{(d)} = 1\) for every finite group \(G\) in which every element has order a power of \(2\), which is generated by its involutions, and in which \([[x, u], u] = 1\) for every \(x \in G\) and every involution \(u \in G\); here \([x, u] = x^{-1} u^{-1} x u\) and \(G^{(d)}\) is the \(d\)-th term of the derived series of \(G\).

def involutionEngelTwoGroupsBoundedDerivedLength : Prop :=
  ∃ d : ℕ, ∀ (G : Type) [Group G] [Finite G], IsInvolutionEngelTwoGroup G → derivedSeries G d = ⊥
Uses 1 · Used by 1

TheoremNegative answer to Kourovka Problem 18.57#●ready to prove

There is no natural number \(d\) such that \(G^{(d)} = 1\) for every finite group \(G\) in which every element has order a power of \(2\), which is generated by its involutions, and in which \([[x, u], u] = 1\) for every \(x \in G\) and every involution \(u \in G\); here \([x, u] = x^{-1} u^{-1} x u\) and \(G^{(d)}\) is the \(d\)-th term of the derived series of \(G\). Thus the derived length of such groups is unbounded.

public theorem_wanted involutionEngelTwoGroupsBoundedDerivedLength_refuted :
    ¬ involutionEngelTwoGroupsBoundedDerivedLength
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 18.57 (D. V. Lytkina); resolution: A. Abdollahi, J. Group Theory 18 (2015), no. 1, 111-114, Kourovka Archive, Problem 18.57: No, it is not, https://arxiv.org/abs/1401.0300v49.
Uses 1
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.