Centralizer dimension of locally finite groups

DefinitionLocally finite groups#✓fully proved

A group \(G\) is locally finite if every finitely generated subgroup of \(G\) is finite.

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

Used by 1

Used byVasil'ev's abelian section bound (Kourovka 19.101)

DefinitionLocally soluble subgroups#✓fully proved

A subgroup \(H\) of a group \(G\) is locally soluble if every finitely generated subgroup of \(H\) is soluble.

def IsLocallySoluble {G : Type} [Group G] (H : Subgroup G) : Prop :=
  ∀ s : Finset G, (s : Set G) ⊆ H → Group.IsSolvable (Subgroup.closure (s : Set G))

Used by 1

Used byVasil'ev's abelian section bound (Kourovka 19.101)

DefinitionCentralizer dimension at most \(k\)#✓fully proved

A group \(G\) has \(c\)-dimension at most \(k\) if every strictly decreasing chain \(C_G(X_0) > C_G(X_1) > \cdots > C_G(X_m)\) of centralizers of subsets \(X_0, \dots, X_m\) of \(G\) has length \(m \le k\).

def CDimLE (G : Type) [Group G] (k : ℕ) : Prop :=
  ∀ (m : ℕ) (X : ℕ → Set G),
    (∀ i < m, Subgroup.centralizer (X (i + 1)) < Subgroup.centralizer (X i)) → m ≤ k

Used by 1

Used byVasil'ev's abelian section bound (Kourovka 19.101)

DefinitionMinimal normal subgroups#✓fully proved

A subgroup \(M\) of a group \(Q\) is a minimal normal subgroup if \(M\) is normal in \(Q\), \(M \ne \{1\}\), and every normal subgroup \(N\) of \(Q\) with \(N \le M\) is either \(\{1\}\) or \(M\).

def IsMinimalNormal {Q : Type} [Group Q] (M : Subgroup Q) : Prop :=
  M.Normal ∧ M ≠ ⊥ ∧ ∀ N : Subgroup Q, N.Normal → N ≤ M → N = ⊥ ∨ N = M

Used by 1

Used bySocle

DefinitionSocle#✓fully proved

The socle of a group \(Q\) is the subgroup of \(Q\) generated by all minimal normal subgroups of \(Q\); it is the trivial subgroup when \(Q\) has no minimal normal subgroup.

noncomputable def socle (Q : Type) [Group Q] : Subgroup Q :=
  sSup {M : Subgroup Q | IsMinimalNormal M}

Uses 1 · Used by 1

Statement usesMinimal normal subgroups

Used byPreimage of the socle of a quotient

DefinitionPreimage of the socle of a quotient#✓fully proved

For a normal subgroup \(R\) of a group \(G\), the preimage in \(G\) of the socle of \(G/R\) under the quotient map \(G \to G/R\).

noncomputable def socleLift {G : Type} [Group G] (R : Subgroup G) [R.Normal] : Subgroup G :=
  (socle (G ⧸ R)).comap (QuotientGroup.mk' R)

Uses 1 · Used by 1

Statement usesSocle

Used byVasil'ev's abelian section bound (Kourovka 19.101)

DefinitionVasil'ev's abelian section bound (Kourovka 19.101)#✓fully proved

The statement that there is a function \(f : \mathbb{N} \to \mathbb{N}\) such that for every \(k \in \mathbb{N}\) and every locally finite group \(G\) of \(c\)-dimension at most \(k\) the following holds: if \(R\) is a normal locally soluble subgroup of \(G\) containing every normal locally soluble subgroup of \(G\) (the locally soluble radical) and \(S\) is the preimage in \(G\) of the socle of \(G/R\), then there is a subgroup \(A\) of \(G\) with \(S \le A\) such that \(xyx^{-1}y^{-1} \in S\) for all \(x, y \in A\) (so \(A/S\) is an abelian subgroup of \(G/S\)), and the index \(|G : A|\) is finite and at most \(f(k)\).

def centralizerDimensionAbelianSectionBound : Prop :=
  ∃ f : ℕ → ℕ, ∀ (k : ℕ) (G : Type) [Group G], IsLocallyFinite G → CDimLE G k →
    ∀ (R : Subgroup G) [R.Normal], IsLocallySoluble R →
      (∀ N : Subgroup G, N.Normal → IsLocallySoluble N → N ≤ R) →
      ∃ A : Subgroup G, socleLift R ≤ A ∧
        (∀ x ∈ A, ∀ y ∈ A, x * y * x⁻¹ * y⁻¹ ∈ socleLift R) ∧ A.index ≠ 0 ∧ A.index ≤ f k

Uses 4 · Used by 1

Statement usesCentralizer dimension at most \(k\) · Locally finite groups · Locally soluble subgroups · Preimage of the socle of a quotient

Used byButurlakin's theorem on locally finite groups of finite \(c\)-dimension

TheoremButurlakin's theorem on locally finite groups of finite \(c\)-dimension#●ready to prove

There is a function \(f : \mathbb{N} \to \mathbb{N}\) such that the following holds for every \(k \in \mathbb{N}\). Let \(G\) be a locally finite group of \(c\)-dimension at most \(k\), let \(R\) be a normal locally soluble subgroup of \(G\) that contains every normal locally soluble subgroup of \(G\) (the locally soluble radical), and let \(S\) be the preimage in \(G\) of the socle of \(G/R\). Then there is a subgroup \(A\) of \(G\) with \(S \le A\) such that \(xyx^{-1}y^{-1} \in S\) for all \(x, y \in A\) (so \(A/S\) is an abelian subgroup of \(G/S\)), and the index \(|G : A|\) is finite and at most \(f(k)\).

public theorem_wanted centralizerDimensionAbelianSectionBound_holds :
    centralizerDimensionAbelianSectionBound

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 19.101 (A. V. Vasil'ev); resolution: A. A. Buturlakin, J. Algebra Appl. 18 (2019), no. 12, 1950223, 12 pp, Kourovka Archive, Problem 19.101: Yes, it is true, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesVasil'ev's abelian section bound (Kourovka 19.101)

7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.