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
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 = ⊥
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
WantedExt/GroupTheory/InvolutionEngelTwoGroupDerivedLengthKourovka18Problem57Wanted.lean:39
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
def involutionEngelTwoGroupsBoundedDerivedLength : Prop :=
∃ d : ℕ, ∀ (G : Type) [Group G] [Finite G], IsInvolutionEngelTwoGroup G → derivedSeries G d = ⊥
WantedExt/GroupTheory/InvolutionEngelTwoGroupDerivedLengthKourovka18Problem57Wanted.lean:46
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.