Rank of a group generated by two subgroups

DefinitionRibes' question on generator counts (Kourovka 12.71)#✓fully proved

Write \(d(X)\) for the minimal number of generators of a finite group \(X\). This is the proposition that for all finite groups \(A\) and \(B\) there are a finite group \(G\) and subgroups \(H, K \le G\) with \(H \cong A\), \(K \cong B\) and \(\langle H, K \rangle = G\) such that \(d(G) = d(A) + d(B)\).

def rankAdditiveGeneration : Prop :=
  ∀ (A B : Type) [Group A] [Finite A] [Group B] [Finite B],
    ∃ (G : Type) (_ : Group G) (_ : Finite G) (H K : Subgroup G),
      Nonempty (H ≃* A) ∧ Nonempty (K ≃* B) ∧ H ⊔ K = ⊤ ∧
        Group.rank G = Group.rank A + Group.rank B

Used by 1

Used byGenerator counts of groups generated by two subgroups are not always additive (Kourovka 12.71)

TheoremGenerator counts of groups generated by two subgroups are not always additive (Kourovka 12.71)#●ready to prove

Write \(d(X)\) for the minimal number of generators of a finite group \(X\). There are finite groups \(A\) and \(B\) such that for every finite group \(G\) and all subgroups \(H, K \le G\) with \(H \cong A\), \(K \cong B\) and \(\langle H, K \rangle = G\), we have \(d(G) \ne d(A) + d(B)\).

Resolved false: the Kourovka Archive answers 12.71 "No, not always" (A. Lucchini, 2001). Since \(d(G) \le d(A) + d(B)\) always holds for such \(G\), every finite group generated by subgroups isomorphic to \(A\) and \(B\) needs fewer than \(d(A) + d(B)\) generators (Kovács and Sim had shown this within soluble groups).

public theorem_wanted rankAdditiveGeneration_refuted : ¬ rankAdditiveGeneration

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 12.71 (L. Ribes); resolution: A. Lucchini, J. Group Theory 4 (2001), no. 1, 53-58, Kourovka Archive, Problem 12.71: No, not always.

Uses 1

Statement usesRibes' question on generator counts (Kourovka 12.71)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.