Finitely presented soluble groups

DefinitionMetanilpotent-by-finite groups#✓fully proved

A group \(G\) is (nilpotent-by-nilpotent)-by-finite when it has a normal subgroup \(M\) of finite index and a normal subgroup \(N\) of \(M\) such that \(N\) and \(M/N\) are both nilpotent.

def IsMetanilpotentByFinite (G : Type) [Group G] : Prop :=
  ∃ M : Subgroup G, M.Normal ∧ M.FiniteIndex ∧
    ∃ N : Subgroup M, ∃ _ : N.Normal, Group.IsNilpotent N ∧ Group.IsNilpotent (M ⧸ N)

Used by 1

Used byGroves's question (Kourovka 16.35)

DefinitionGroves's question (Kourovka 16.35)#✓fully proved

The proposition that every finitely presented soluble group \(G\) is (nilpotent-by-nilpotent)-by-finite, that is, \(G\) has a normal subgroup \(M\) of finite index and a normal subgroup \(N\) of \(M\) such that \(N\) and \(M/N\) are both nilpotent.

def finitelyPresentedSolubleMetanilpotentByFinite : Prop :=
  ∀ (G : Type) [Group G], Group.IsFinitelyPresented G → Group.IsSolvable G →
    IsMetanilpotentByFinite G

Uses 1 · Used by 1

Statement usesMetanilpotent-by-finite groups

Used byGroves's question (Kourovka 16.35) has a negative answer

TheoremGroves's question (Kourovka 16.35) has a negative answer#●ready to prove

Not every finitely presented soluble group is (nilpotent-by-nilpotent)-by-finite: there is a finitely presented soluble group \(G\) such that for no normal subgroup \(M\) of finite index in \(G\) is there a normal subgroup \(N\) of \(M\) with \(N\) and \(M/N\) both nilpotent.

public theorem_wanted finitelyPresentedSolubleMetanilpotentByFinite_refuted :
    ¬ finitelyPresentedSolubleMetanilpotentByFinite

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 16.35 (J. R. J. Groves); resolution: V. V. Bludov, letter of 27 April 2007, as recorded in the Kourovka Archive, Kourovka Archive, Problem 16.35 (No: for a prime p, ⟨a, b, c, d | b^a = b^p, c^a = c^p, d^a = d, c^b = c, d^c = d d^b, [d, d^b] = 1, d^p = 1⟩ is soluble of derived length 3 but not metanilpotent-by-finite).

Uses 1

Statement usesGroves's question (Kourovka 16.35)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.