Generator number of almost simple groups

DefinitionRelative generator number#✓fully proved

For subgroups \(G\) and \(N\) of a group \(A\), the relative generator number of \(G\) modulo \(N\) is the least \(k\) such that some \(k\) elements of \(A\) together with \(N\) generate \(G\), and \(0\) if no finite set of elements does. For a normal subgroup \(N \le G\) with \(G / N\) finitely generated it is \(d(G / N)\), the minimal number of generators of \(G / N\).

noncomputable def relGenNum {A : Type*} [Group A] (G N : Subgroup A) : ℕ :=
  sInf {k | ∃ T : Finset A, T.card = k ∧ Subgroup.closure (T : Set A) ⊔ N = G}

Used by 1

Used byThe generator-number formula for almost simple groups (Kourovka 11.27)

DefinitionThe generator-number formula for almost simple groups (Kourovka 11.27)#✓fully proved

The proposition that for every finite non-abelian simple group \(S\), identified with its inner automorphism group \(\mathrm{Inn}(S) \le \mathrm{Aut}(S)\), and every subgroup \(G\) of \(\mathrm{Aut}(S)\) containing \(S\), \(d(G) = \max(2, d(G / S))\). Here \(d(G)\) is the minimal number of generators of \(G\), and \(d(G / S)\), the minimal number of generators of \(G / S\), is taken to be the least number of elements of \(G\) that together with \(S\) generate \(G\).

def almostSimpleGenNumEq : Prop :=
  ∀ (S : Type) [Group S] [Finite S], IsSimpleGroup S → (∃ a b : S, a * b ≠ b * a) →
    ∀ G : Subgroup (MulAut S), (MulAut.conj : S →* MulAut S).range ≤ G →
      Group.rank G = max 2 (relGenNum G (MulAut.conj : S →* MulAut S).range)

Uses 1 · Used by 1

Statement usesRelative generator number

Used byGenerator number of almost simple groups (Kourovka 11.27)

DefinitionThe 3-generator bound for almost simple groups (Kourovka 11.27)#✓fully proved

The proposition that for every finite non-abelian simple group \(S\), identified with its inner automorphism group \(\mathrm{Inn}(S) \le \mathrm{Aut}(S)\), every subgroup \(G\) of \(\mathrm{Aut}(S)\) containing \(S\) is generated by at most \(3\) elements.

def almostSimpleGenNumLeThree : Prop :=
  ∀ (S : Type) [Group S] [Finite S], IsSimpleGroup S → (∃ a b : S, a * b ≠ b * a) →
    ∀ G : Subgroup (MulAut S), (MulAut.conj : S →* MulAut S).range ≤ G → Group.rank G ≤ 3

Used by 1

Used byAlmost simple groups are generated by 3 elements (Kourovka 11.27)

TheoremGenerator number of almost simple groups (Kourovka 11.27)#●ready to prove

Let \(S\) be a finite non-abelian simple group, identified with its inner automorphism group \(\mathrm{Inn}(S) \le \mathrm{Aut}(S)\). For every subgroup \(G\) of \(\mathrm{Aut}(S)\) containing \(S\), \(d(G) = \max(2, d(G / S))\), where \(d(G)\) is the minimal number of generators of \(G\) and \(d(G / S)\), the minimal number of generators of \(G / S\), is taken to be the least number of elements of \(G\) that together with \(S\) generate \(G\).

Dalla Volta and Lucchini proved this using the classification of finite simple groups.

public theorem_wanted almostSimpleGenNumEq_holds : almostSimpleGenNumEq

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 11.27 (K. Gruenberg); resolution: F. Dalla Volta and A. Lucchini, J. Algebra 178, no. 1 (1995), 194-223, Kourovka Archive, Problem 11.27: "The number d(G) is found (mod CFSG) for every such a group G. In particular, d(G) = max {2, d(G/S)} and d(G) ≤ 3", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesThe generator-number formula for almost simple groups (Kourovka 11.27)

TheoremAlmost simple groups are generated by 3 elements (Kourovka 11.27)#●ready to prove

Let \(S\) be a finite non-abelian simple group, identified with its inner automorphism group \(\mathrm{Inn}(S) \le \mathrm{Aut}(S)\). Every subgroup \(G\) of \(\mathrm{Aut}(S)\) containing \(S\) is generated by at most \(3\) elements.

Dalla Volta and Lucchini proved this using the classification of finite simple groups.

public theorem_wanted almostSimpleGenNumLeThree_holds : almostSimpleGenNumLeThree

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 11.27 (K. Gruenberg); resolution: F. Dalla Volta and A. Lucchini, J. Algebra 178, no. 1 (1995), 194-223, Kourovka Archive, Problem 11.27: "The number d(G) is found (mod CFSG) for every such a group G. In particular, d(G) = max {2, d(G/S)} and d(G) ≤ 3", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesThe 3-generator bound for almost simple groups (Kourovka 11.27)

DefinitionAlmost simple groups#✓fully proved

A group \(G\) is almost simple when there is a nonabelian finite simple group \(S\) such that \(G\) is isomorphic to a subgroup \(A\) of the automorphism group \(\mathrm{Aut}(S)\) that contains the inner automorphism group \(\mathrm{Inn}(S)\).

def IsAlmostSimple (G : Type u) [Group G] : Prop :=
  ∃ (S : Type u) (groupStructure : Group S) (finiteS : Finite S)
      (simpleS : IsSimpleGroup S),
    letI := groupStructure
    letI := finiteS
    letI := simpleS
    ¬IsMulCommutative S ∧
      ∃ A : Subgroup (MulAut S),
        MonoidHom.range (MulAut.conj : S →* MulAut S) ≤ A ∧
          Nonempty (G ≃* A)

4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.