Cayley–Hamilton analogue for free groups

DefinitionBogopolski's Cayley–Hamilton question for free groups (Kourovka 17.32)#✓fully proved

The assertion that for every natural number \(n\), every element \(w\) of the free group \(F_n\) of rank \(n\) and every automorphism \(\varphi\) of \(F_n\), if \(w, \varphi(w), \dots, \varphi^n(w)\) generate \(F_n\), then already \(w, \varphi(w), \dots, \varphi^{n-1}(w)\) generate \(F_n\).

def freeGroupCayleyHamilton : Prop :=
  ∀ (n : ℕ) (w : FreeGroup (Fin n)) (φ : MulAut (FreeGroup (Fin n))),
    Subgroup.closure {x | ∃ i ≤ n, x = (φ ^ i) w} = ⊤ →
      Subgroup.closure {x | ∃ i < n, x = (φ ^ i) w} = ⊤
Used by 1

TheoremBogopolski's Cayley–Hamilton analogue fails for free groups (Kourovka 17.32)#●ready to prove

There are a natural number \(n\), an element \(w\) of the free group \(F_n\) of rank \(n\) and an automorphism \(\varphi\) of \(F_n\) such that \(w, \varphi(w), \dots, \varphi^n(w)\) generate \(F_n\) but \(w, \varphi(w), \dots, \varphi^{n-1}(w)\) do not.

Ionin and Semidetnov (Answer 8.2) give the example \(n = 2\), \(F_2 = \langle x, y \rangle\), \(w = xy\) and \(\varphi(x) = yx\), \(\varphi(y) = x\). The Kourovka Notebook (21st issue) answers 17.32 "No, it is not true", citing their preprint and a preprint of O. Kharlampovich.

public theorem_wanted freeGroupCayleyHamilton_refuted : ¬ freeGroupCayleyHamilton
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 17.32 (O. V. Bogopolski); resolution: V. Ionin and A. Semidetnov, On some more problems from the Kourovka Notebook, preprint, arXiv:2608.29219 (2026; solutions found with the assistance of large language models and checked by the authors, per its abstract); O. Kharlampovich, preprint (2026), Ionin-Semidetnov, Answer 8.2 (the assertion fails for n = 2: w = xy, φ(x) = yx, φ(y) = x); the Kourovka Notebook (21st issue) marks 17.32 solved (No, it is not true), https://arxiv.org/abs/2608.29219.
Uses 1
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.