Minimal condition on centralizers

DefinitionLocally finite group#✓fully proved

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

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

Used by 1

Used byWilson's question on \(2\)-groups with the minimal condition on centralizers (Kourovka problem 11.103)

DefinitionMinimal condition on centralizers#✓fully proved

For a subset \(X\) of a group \(G\), write \(C_G(X)\) for the centralizer of \(X\) in \(G\). The group \(G\) satisfies the minimal condition on centralizers when there is no sequence of subsets \(X_0, X_1, X_2, \ldots\) of \(G\) whose centralizers form a strictly descending chain \(C_G(X_0) > C_G(X_1) > C_G(X_2) > \cdots\), where \(H > K\) means that \(K\) is a proper subgroup of \(H\).

def MinimalConditionOnCentralizers (G : Type*) [Group G] : Prop :=
  ¬ ∃ X : ℕ → Set G, ∀ i, Subgroup.centralizer (X (i + 1)) < Subgroup.centralizer (X i)

Used by 1

Used byWilson's question on \(2\)-groups with the minimal condition on centralizers (Kourovka problem 11.103)

DefinitionWilson's question on \(2\)-groups with the minimal condition on centralizers (Kourovka problem 11.103)#✓fully proved

Wilson's question on \(2\)-groups with the minimal condition on centralizers (Kourovka problem 11.103). The statement that every group \(G\) in which every element has order a power of \(2\) and which satisfies the minimal condition on centralizers is locally finite.

def twoGroupMinimalCentralizersLocallyFinite : Prop :=
  ∀ (G : Type) [Group G], IsPGroup 2 G → MinimalConditionOnCentralizers G → IsLocallyFinite G

Uses 2 · Used by 1

Statement usesLocally finite group · Minimal condition on centralizers

Used byEvery \(2\)-group with the minimal condition on centralizers is locally finite (Kourovka 11.103)

TheoremEvery \(2\)-group with the minimal condition on centralizers is locally finite (Kourovka 11.103)#●ready to prove

Every group \(G\) in which every element has order a power of \(2\) and which satisfies the minimal condition on centralizers is locally finite.

Wagner proved that the Sylow \(2\)-subgroups of a periodic group with the minimal condition on centralizers are locally finite; a \(2\)-group is periodic and is its own Sylow \(2\)-subgroup. The Kourovka Archive answers 11.103 "Yes, it is".

public theorem_wanted twoGroupMinimalCentralizersLocallyFinite_holds :
    twoGroupMinimalCentralizersLocallyFinite

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 11.103 (John S. Wilson); resolution: F. O. Wagner, Nilpotency in groups with the minimal condition on centralizers, J. Algebra 217, no. 2 (1999), 448-460, abstract: the Sylow 2-subgroups of a periodic group with the minimal condition on centralizers are locally finite and conjugate; Kourovka Archive, Problem 11.103, https://doi.org/10.1006/jabr.1998.7824.

Uses 1

Statement usesWilson's question on \(2\)-groups with the minimal condition on centralizers (Kourovka problem 11.103)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.