Fixed subgroups of free group automorphisms

DefinitionNorm of an automorphism of a free group#✓fully proved

Let \(F_n\) be the free group on the basis \(x_0, \dots, x_{n-1}\), and for \(w \in F_n\) let \(|w|\) be the length of the reduced word representing \(w\). The norm of an automorphism \(\alpha\) of \(F_n\) is \(\|\alpha\| = \max(|\alpha(x_0)|, \dots, |\alpha(x_{n-1})|)\), taken to be \(0\) when \(n = 0\).

def autNorm {n : ℕ} (α : MulAut (FreeGroup (Fin n))) : ℕ :=
  Finset.univ.sup fun i => (α (FreeGroup.of i)).norm

Used by 2

Used byKourovka Problem 14.23, rank-dependent form · Kourovka Problem 14.23, rank-uniform form

DefinitionFixed subgroup of a free group automorphism#✓fully proved

For an automorphism \(\alpha\) of the free group \(F_n\) on \(x_0, \dots, x_{n-1}\), the fixed subgroup of \(\alpha\) is the subgroup \(\mathrm{Fix}(\alpha) = \{x \in F_n \mid \alpha(x) = x\}\) of \(F_n\).

def fixedSubgroup {n : ℕ} (α : MulAut (FreeGroup (Fin n))) : Subgroup (FreeGroup (Fin n)) :=
  (α : FreeGroup (Fin n) →* FreeGroup (Fin n)).eqLocus (MonoidHom.id _)

Used by 1

Used byFixed subgroups with a short free basis

DefinitionFixed subgroups with a short free basis#✓fully proved

Let \(\alpha\) be an automorphism of the free group \(F_n\) on \(x_0, \dots, x_{n-1}\), let \(|w|\) be the length of the reduced word representing \(w \in F_n\), and let \(L\) be a natural number. The fixed subgroup \(\mathrm{Fix}(\alpha)\) has a short free basis with bound \(L\) when, for some \(k \ge 0\), it has a free basis \(y_1, \dots, y_k\) with \(|y_i| \le L\) for every \(i\).

def HasShortFixedBasis {n : ℕ} (α : MulAut (FreeGroup (Fin n))) (L : ℕ) : Prop :=
  ∃ (k : ℕ) (b : FreeGroupBasis (Fin k) (fixedSubgroup α)),
    ∀ i, ((b i : fixedSubgroup α) : FreeGroup (Fin n)).norm ≤ L

Uses 1 · Used by 2

Statement usesFixed subgroup of a free group automorphism

Used byKourovka Problem 14.23, rank-dependent form · Kourovka Problem 14.23, rank-uniform form

DefinitionKourovka Problem 14.23, rank-dependent form#✓fully proved

For every \(n\) there is a computable function \(f : \mathbb{N} \to \mathbb{N}\) such that for every automorphism \(\alpha\) of the free group \(F_n\) on \(x_0, \dots, x_{n-1}\), the fixed subgroup \(\mathrm{Fix}(\alpha)\) has a finite free basis all of whose elements have reduced word length at most \(f(\|\alpha\|)\), where \(\|\alpha\|\) is the maximum of the reduced word lengths of \(\alpha(x_0), \dots, \alpha(x_{n-1})\).

This is the form of Kourovka Notebook Problem 14.23 (O. V. Bogopolski) in which \(f\) may depend on the rank \(n\).

def fixedSubgroupBasisRecursiveBoundEachRank : Prop :=
  ∀ n : ℕ, ∃ f : ℕ → ℕ, Computable f ∧
    ∀ α : MulAut (FreeGroup (Fin n)), HasShortFixedBasis α (f (autNorm α))

Uses 2 · Used by 1

Statement usesFixed subgroups with a short free basis · Norm of an automorphism of a free group

Used byKourovka Problem 14.23 holds for each rank

DefinitionKourovka Problem 14.23, rank-uniform form#✓fully proved

