Perfect locally nilpotent p-groups

DefinitionLocally nilpotent group#✓fully proved

A group is locally nilpotent if every finitely generated subgroup is nilpotent.

def IsLocallyNilpotent (G : Type*) [Group G] : Prop :=
  ∀ H : Subgroup G, H.FG → Group.IsNilpotent H

Used by 1

Used byKourovka 14.86: perfect locally nilpotent \(p\)-groups with nilpotent proper subgroups

DefinitionKourovka 14.86: perfect locally nilpotent \(p\)-groups with nilpotent proper subgroups#✓fully proved

The proposition that for some prime \(p\) there is an infinite locally nilpotent \(p\)-group \(G\) (every element of \(G\) has order a power of \(p\)) such that \(G = [G, G]\) and every proper subgroup of \(G\) is nilpotent.

def perfectLocallyNilpotentPGroupWithNilpotentProperSubgroups : Prop :=
  ∃ p : ℕ, p.Prime ∧ ∃ (G : Type) (_ : Group G), Infinite G ∧ IsPGroup p G ∧
    IsLocallyNilpotent G ∧ commutator G = ⊤ ∧ ∀ H : Subgroup G, H ≠ ⊤ → Group.IsNilpotent H

Uses 1 · Used by 1

Statement usesLocally nilpotent group

Used byNo infinite perfect locally nilpotent \(p\)-group has only nilpotent proper subgroups

TheoremNo infinite perfect locally nilpotent \(p\)-group has only nilpotent proper subgroups#●ready to prove

There is no prime \(p\) and no infinite locally nilpotent \(p\)-group \(G\) (every element of \(G\) has order a power of \(p\)) such that \(G = [G, G]\) and every proper subgroup of \(G\) is nilpotent.

public theorem_wanted perfectLocallyNilpotentPGroupWithNilpotentProperSubgroups_refuted :
    ¬ perfectLocallyNilpotentPGroupWithNilpotentProperSubgroups

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 14.86 (J. Wiegold); resolution: A. O. Asar, Locally nilpotent p-groups whose proper subgroups are hypercentral or nilpotent-by-Chernikov, J. London Math. Soc. (2) 61 (2000), no. 2, 412-422, Kourovka Archive, Problem 14.86 (answer: No, it does not exist).

Uses 1

Statement usesKourovka 14.86: perfect locally nilpotent \(p\)-groups with nilpotent proper subgroups

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.