Word problem for automorphism groups of free groups

DefinitionThe automorphism spelled by a word#✓fully proved

Let \(F_n\) be the free group on \(n\) generators and let \(g_0, \dots, g_{k-1}\) be automorphisms of \(F_n\). A word \(w = ((i_1, b_1), \dots, (i_r, b_r))\) is a finite list of letters \((i, b)\) with \(i \in \mathbb{N}\) and \(b\) a boolean. The automorphism spelled by \(w\) over \((g_i)\) is the product \(a_1 a_2 \cdots a_r\) in \(\operatorname{Aut}(F_n)\), whose group operation is composition, where for \(i_j < k\) the factor \(a_j\) is \(g_{i_j}\) if \(b_j\) is true and \(g_{i_j}^{-1}\) if \(b_j\) is false, and for \(i_j \ge k\) the factor \(a_j\) is the identity. The empty word spells the identity.

def evalAutWord {n k : ℕ} (gens : Fin k → MulAut (FreeGroup (Fin n))) (w : List (ℕ × Bool)) :
    MulAut (FreeGroup (Fin n)) :=
  FreeGroup.lift (fun i : ℕ => if h : i < k then gens ⟨i, h⟩ else 1) (FreeGroup.mk w)

Used by 1

Used byThe word problem of Aut(Fₙ) for a family of automorphisms

DefinitionThe word problem of Aut(Fₙ) for a family of automorphisms#✓fully proved

Let \(F_n\) be the free group on \(n\) generators and let \(g_0, \dots, g_{k-1}\) be automorphisms of \(F_n\). A word is a finite list of letters \((i, b)\) with \(i \in \mathbb{N}\) and \(b\) a boolean. The word problem for \((g_i)\) is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of lists of pairs of a natural number and a boolean, to a word \(w\) such that every letter \((i, b)\) of \(w\) has \(i < k\) and the automorphism spelled by \(w\) over \((g_i)\) is the identity; here the letter \((i, \mathrm{true})\) stands for \(g_i\) and \((i, \mathrm{false})\) for \(g_i^{-1}\). Bitstrings that do not decode to a word are rejected.

noncomputable def autWordProblem {n k : ℕ} (gens : Fin k → MulAut (FreeGroup (Fin n))) :
    DecisionProblem := fun x =>
  match bitDecode (α := List (ℕ × Bool)) x with
  | some w => decide ((∀ l ∈ w, l.1 < k) ∧ evalAutWord gens w = 1)
  | none => false

Uses 10 · Used by 1

Statement usesThe automorphism spelled by a word · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Decision problems

Used byPolynomial-time word problem for Aut(Fₙ) (Kourovka 16.109)

DefinitionPolynomial-time word problem for Aut(Fₙ) (Kourovka 16.109)#✓fully proved

The proposition that for every \(n \ge 2\), writing \(F_n\) for the free group on \(n\) generators, for every natural number \(k\) and every family \(g_0, \dots, g_{k-1}\) of automorphisms of \(F_n\) that generates \(\operatorname{Aut}(F_n)\), the word problem of \(\operatorname{Aut}(F_n)\) for the family \((g_i)\), a decision problem on bitstrings, belongs to the complexity class P.

def autFreeGroupWordProblemInP : Prop :=
  ∀ n : ℕ, 2 ≤ n → ∀ (k : ℕ) (gens : Fin k → MulAut (FreeGroup (Fin n))),
    Subgroup.closure (Set.range gens) = ⊤ → autWordProblem gens ∈ P

Uses 4 · Used by 1

Statement usesThe word problem of Aut(Fₙ) for a family of automorphisms · Complexity classes · Decision problems · The complexity class P

Used byThe word problem for Aut(Fₙ) is solvable in polynomial time

TheoremThe word problem for Aut(Fₙ) is solvable in polynomial time#●ready to prove

Let \(n \ge 2\) and let \(F_n\) be the free group on \(n\) generators. For every natural number \(k\) and every family \(g_0, \dots, g_{k-1}\) of automorphisms of \(F_n\) that generates \(\operatorname{Aut}(F_n)\), the word problem of \(\operatorname{Aut}(F_n)\) for this family belongs to the complexity class P. Here a word is a finite list of letters \((i, b)\) with \(i \in \mathbb{N}\) and \(b\) a boolean, the letter \((i, \mathrm{true})\) standing for \(g_i\) and \((i, \mathrm{false})\) for \(g_i^{-1}\), and the word problem is the decision problem on bitstrings that accepts exactly the bitstrings that decode, under the canonical bitstring encoding of lists of pairs of a natural number and a boolean, to a word whose letter indices are all below \(k\) and whose product in \(\operatorname{Aut}(F_n)\) is the identity; bitstrings that do not decode to a word are rejected.

Schleimer proves (Theorem 5.2) that the word problem for \(\operatorname{Aut}(F_m)\) is solvable in polynomial time, and observes (Remark 5.1) that changing the generating set alters running times by at most a multiplicative constant; the Kourovka Archive answers 16.109 "Yes, there is".

public theorem_wanted autFreeGroupWordProblemInP_holds : autFreeGroupWordProblemInP

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 16.109 (V. E. Shpilrain); resolution: S. Schleimer, Polynomial-time word problems, Comment. Math. Helv. 83 (2008), 741-765, Theorem 5.2 (the word problem for Aut(F_m) is polynomial time) and Remark 5.1 (choosing a different generating set alters running times by at most a multiplicative constant); Kourovka Archive, Problem 16.109 (Yes, there is), https://wrap.warwick.ac.uk/44057/.

Uses 1

Statement usesPolynomial-time word problem for Aut(Fₙ) (Kourovka 16.109)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.