There is a computable function \(f : \mathbb{N} \to \mathbb{N}\) such that for every \(n\) and every automorphism \(\alpha\) of the free group \(F_n\) on \(x_0, \dots, x_{n-1}\), the fixed subgroup \(\mathrm{Fix}(\alpha)\) has a finite free basis all of whose elements have reduced word length at most \(f(\|\alpha\|)\), where \(\|\alpha\|\) is the maximum of the reduced word lengths of \(\alpha(x_0), \dots, \alpha(x_{n-1})\).

This is the form of Kourovka Notebook Problem 14.23 (O. V. Bogopolski) in which one \(f\) must work for all ranks \(n\).

def fixedSubgroupBasisRecursiveBoundUniform : Prop :=
  ∃ f : ℕ → ℕ, Computable f ∧
    ∀ (n : ℕ) (α : MulAut (FreeGroup (Fin n))), HasShortFixedBasis α (f (autNorm α))

Uses 2 · Used by 1

Statement usesFixed subgroups with a short free basis · Norm of an automorphism of a free group

Used byKourovka Problem 14.23 fails uniformly in the rank

TheoremKourovka Problem 14.23 holds for each rank#●ready to prove

For every \(n\) there is a computable function \(f : \mathbb{N} \to \mathbb{N}\) such that for every automorphism \(\alpha\) of the free group \(F_n\) on \(x_0, \dots, x_{n-1}\), the fixed subgroup \(\mathrm{Fix}(\alpha)\) has a finite free basis all of whose elements have reduced word length at most \(f(\|\alpha\|)\), where \(\|\alpha\|\) is the maximum of the reduced word lengths of \(\alpha(x_0), \dots, \alpha(x_{n-1})\).

This follows from the algorithm computing a basis of \(\mathrm{Fix}(\alpha)\) (Kharlampovich, Proposition 2); the Kourovka Notebook (21st issue) records this answer.

public theorem_wanted fixedSubgroupBasisRecursiveBoundEachRank_holds :
    fixedSubgroupBasisRecursiveBoundEachRank

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 14.23 (O. V. Bogopolski); resolution: O. Kharlampovich, Two observations on Problems 14.23 and 17.32 of the Kourovka Notebook, preprint (2026), Proposition 2 (each rank); O. Kharlampovich, A counterexample to the rank-uniform form of Kourovka Notebook Problem 14.23, preprint (2026), Theorem 1, the Kourovka Notebook (21st issue) marks 14.23 solved: true for each given rank, false if one function must work for all ranks, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/08/kourovka_14_23_uniform_counterexample.pdf.

Uses 1

Statement usesKourovka Problem 14.23, rank-dependent form

TheoremKourovka Problem 14.23 fails uniformly in the rank#●ready to prove

There is no computable function \(f : \mathbb{N} \to \mathbb{N}\) such that for every \(n\) and every automorphism \(\alpha\) of the free group \(F_n\) on \(x_0, \dots, x_{n-1}\), the fixed subgroup \(\mathrm{Fix}(\alpha)\) has a finite free basis all of whose elements have reduced word length at most \(f(\|\alpha\|)\), where \(\|\alpha\|\) is the maximum of the reduced word lengths of \(\alpha(x_0), \dots, \alpha(x_{n-1})\).

Kharlampovich (Theorem 1) proves more: for every \(r \ge 3\) there is an automorphism \(\alpha_r\) of the free group of rank \(2r - 1\) with \(\|\alpha_r\| = 3\) such that every generating set of \(\mathrm{Fix}(\alpha_r)\) contains an element of length at least \(r\), so no function at all, computable or not, works for all ranks; the Kourovka Notebook (21st issue) records this answer.

public theorem_wanted fixedSubgroupBasisRecursiveBoundUniform_refuted :
    ¬ fixedSubgroupBasisRecursiveBoundUniform

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 14.23 (O. V. Bogopolski); resolution: O. Kharlampovich, Two observations on Problems 14.23 and 17.32 of the Kourovka Notebook, preprint (2026), Proposition 2 (each rank); O. Kharlampovich, A counterexample to the rank-uniform form of Kourovka Notebook Problem 14.23, preprint (2026), Theorem 1, the Kourovka Notebook (21st issue) marks 14.23 solved: true for each given rank, false if one function must work for all ranks, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/08/kourovka_14_23_uniform_counterexample.pdf.

