Locally nilpotent groups

DefinitionLocally nilpotent subgroup#✓fully proved

A subgroup \(N\) of a group \(G\) is locally nilpotent when every subgroup generated by finitely many elements of \(N\) is nilpotent.

def IsLocallyNilpotent {G : Type} [Group G] (N : Subgroup G) : Prop :=
  ∀ s : Finset G, (s : Set G) ⊆ N → Group.IsNilpotent (Subgroup.closure (s : Set G))

Used by 1

Used byHirsch–Plotkin radical

DefinitionHirsch–Plotkin radical#✓fully proved

The Hirsch–Plotkin radical of a group \(G\) is the subgroup generated by all locally nilpotent normal subgroups of \(G\). By the Hirsch–Plotkin theorem it is the largest locally nilpotent normal subgroup of \(G\).

def hirschPlotkinRadical (G : Type) [Group G] : Subgroup G :=
  sSup {N : Subgroup G | N.Normal ∧ IsLocallyNilpotent N}

Uses 1

Statement usesLocally nilpotent subgroup

DefinitionLocally nilpotent group (Kourovka 13.16)#✓fully proved

A group \(G\) is locally nilpotent if for every finite subset \(S \subseteq G\) the subgroup generated by \(S\) is nilpotent, that is, every finitely generated subgroup of \(G\) is nilpotent.

def IsLocallyNilpotent (G : Type*) [Group G] : Prop :=
  ∀ S : Set G, S.Finite → Group.IsNilpotent (Subgroup.closure S)

Used by 1

Used byKourovka Problem 13.16 (Wagner)

DefinitionMinimal condition on centralizers (Kourovka 13.16)#✓fully proved

For a subset \(X\) of a group \(G\), let \(C_G(X)\) be its centralizer, the subgroup of elements of \(G\) that commute with every element of \(X\). The group \(G\) satisfies the minimal condition on centralizers if every nonempty set of such centralizers has a minimal element with respect to inclusion; equivalently, there is no infinite strictly descending chain \(C_G(X_0) > C_G(X_1) > \cdots\) of centralizers.

def HasMinCentralizers (G : Type*) [Group G] : Prop :=
  WellFounded fun H K : {H : Subgroup G // ∃ X : Set G, H = Subgroup.centralizer X} => H.1 < K.1

Used by 1

Used byKourovka Problem 13.16 (Wagner)

DefinitionHypercentral group (Kourovka 13.16)#✓fully proved

A group \(G\) is hypercentral if for every proper normal subgroup \(N\) of \(G\) there is some \(g \in G\) with \(g \notin N\) and \(g h g^{-1} h^{-1} \in N\) for all \(h \in G\); that is, every nontrivial quotient \(G/N\) has nontrivial centre (equivalently, the transfinite upper central series of \(G\) reaches \(G\)).

def IsHypercentral (G : Type*) [Group G] : Prop :=
  ∀ N : Subgroup G, N.Normal → N ≠ ⊤ → ∃ g : G, g ∉ N ∧ ∀ h : G, g * h * g⁻¹ * h⁻¹ ∈ N

Used by 1

Used byKourovka Problem 13.16 (Wagner)

DefinitionKourovka Problem 13.16 (Wagner)#✓fully proved

The proposition that every locally nilpotent group satisfying the minimal condition on centralizers is hypercentral.

def locallyNilpotentMinCentralizersHypercentral : Prop :=
  ∀ (G : Type) [Group G], IsLocallyNilpotent G → HasMinCentralizers G → IsHypercentral G

Uses 3 · Used by 1

Statement usesMinimal condition on centralizers (Kourovka 13.16) · Hypercentral group (Kourovka 13.16) · Locally nilpotent group (Kourovka 13.16)

Used byLocally nilpotent groups with the minimal condition on centralizers are hypercentral

TheoremLocally nilpotent groups with the minimal condition on centralizers are hypercentral#●ready to prove

Every locally nilpotent group satisfying the minimal condition on centralizers is hypercentral. This answers Kourovka Problem 13.16 (F. O. Wagner) in the affirmative (V. V. Bludov, 1998).

public theorem_wanted locallyNilpotentMinCentralizersHypercentral_holds :
    locallyNilpotentMinCentralizersHypercentral

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 13.16 (F. O. Wagner); resolution: V. V. Bludov, Algebra and Logic 37 (1998), no. 3, 151-156, Kourovka Archive, Problem 13.16: Yes, it is.

Uses 1

Statement usesKourovka Problem 13.16 (Wagner)

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.