Upper composition factors of finitely generated groups

DefinitionComposition factor of a group (via subnormal subgroups)#✓fully proved

For groups \(T\) and \(Q\), \(T\) is a composition factor of \(Q\) when some subnormal subgroup \(H\) of \(Q\) maps onto \(T\), that is, there is a surjective group homomorphism \(H \to T\). Here \(H\) is subnormal in \(Q\) when there is a finite chain of subgroups \(H = H_0 \le H_1 \le \dots \le H_k = Q\) in which each \(H_j\) is normal in \(H_{j+1}\).

For simple \(T\) and finite \(Q\) this is the same as \(T\) occurring as a factor of a composition series of \(Q\) (refine the kernel and the subnormal chain).

def IsCompositionFactor (T Q : Type*) [Group T] [Group Q] : Prop :=
  ∃ H : Subgroup Q, H.IsSubnormal ∧ ∃ f : H →* T, Function.Surjective f

Used by 1

Used byUpper composition factors

DefinitionUpper composition factors#✓fully proved

For groups \(T\) and \(G\), \(T\) is an upper composition factor of \(G\) when it is a composition factor of some finite quotient of \(G\): there are a finite group \(Q\) and a surjective group homomorphism \(G \to Q\) such that \(T\) is a composition factor of \(Q\), that is, \(T\) is a homomorphic image of a subnormal subgroup of \(Q\).

def IsUpperCompositionFactor (T G : Type) [Group T] [Group G] : Prop :=
  ∃ (Q : Type) (_ : Group Q) (_ : Finite Q) (π : G →* Q), Function.Surjective π ∧
    IsCompositionFactor T Q

Uses 1 · Used by 2

Statement usesComposition factor of a group (via subnormal subgroups)

Used byKourovka Problem 11.57, 3-generator form (statement) · Kourovka Problem 11.57, 63-generator form (statement)

DefinitionKourovka Problem 11.57, 63-generator form (statement)#✓fully proved

The statement that for every family \((T_i)_{i \in I}\) of finite non-abelian simple groups there is a group \(G\) generated by \(63\) elements such that a finite simple group \(Q\) is an upper composition factor of \(G\) if and only if \(Q\) is isomorphic to \(T_i\) for some \(i \in I\).

def upperCompositionFactorsAnySet63 : Prop :=
  ∀ (ι : Type) (T : ι → Type) [∀ i, Group (T i)],
    (∀ i, Finite (T i) ∧ IsSimpleGroup (T i) ∧ ∃ a b : T i, a * b ≠ b * a) →
    ∃ (G : Type) (_ : Group G), (∃ s : Fin 63 → G, Subgroup.closure (Set.range s) = ⊤) ∧
      ∀ (Q : Type) [Group Q] [Finite Q], IsSimpleGroup Q →
        (IsUpperCompositionFactor Q G ↔ ∃ i, Nonempty (Q ≃* T i))

Uses 1 · Used by 1

Statement usesUpper composition factors

Used bySegal's theorem on upper composition factors, 63 generators (Kourovka Problem 11.57)

DefinitionKourovka Problem 11.57, 3-generator form (statement)#✓fully proved

The statement that for every family \((T_i)_{i \in I}\) of finite non-abelian simple groups there is a group \(G\) generated by \(3\) elements such that a finite non-abelian simple group \(Q\) is an upper composition factor of \(G\) if and only if \(Q\) is isomorphic to \(T_i\) for some \(i \in I\). Abelian upper composition factors of \(G\) are not restricted.

def nonabelianUpperCompositionFactorsAnySet3 : Prop :=
  ∀ (ι : Type) (T : ι → Type) [∀ i, Group (T i)],
    (∀ i, Finite (T i) ∧ IsSimpleGroup (T i) ∧ ∃ a b : T i, a * b ≠ b * a) →
    ∃ (G : Type) (_ : Group G), (∃ s : Fin 3 → G, Subgroup.closure (Set.range s) = ⊤) ∧
      ∀ (Q : Type) [Group Q] [Finite Q], IsSimpleGroup Q → (∃ a b : Q, a * b ≠ b * a) →
        (IsUpperCompositionFactor Q G ↔ ∃ i, Nonempty (Q ≃* T i))

Uses 1 · Used by 1

Statement usesUpper composition factors

Used bySegal's theorem on upper composition factors, 3 generators (Kourovka Problem 11.57)

TheoremSegal's theorem on upper composition factors, 63 generators (Kourovka Problem 11.57)#●ready to prove

For every family \((T_i)_{i \in I}\) of finite non-abelian simple groups there is a group \(G\) generated by \(63\) elements such that a finite simple group \(Q\) is an upper composition factor of \(G\) (a composition factor of some finite quotient of \(G\)) if and only if \(Q\) is isomorphic to \(T_i\) for some \(i \in I\). In particular, no cyclic group of prime order is an upper composition factor of \(G\).

public theorem_wanted upperCompositionFactorsAnySet63_holds : upperCompositionFactorsAnySet63

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.57 (A. Mann, D. Segal); resolution: D. Segal, Proc. London Math. Soc. (3) 82 (2001), 597-613, Kourovka Archive, Problem 11.57: any set of non-abelian finite simple groups is the set of upper composition factors of a 63-generator group; with abelian upper composition factors allowed, 3 generators suffice, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 11.57, 63-generator form (statement)

TheoremSegal's theorem on upper composition factors, 3 generators (Kourovka Problem 11.57)#●ready to prove

For every family \((T_i)_{i \in I}\) of finite non-abelian simple groups there is a group \(G\) generated by \(3\) elements such that a finite non-abelian simple group \(Q\) is an upper composition factor of \(G\) (a composition factor of some finite quotient of \(G\)) if and only if \(Q\) is isomorphic to \(T_i\) for some \(i \in I\). Abelian upper composition factors of \(G\) are not restricted.

public theorem_wanted nonabelianUpperCompositionFactorsAnySet3_holds :
    nonabelianUpperCompositionFactorsAnySet3

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.57 (A. Mann, D. Segal); resolution: D. Segal, Proc. London Math. Soc. (3) 82 (2001), 597-613, Kourovka Archive, Problem 11.57: any set of non-abelian finite simple groups is the set of upper composition factors of a 63-generator group; with abelian upper composition factors allowed, 3 generators suffice, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 11.57, 3-generator form (statement)

4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.