Locally finite simple groups

DefinitionLocally finite group#✓fully proved

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

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

Used by 1

Used byAbsolute simplicity of locally finite simple groups (Kourovka 11.108)

DefinitionComposition series in Kurosh's sense#✓fully proved

A set \(S\) of subgroups of a group \(G\) is a composition series of \(G\) when it contains the trivial subgroup and \(G\), it is totally ordered by inclusion, it contains the join and the intersection of every subset of \(S\), and for every jump \(A < B\) of \(S\) (members \(A \subsetneq B\) of \(S\) with no member of \(S\) strictly between them) \(A\) is normal in \(B\) and the quotient \(B / A\) is a simple group.

def IsCompositionSeries {G : Type*} [Group G] (S : Set (Subgroup G)) : Prop :=
  ⊥ ∈ S ∧ ⊤ ∈ S ∧ IsChain (· ≤ ·) S ∧ (∀ T ⊆ S, sSup T ∈ S) ∧ (∀ T ⊆ S, sInf T ∈ S) ∧
    ∀ A ∈ S, ∀ B ∈ S, A < B → (∀ C ∈ S, ¬ (A < C ∧ C < B)) →
      ∃ _ : (A.subgroupOf B).Normal, IsSimpleGroup (B ⧸ A.subgroupOf B)

Used by 1

Used byAbsolute simplicity of locally finite simple groups (Kourovka 11.108)

DefinitionAbsolute simplicity of locally finite simple groups (Kourovka 11.108)#✓fully proved

The statement, asked by R. Phillips, that every locally finite simple group \(G\) is absolutely simple: every composition series of \(G\) in Kurosh's sense consists of the trivial subgroup and \(G\) alone.

def locallyFiniteSimpleIsAbsolutelySimple : Prop :=
  ∀ (G : Type) [Group G], IsLocallyFinite G → IsSimpleGroup G →
    ∀ S : Set (Subgroup G), IsCompositionSeries S → S = {⊥, ⊤}

Uses 2 · Used by 1

Statement usesComposition series in Kurosh's sense · Locally finite group

Used byLocally finite simple groups need not be absolutely simple

TheoremLocally finite simple groups need not be absolutely simple#●ready to prove

There is a locally finite simple group \(G\) with a composition series, in Kurosh's sense, other than the series consisting of the trivial subgroup and \(G\) alone. That is, the statement of Kourovka Problem 11.108, that every locally finite simple group is absolutely simple, is false.

The Kourovka Archive answers 11.108 "No, not every", citing Meierfrankenfeld (1995), whose Section 6 constructs countable locally finite simple groups \(G\) that are not absolutely simple, with an ascending series \(M_1 \trianglelefteq M_2 \trianglelefteq \cdots\) of proper subgroups whose union is \(G\).

public theorem_wanted locallyFiniteSimpleIsAbsolutelySimple_refuted :
    ¬ locallyFiniteSimpleIsAbsolutelySimple

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.108 (R. Phillips); resolution: U. Meierfrankenfeld, Non-finitary locally finite simple groups, in: Proc. Int. Conf. Finite and Locally Finite Groups, Istanbul, 1994, Kluwer, 1995, 189-212, Section 6, countable locally finite simple groups that are not absolutely simple; Kourovka Archive, Problem 11.108 ("No, not every"), https://users.math.msu.edu/users/meierfra/Preprints/Nflfsg/nflfsg.pdf.

Uses 1

Statement usesAbsolute simplicity of locally finite simple groups (Kourovka 11.108)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.