Bases of permutation groups

DefinitionBase of a group action#✓fully proved

For a group \(G\) acting on a set \(\Omega\), a finite set \(B \subseteq \Omega\) is a base when its pointwise stabilizer is trivial: the only \(g \in G\) with \(g \cdot \omega = \omega\) for all \(\omega \in B\) is \(g = 1\).

def IsBase (G Ω : Type) [Group G] [MulAction G Ω] (B : Finset Ω) : Prop :=
  ∀ g : G, (∀ ω ∈ B, g • ω = ω) → g = 1

Used by 1

Used byMinimal base

DefinitionMinimal base#✓fully proved

For a group \(G\) acting on a set \(\Omega\), a finite set \(B \subseteq \Omega\) is a minimal base when it is a base, that is, its pointwise stabilizer in \(G\) is trivial, and for every \(\omega \in B\) the set \(B \setminus \{\omega\}\) is not a base.

def IsMinimalBase (G Ω : Type) [Group G] [MulAction G Ω] (B : Finset Ω) : Prop :=
  IsBase G Ω B ∧ ∀ ω ∈ B, ¬ IsBase G Ω (B.erase ω)

Uses 1 · Used by 1

Statement usesBase of a group action

Used byMaximal size of a minimal base

DefinitionMaximal size of a minimal base#✓fully proved

For a group \(G\), the number \(b(G)\) is the supremum in \(\mathbb{N}\) of the sizes of the minimal bases of \(G\) over all actions of \(G\) on a set \(\Omega\), where a minimal base is a finite set \(B \subseteq \Omega\) whose pointwise stabilizer in \(G\) is trivial while that of \(B \setminus \{\omega\}\) is not, for every \(\omega \in B\). It is the largest such size when these sizes are bounded, as they are for finite \(G\), and \(0\) when they are unbounded.

noncomputable def maxMinimalBaseSize (G : Type) [Group G] : ℕ :=
  sSup {k | ∃ (Ω : Type) (_ : MulAction G Ω) (B : Finset Ω), IsMinimalBase G Ω B ∧ B.card = k}

Uses 1 · Used by 1

Statement usesMinimal base

Used byCameron's question on minimal bases and independent sets

DefinitionIndependent subset of a group#✓fully proved

A finite subset \(S\) of a group \(G\) is independent when no element \(s \in S\) lies in the subgroup of \(G\) generated by \(S \setminus \{s\}\).

def IsIndependent {G : Type} [Group G] (S : Finset G) : Prop :=
  ∀ s ∈ S, s ∉ Subgroup.closure ((S.erase s : Finset G) : Set G)

Used by 1

Used byMaximal size of an independent set

DefinitionMaximal size of an independent set#✓fully proved

For a group \(G\), a finite subset \(S \subseteq G\) is independent when no \(s \in S\) lies in the subgroup generated by \(S \setminus \{s\}\). The number \(\mu'(G)\) is the supremum in \(\mathbb{N}\) of the sizes of the finite independent subsets of \(G\): their largest size when these sizes are bounded, as they are for finite \(G\), and \(0\) when they are unbounded.

noncomputable def maxIndependentSize (G : Type) [Group G] : ℕ :=
  sSup {k | ∃ S : Finset G, IsIndependent S ∧ S.card = k}

Uses 1 · Used by 1

Statement usesIndependent subset of a group

Used byCameron's question on minimal bases and independent sets

DefinitionCameron's question on minimal bases and independent sets#✓fully proved

The statement that \(b(G) = \mu'(G)\) for every finite group \(G\), where \(b(G)\) is the largest size of a minimal base of \(G\) over all actions of \(G\) on a set, and \(\mu'(G)\) is the largest size of an independent subset of \(G\) (a subset none of whose elements lies in the subgroup generated by the others).

This is Kourovka Notebook Problem 16.45, posed by P. J. Cameron.

def maxMinimalBaseSizeEqMaxIndependentSize : Prop :=
  ∀ (G : Type) [Group G] [Finite G], maxMinimalBaseSize G = maxIndependentSize G

Uses 2 · Used by 1

Statement usesMaximal size of an independent set · Maximal size of a minimal base

Used byKourovka Problem 16.45 has a negative answer

TheoremKourovka Problem 16.45 has a negative answer#●ready to prove

It is not true that \(b(G) = \mu'(G)\) for every finite group \(G\), where \(b(G)\) is the largest size of a minimal base of \(G\) over all actions of \(G\) on a set, and \(\mu'(G)\) is the largest size of an independent subset of \(G\).

The counterexample in the source is Kriebel's affine group \(G = \mathbb{F}_{29}^2 \rtimes \mathrm{SL}_2(5)\) of order \(100920\), for which \(b(G) = 3 < 4 = \mu'(G)\).

public theorem_wanted maxMinimalBaseSizeEqMaxIndependentSize_refuted :
    ¬ maxMinimalBaseSizeEqMaxIndependentSize

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 16.45 (P. J. Cameron); resolution: A. Kriebel, A counterexample to Kourovka Notebook Problem 16.45, preprint, Zenodo record 22929486 (2026), main theorem: G = F_29^2 ⋊ SL_2(5) of order 100920 has b(G) = 3 < 4 = μ'(G); the Kourovka Notebook (21st issue) marks 16.45 solved (AI solution confirmed by P. J. Cameron), https://zenodo.org/records/22929486.

Uses 1

Statement usesCameron's question on minimal bases and independent sets

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.