Uses 1

Statement usesKourovka Problem 14.23, rank-uniform form

AbbreviationEncoded words in a free group of finite rank#✓fully proved

A word of rank \(r\) is a finite list of pairs \((i, \varepsilon)\) with \(i < r\) and \(\varepsilon\) a Boolean. It encodes the element of the free group \(F_r\) of rank \(r\) that is the product of its letters, where \((i, \mathrm{true})\) stands for the \(i\)-th free generator and \((i, \mathrm{false})\) for its inverse.

abbrev Word (r : ℕ) : Type :=
  List (Fin r × Bool)

Used by 2

Used byDecidability of fixed points of free group automorphisms (Kourovka 10.25) · Endomorphism of a free group given by generator images

DefinitionEndomorphism of a free group given by generator images#✓fully proved

Let \(F_r\) be the free group on generators \(e_0, \dots, e_{r-1}\). Given, for each \(i < r\), a word \(u_i\) in these generators and their inverses, this is the endomorphism of \(F_r\) sending each \(e_i\) to the element of \(F_r\) represented by \(u_i\).

def endo {r : ℕ} (img : Fin r → Word r) : FreeGroup (Fin r) →* FreeGroup (Fin r) :=
  FreeGroup.lift fun a => FreeGroup.mk (img a)

Uses 1 · Used by 1

Statement usesEncoded words in a free group of finite rank

Used byDecidability of fixed points of free group automorphisms (Kourovka 10.25)

DefinitionDecidability of fixed points of free group automorphisms (Kourovka 10.25)#✓fully proved

The assertion that for every natural number \(r\) there is a computable function \(f\) which takes the images of the \(r\) free generators of the free group \(F_r\), each encoded as a word in the generators and their inverses, and returns a Boolean, such that whenever the endomorphism \(\varphi\) of \(F_r\) sending each generator to its image is bijective, \(f\) returns true exactly when \(\varphi(w) = w\) for some \(w \neq 1\) in \(F_r\).

def automorphismFixedPointDecidable : Prop :=
  ∀ r : ℕ, ∃ f : (Fin r → Word r) → Bool, Computable f ∧
    ∀ img : Fin r → Word r, Function.Bijective (endo img) →
      (f img = true ↔ ∃ w : FreeGroup (Fin r), w ≠ 1 ∧ endo img w = w)

Uses 2 · Used by 1

Statement usesEncoded words in a free group of finite rank · Endomorphism of a free group given by generator images

Used byFixed points of free group automorphisms are decidable (Kourovka 10.25)

TheoremFixed points of free group automorphisms are decidable (Kourovka 10.25)#●ready to prove

For every natural number \(r\) there is a computable function \(f\) which takes the images of the \(r\) free generators of the free group \(F_r\), each encoded as a word in the generators and their inverses, and returns a Boolean, such that whenever the endomorphism \(\varphi\) of \(F_r\) sending each generator to its image is bijective, \(f\) returns true exactly when \(\varphi(w) = w\) for some \(w \neq 1\) in \(F_r\).

The Kourovka Archive answers Problem 10.25 "Yes, it does", citing Bogopolski and Maslakova (2016), who give an algorithm computing a basis of the fixed subgroup of an automorphism of a free group of finite rank; the automorphism has a non-trivial fixed point exactly when that basis is nonempty.

public theorem_wanted automorphismFixedPointDecidable_holds : automorphismFixedPointDecidable

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 10.25 (G. S. Makanin); resolution: O. Bogopolski and O. Maslakova, Int. J. Algebra Comput. 26, no. 1 (2016), 29-67, algorithm computing a basis of the fixed subgroup of an automorphism of a free group of finite rank; Kourovka Archive, Problem 10.25 ("Yes, it does").

Uses 1

Statement usesDecidability of fixed points of free group automorphisms (Kourovka 10.25)

8 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.