Free groups in the infinite symmetric group

DefinitionEmbedding the free group of rank 2 in \(\mathrm{Sym}(\mathbb{N})\) with finitely many orbits (Kourovka 12.10)#✓fully proved

Embedding the free group of rank 2 in \(\mathrm{Sym}(\mathbb{N})\) with finitely many orbits (Kourovka 12.10). The statement, posed by P. Neumann and A. M. W. Glass, that there is an injective group homomorphism \(f\) from the free group \(F_2\) of rank \(2\) into the symmetric group \(\mathrm{Sym}(\mathbb{N})\) of all permutations of \(\mathbb{N}\) such that, for every non-identity element \(w\) of \(F_2\), the cyclic subgroup generated by \(f(w)\) has only finitely many orbits on \(\mathbb{N}\).

def freeGroupEmbedsFiniteOrbits : Prop :=
  ∃ f : FreeGroup (Fin 2) →* Equiv.Perm ℕ, Function.Injective f ∧
    ∀ w : FreeGroup (Fin 2), w ≠ 1 →
      Finite (MulAction.orbitRel.Quotient (Subgroup.zpowers (f w)) ℕ)
Used by 1

TheoremThe free group of rank 2 embeds in \(\mathrm{Sym}(\mathbb{N})\) with finitely many orbits#●ready to prove

There is an injective group homomorphism \(f\) from the free group \(F_2\) of rank \(2\) into the symmetric group \(\mathrm{Sym}(\mathbb{N})\) of all permutations of \(\mathbb{N}\) such that, for every non-identity element \(w\) of \(F_2\), the cyclic subgroup generated by \(f(w)\) has only finitely many orbits on \(\mathbb{N}\). This answers Kourovka Problem 12.10 positively.

The Kourovka Archive answers 12.10 "Yes, it can" (Macpherson).

public theorem_wanted freeGroupEmbedsFiniteOrbits_holds : freeGroupEmbedsFiniteOrbits
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 12.10 (A. M. W. Glass); resolution: H. D. Macpherson, in: Ordered groups and infinite permutation groups (Mathematics and its Applications 354), Kluwer, Dordrecht, 1996, 221-230, Kourovka Archive, Problem 12.10: "Yes, it can", https://arxiv.org/abs/1401.0300v49.
Uses 1
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.