Residually nilpotent groups

DefinitionResidually nilpotent group#✓fully proved

A group \(G\) is residually nilpotent if for every element \(g \ne 1\) of \(G\) there is a normal subgroup \(N\) of \(G\) with \(g \notin N\) such that the quotient \(G/N\) is nilpotent.

def IsResiduallyNilpotent (G : Type) [Group G] : Prop :=
  ∀ g : G, g ≠ 1 → ∃ N : Subgroup G, ∃ _ : N.Normal, g ∉ N ∧ Group.IsNilpotent (G ⧸ N)

Used by 1

Used byMikhailov–Passi question on free central extensions (Kourovka 16.65)

DefinitionResidually torsion-free nilpotent group#✓fully proved

A group \(G\) is residually torsion-free nilpotent if for every element \(g \ne 1\) of \(G\) there is a normal subgroup \(N\) of \(G\) with \(g \notin N\) such that the quotient \(G/N\) is nilpotent and torsion-free, that is, every nontrivial element of \(G/N\) has infinite order.

def IsResiduallyTorsionFreeNilpotent (G : Type) [Group G] : Prop :=
  ∀ g : G, g ≠ 1 → ∃ N : Subgroup G, ∃ _ : N.Normal, g ∉ N ∧ Group.IsNilpotent (G ⧸ N) ∧
    ∀ x : G ⧸ N, x ≠ 1 → ¬ IsOfFinOrder x

Used by 1

Used byMikhailov–Passi question on free central extensions (Kourovka 16.65)

DefinitionMikhailov–Passi question on free central extensions (Kourovka 16.65)#✓fully proved

The assertion that there exist a free group \(F\) and a normal subgroup \(R\) of \(F\) such that \(F/R\) is finitely presented and residually torsion-free nilpotent, while \(F/[F, R]\) is not residually nilpotent, where \([F, R]\) is the subgroup of \(F\) generated by all commutators \([f, r]\) with \(f \in F\) and \(r \in R\).

def existsPresentationWithNonResiduallyNilpotentQuotient : Prop :=
  ∃ (α : Type) (R : Subgroup (FreeGroup α)) (_ : R.Normal),
    Group.IsFinitelyPresented (FreeGroup α ⧸ R) ∧
    IsResiduallyTorsionFreeNilpotent (FreeGroup α ⧸ R) ∧
    ¬ IsResiduallyNilpotent (FreeGroup α ⧸ ⁅(⊤ : Subgroup (FreeGroup α)), R⁆)

Uses 2 · Used by 1

Statement usesResidually nilpotent group · Residually torsion-free nilpotent group

Used byFree central extensions need not be residually nilpotent

TheoremFree central extensions need not be residually nilpotent#●ready to prove

There exist a free group \(F\) and a normal subgroup \(R\) of \(F\) such that \(F/R\) is finitely presented and residually torsion-free nilpotent, while \(F/[F, R]\) is not residually nilpotent; here \([F, R]\) is the subgroup of \(F\) generated by all commutators \([f, r]\) with \(f \in F\) and \(r \in R\).

public theorem_wanted existsPresentationWithNonResiduallyNilpotentQuotient_holds :
    existsPresentationWithNonResiduallyNilpotentQuotient

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.65 (R. Mikhailov, I. B. S. Passi); resolution: V. V. Bludov, J. Group Theory 12 (2009), no. 4, 579-590, Kourovka Archive, Problem 16.65 (Yes, there does).

Uses 1

Statement usesMikhailov–Passi question on free central extensions (Kourovka 16.65)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.