Alperin groups

DefinitionAlperin group#✓fully proved

A group \(G\) is an Alperin group when, for all \(x, y \in G\), the derived subgroup \([H, H]\) of the subgroup \(H = \langle x, y \rangle\) generated by \(x\) and \(y\) is cyclic.

def IsAlperinGroup (G : Type) [Group G] : Prop :=
  ∀ x y : G, IsCyclic (⁅Subgroup.closure {x, y}, Subgroup.closure {x, y}⁆ : Subgroup G)

Used by 1

Used byKourovka Problem 18.33 on the derived length of finite Alperin groups

DefinitionKourovka Problem 18.33 on the derived length of finite Alperin groups#✓fully proved

This proposition asserts that every finite Alperin group \(G\) has derived length at most \(6\), that is, its sixth derived subgroup \(G^{(6)}\) is trivial. Here \(G\) is an Alperin group when, for all \(x, y \in G\), the derived subgroup of the subgroup \(\langle x, y \rangle\) generated by \(x\) and \(y\) is cyclic.

Problem 18.33 (B. M. Veretennikov) asks whether such a bound exists; \(6\) is the bound given in the answer.

def alperinGroupDerivedLengthAtMostSix : Prop :=
  ∀ (G : Type) [Group G] [Finite G], IsAlperinGroup G → derivedSeries G 6 = ⊥

Uses 1 · Used by 1

Statement usesAlperin group

Used byFinite Alperin groups have derived length at most six

TheoremFinite Alperin groups have derived length at most six#●ready to prove

Let \(G\) be a finite group in which, for all \(x, y \in G\), the derived subgroup of the subgroup \(\langle x, y \rangle\) generated by \(x\) and \(y\) is cyclic (an Alperin group). Then the sixth derived subgroup \(G^{(6)}\) of \(G\) is trivial, that is, \(G\) has derived length at most \(6\).

public theorem_wanted alperinGroupDerivedLengthAtMostSix_holds : alperinGroupDerivedLengthAtMostSix

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.33 (B. M. Veretennikov); resolution: P. Longobardi, M. Maj and H. Smith, Rend. Sem. Mat. Univ. Padova 115 (2006), 29-40; B. Wilkens, J. Group Theory 17 (2014), no. 1, 151-174, Kourovka Archive, Problem 18.33: Yes, it is at most 6: finite Alperin groups of odd order are metabelian and finite Alperin groups are supersoluble (Longobardi-Maj-Smith), so the elements of odd order form a metabelian normal subgroup, and finite Alperin 2-groups have derived length at most 4 (Wilkens), https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 18.33 on the derived length of finite Alperin groups

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.