Spread of a group

DefinitionSpread at least \(k\)#✓fully proved

A group \(G\) has spread at least \(k\), for a natural number \(k\), when for every family \(x_1, \dots, x_k\) of nontrivial elements of \(G\), not necessarily distinct, there is an element \(y \in G\) such that the subgroup \(\langle x_i, y \rangle\) generated by \(x_i\) and \(y\) is all of \(G\) for every \(i\).

def HasSpreadAtLeast (G : Type u) [Group G] (k : ℕ) : Prop :=
  ∀ x : Fin k → G, (∀ i, x i ≠ 1) →
    ∃ y : G, ∀ i, Subgroup.closure {x i, y} = ⊤

Used by 1

Used bySpread exactly \(k\)

DefinitionSpread exactly \(k\)#✓fully proved

A group \(G\) has spread exactly \(k\), for a natural number \(k\), when \(G\) has spread at least \(k\) and, for every natural number \(m > k\), \(G\) does not have spread at least \(m\).

def HasSpreadExactly (G : Type u) [Group G] (k : ℕ) : Prop :=
  HasSpreadAtLeast G k ∧ ∀ m : ℕ, m > k → ¬ HasSpreadAtLeast G m

Uses 1 · Used by 1

Statement usesSpread at least \(k\)

Used byExistence of a group of spread exactly one (Kourovka 21.38)

DefinitionExistence of a group of spread exactly one (Kourovka 21.38)#✓fully proved

The conjecture that there exists a group of spread exactly \(1\).

def conjecture : Prop :=
  ∃ (G : Type u) (_ : Group G), HasSpreadExactly G 1

Uses 1 · Used by 1

Statement usesSpread exactly \(k\)

Used byThere is a group of spread exactly one

TheoremThere is a group of spread exactly one#●ready to prove

There exists a group \(G\) of spread exactly \(1\): for every nontrivial \(x \in G\) there is \(y \in G\) with \(\langle x, y \rangle = G\), but for every natural number \(m > 1\) there are nontrivial elements \(x_1, \dots, x_m \in G\) such that no single \(y \in G\) satisfies \(\langle x_i, y \rangle = G\) for all \(i\). This answers Kourovka Problem 21.38 affirmatively.

The Nilradical note A group of spread one (17 September 2026, Kourovka Notebook site), Theorem 1, shows that the subgroup \(\{f \in F : f'(0^+) = f'(1^-)\}\) of Thompson's group \(F\) is infinite and has spread exactly one. The note is not refereed; the Kourovka Notebook (arXiv:1401.0300v49) marks Problem 21.38 solved (AI solution confirmed by S. Corson).

public theorem_wanted conjecture_holds : conjecture

Sources

• Nilradical, A group of spread one (note of 17 September 2026, Kourovka Notebook site), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/nilradical-kourovka-21-38.pdf; E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (20 October 2026), Problem 21.38, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesExistence of a group of spread exactly one (Kourovka 21.38)

DefinitionSpread of a group#✓fully proved

Let \(G\) be a group. The spread \(s(G)\) of \(G\) is the supremum in \(\mathbb{N} \cup \{\infty\}\) of the natural numbers \(k\) such that for any non-trivial elements \(x_1, \dots, x_k\) of \(G\) (not necessarily distinct) there exists \(y \in G\) such that the subgroup \(\langle x_i, y \rangle\) generated by \(x_i\) and \(y\) is all of \(G\) for every \(i\). In particular \(s(G) = \infty\) when there is no largest such \(k\).

noncomputable def s (G : Type*) [Group G] : ℕ∞ :=
  sSup ((↑) '' {k : ℕ | ∀ x : Fin k → G, 1 ∉ Set.range x → ∃ y, ∀ i, Subgroup.closure {x i, y} = ⊤})

Used by 1

Used byBurness–Guralnick–Harper spread theorem

TheoremBurness–Guralnick–Harper spread theorem#●ready to prove

Let \(G\) be a finite group. Then the spread \(s(G)\) is at least \(2\) if and only if every proper quotient of \(G\) is cyclic, that is, \(G/N\) is cyclic for every non-trivial normal subgroup \(N\) of \(G\).

public theorem_wanted theorem_1 (G : Type*) [Group G] [Finite G] :
    s G ≥ 2 ↔ ∀ (N : Subgroup G) [N.Normal] [Nontrivial N], IsCyclic (G ⧸ N)

Sources

• T. C. Burness, R. M. Guralnick, and S. Harper, The spread of a finite group, Annals of Math, 193 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_spread_of_a_finite_group of the lean-eval benchmark.

Uses 1

Statement usesSpread of a group

4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.