Finite quotients of one-relator groups

DefinitionFinite soluble groups as images of one-relator groups (Kourovka 18.75)#✓fully proved

The statement, posed by A. Yu. Olshanskii, that every finite soluble group \(G\) has a natural number \(d\) such that for every element \(w\) of the free group on \(x_1, \dots, x_d\) there is a surjective homomorphism from the one-relator group \(\langle x_1, \dots, x_d \mid w \rangle\) onto \(G\).

def solubleGroupImageOfOneRelatorGroups : Prop :=
  ∀ (G : Type) [Group G] [Finite G], Group.IsSolvable G →
    ∃ d : ℕ, ∀ w : FreeGroup (Fin d),
      ∃ f : PresentedGroup ({w} : Set (FreeGroup (Fin d))) →* G, Function.Surjective f

Used by 1

Used byFinite soluble groups are images of one-relator groups

TheoremFinite soluble groups are images of one-relator groups#●ready to prove

Every finite soluble group \(G\) has a natural number \(d\) such that for every element \(w\) of the free group on \(x_1, \dots, x_d\) there is a surjective homomorphism from the one-relator group \(\langle x_1, \dots, x_d \mid w \rangle\) onto \(G\). That is, Kourovka Problem 18.75 has a positive answer.

Resolved true: the Kourovka Archive answers 18.75 "Yes, it does" (N. Nikolov and D. Segal, 2007).

public theorem_wanted solubleGroupImageOfOneRelatorGroups_holds :
    solubleGroupImageOfOneRelatorGroups

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.75 (A. Yu. Olshanskii); resolution: N. Nikolov and D. Segal, Bull. London Math. Soc. 39 (2007), no. 2, 209-213, Kourovka Archive, Problem 18.75: Yes, it does, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesFinite soluble groups as images of one-relator groups (Kourovka 18.75)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.