Andrews–Curtis moves

DefinitionElementary Andrews–Curtis moves#✓fully proved

Let \(F_n\) be the free group on \(n\) generators. A map \(f \colon F_n^n \to F_n^n\) on \(n\)-tuples \((u_1, \dots, u_n)\) of elements of \(F_n\) is an elementary Andrews–Curtis move if there is an index \(i\) such that \(f\) replaces the entry \(u_i\) of every tuple by \(u_i u_j\), \(u_i u_j^{-1}\), \(u_j u_i\) or \(u_j^{-1} u_i\) for a fixed index \(j \ne i\), or by \(u_i^{-1}\), or by \(w u_i w^{-1}\) for a fixed \(w \in F_n\), and leaves all other entries unchanged.

def IsACMove (n : ℕ) (f : (Fin n → FreeGroup (Fin n)) → (Fin n → FreeGroup (Fin n))) : Prop :=
  (∃ i j : Fin n, i ≠ j ∧
    (f = (fun u => Function.update u i (u i * u j)) ∨
      f = (fun u => Function.update u i (u i * (u j)⁻¹)) ∨
      f = (fun u => Function.update u i (u j * u i)) ∨
      f = (fun u => Function.update u i ((u j)⁻¹ * u i)))) ∨
  (∃ i : Fin n, f = fun u => Function.update u i (u i)⁻¹) ∨
  (∃ (i : Fin n) (w : FreeGroup (Fin n)), f = fun u => Function.update u i (w * u i * w⁻¹))
Used by 1

DefinitionThe Andrews–Curtis group \(AC_n\)#✓fully proved

For \(n \in \mathbb{N}\) let \(F_n\) be the free group on \(n\) generators. The Andrews–Curtis group \(AC_n\) is the subgroup of the group of permutations of the set \(F_n^n\) of \(n\)-tuples \((u_1, \dots, u_n)\) of elements of \(F_n\) generated by the elementary Andrews–Curtis moves that are permutations: \(u_i \mapsto u_i u_j^{\pm 1}\) and \(u_i \mapsto u_j^{\pm 1} u_i\) for indices \(i \ne j\), \(u_i \mapsto u_i^{-1}\), and \(u_i \mapsto w u_i w^{-1}\) for \(w \in F_n\), all other entries unchanged. Viewing a tuple as the relators of a balanced presentation \(\langle x_1, \dots, x_n \mid u_1, \dots, u_n \rangle\), these are the Nielsen transformations of the relator tuple together with conjugations of relators.

def andrewsCurtisGroup (n : ℕ) : Subgroup (Equiv.Perm (Fin n → FreeGroup (Fin n))) :=
  Subgroup.closure {σ | IsACMove n σ}
Uses 1 · Used by 2

DefinitionKourovka Problem 18.89 for \(n = 2\)#✓fully proved

The proposition, asked by J. Swan and A. Lisitsa, that the Andrews–Curtis group \(AC_2\) (the subgroup of the permutation group of the set of pairs of elements of the free group \(F_2\) generated by the elementary Andrews–Curtis moves) is finitely presented.

def andrewsCurtisTwoFinitelyPresented : Prop :=
  Group.IsFinitelyPresented (andrewsCurtisGroup 2)
Uses 1 · Used by 1

DefinitionKourovka Problem 18.89 for \(n \ge 3\)#✓fully proved

The proposition that for every \(n \ge 3\) the Andrews–Curtis group \(AC_n\) (the subgroup of the permutation group of the set of \(n\)-tuples of elements of the free group \(F_n\) generated by the elementary Andrews–Curtis moves) is finitely presented.

def andrewsCurtisFinitelyPresentedOfThreeLe : Prop :=
  ∀ n : ℕ, 3 ≤ n → Group.IsFinitelyPresented (andrewsCurtisGroup n)
Uses 1 · Used by 1

TheoremThe Andrews–Curtis group \(AC_2\) is not finitely presented (Kourovka 18.89)#●ready to prove

The Andrews–Curtis group \(AC_2\), the subgroup of the permutation group of the set \(F_2^2\) of pairs of elements of the free group \(F_2\) generated by the elementary Andrews–Curtis moves, is not finitely presented.

The Kourovka Notebook (21st issue) records this, citing Krstić–McCool (1997) and Roman'kov (2023), who also shows that the group of moves on all relator tuples is isomorphic to the Andrews–Curtis group of \(F_2\).

public theorem_wanted andrewsCurtisTwoFinitelyPresented_refuted :
    ¬ andrewsCurtisTwoFinitelyPresented
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 18.89 (J. Swan, A. Lisitsa); resolution: S. Krstić and J. McCool, J. London Math. Soc. (2) 56 (1997), no. 2, 264-274; V. A. Roman'kov, On the Andrews-Curtis groups: non-finite presentability, preprint, arXiv:2305.11838 (2023); G. Kiralis, S. Krstić and J. McCool, Proc. London Math. Soc. (3) 73 (1996), no. 3, 575-622; M. Ershov, letter of 16 October 2025, AC_2 is not finitely presented (Krstić-McCool, Theorem 1; Roman'kov, Theorem B: AC(F_2) ≅ A_{2,2} is not finitely presented); AC_n, n ≥ 3, is finitely presented by Kiralis-Krstić-McCool, Theorem 3.1, since AC_n ≅ A_{n,n} ≅ Φ_n(F_n) (Ershov's letter); the Kourovka Notebook (21st issue) marks 18.89 solved, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2025/11/kourovka1889.pdf.
Uses 1

TheoremThe Andrews–Curtis groups \(AC_n\) are finitely presented for \(n \ge 3\) (Kourovka 18.89)#●ready to prove

For every \(n \ge 3\), the Andrews–Curtis group \(AC_n\), the subgroup of the permutation group of the set \(F_n^n\) of \(n\)-tuples of elements of the free group \(F_n\) generated by the elementary Andrews–Curtis moves, is finitely presented.

The Kourovka Notebook (21st issue) records this, deducing it from Kiralis–Krstić–McCool (1996), Theorem 3.1, through an isomorphism observed by M. Ershov (letter of 2025, using Roman'kov's Lemma 3.2).

public theorem_wanted andrewsCurtisFinitelyPresentedOfThreeLe_holds :
    andrewsCurtisFinitelyPresentedOfThreeLe
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 18.89 (J. Swan, A. Lisitsa); resolution: S. Krstić and J. McCool, J. London Math. Soc. (2) 56 (1997), no. 2, 264-274; V. A. Roman'kov, On the Andrews-Curtis groups: non-finite presentability, preprint, arXiv:2305.11838 (2023); G. Kiralis, S. Krstić and J. McCool, Proc. London Math. Soc. (3) 73 (1996), no. 3, 575-622; M. Ershov, letter of 16 October 2025, AC_2 is not finitely presented (Krstić-McCool, Theorem 1; Roman'kov, Theorem B: AC(F_2) ≅ A_{2,2} is not finitely presented); AC_n, n ≥ 3, is finitely presented by Kiralis-Krstić-McCool, Theorem 3.1, since AC_n ≅ A_{n,n} ≅ Φ_n(F_n) (Ershov's letter); the Kourovka Notebook (21st issue) marks 18.89 solved, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2025/11/kourovka1889.pdf.
Uses 1
4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.