Cofinitary permutation groups

DefinitionCofinitary permutation groups#✓fully proved

A subgroup \(G\) of the group of permutations of a set \(\Omega\) is cofinitary when every non-identity element of \(G\) fixes only finitely many points of \(\Omega\).

def IsCofinitary {Ω : Type} (G : Subgroup (Equiv.Perm Ω)) : Prop :=
  ∀ g ∈ G, g ≠ 1 → {x : Ω | g x = x}.Finite

Used by 1

Used byClaim of Kourovka Problem 13.28

DefinitionClaim of Kourovka Problem 13.28#✓fully proved

For every infinite set \(\Omega\), every cofinitary subgroup \(G\) of the group of permutations of \(\Omega\) that is closed in the topology of pointwise convergence is locally compact in the subspace topology.

def closedCofinitaryLocallyCompact : Prop :=
  ∀ (Ω : Type) [Infinite Ω] (G : Subgroup (Equiv.Perm Ω)), IsCofinitary G →
    @IsClosed _ (Equiv.Perm.pointwiseTopology (α := Ω)) (G : Set (Equiv.Perm Ω)) →
    @LocallyCompactSpace G
      (TopologicalSpace.induced ((↑) : G → Equiv.Perm Ω)
        (Equiv.Perm.pointwiseTopology (α := Ω)))

Uses 2 · Used by 1

Statement usesPointwise convergence topology on permutations · Cofinitary permutation groups

Used byClosed cofinitary permutation groups need not be locally compact

TheoremClosed cofinitary permutation groups need not be locally compact#●ready to prove

The claim of Kourovka Problem 13.28 is false: there are an infinite set \(\Omega\) and a subgroup \(G\) of the group of permutations of \(\Omega\) such that \(G\) is cofinitary (every non-identity element of \(G\) fixes only finitely many points of \(\Omega\)) and closed in the topology of pointwise convergence, but \(G\) is not locally compact in the subspace topology.

public theorem_wanted closedCofinitaryLocallyCompact_refuted : ¬ closedCofinitaryLocallyCompact

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.28 (D. M. Evans; P. J. Cameron); resolution: G. Hjorth, J. Algebra 200 (1998), no. 2, 439-448, Kourovka Archive, Problem 13.28: No, not always.

Uses 1

Statement usesClaim of Kourovka Problem 13.28

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.