Finite-state automorphisms of rooted trees

DefinitionAutomorphism of the regular rooted tree#✓fully proved

For \(d \in \mathbb{N}\), the vertices of the \(d\)-regular rooted tree are the finite words over the alphabet \(\{0, \dots, d-1\}\). A permutation \(f\) of this set of words is a tree automorphism when, for all words \(u\) and \(v\), writing \(|u|\) for the length of \(u\) and \(uv\) for the concatenation of \(u\) and \(v\), the word \(f(u)\) has length \(|u|\) and the first \(|u|\) letters of \(f(uv)\) form \(f(u)\).

def IsTreeAut {d : ℕ} (f : Equiv.Perm (List (Fin d))) : Prop :=
  ∀ u v : List (Fin d), (f u).length = u.length ∧ (f (u ++ v)).take u.length = f u

Used by 1

Used byFinite-state automorphism of the regular rooted tree

DefinitionSection of a map of the regular rooted tree at a vertex#✓fully proved

For \(d \in \mathbb{N}\), let \(f\) be a permutation of the finite words over \(\{0, \dots, d-1\}\) (the vertices of the \(d\)-regular rooted tree) and let \(u\) be a word, of length \(|u|\). The section (state) of \(f\) at \(u\) is the map sending each word \(w\) to the word obtained from \(f(uw)\) by deleting its first \(|u|\) letters, where \(uw\) is the concatenation of \(u\) and \(w\).

def treeSection {d : ℕ} (f : Equiv.Perm (List (Fin d))) (u : List (Fin d)) :
    List (Fin d) → List (Fin d) :=
  fun w => (f (u ++ w)).drop u.length

Used by 1

Used byFinite-state automorphism of the regular rooted tree

DefinitionFinite-state automorphism of the regular rooted tree#✓fully proved

For \(d \in \mathbb{N}\), a permutation \(f\) of the finite words over \(\{0, \dots, d-1\}\) is a finite-state automorphism of the \(d\)-regular rooted tree when it is an automorphism of the tree and the sections of \(f\) at all vertices \(u\) form a finite set of maps.

def IsFiniteStateAut {d : ℕ} (f : Equiv.Perm (List (Fin d))) : Prop :=
  IsTreeAut f ∧ (Set.range (treeSection f)).Finite

Uses 2 · Used by 1

Statement usesAutomorphism of the regular rooted tree · Section of a map of the regular rooted tree at a vertex

Used byKourovka Problem 16.34: conjugacy in finite-state automorphism groups

DefinitionValue of a word in the generators#✓fully proved

For \(d, k \in \mathbb{N}\), let \(g_0, \dots, g_{k-1}\) be permutations of the finite words over \(\{0, \dots, d-1\}\), and let \(w\) be a word whose letters are pairs \((i, b)\) with \(i < k\) and \(b\) a boolean. The value of \(w\) is the element of the group generated by \(g_0, \dots, g_{k-1}\) obtained by multiplying, from left to right, \(g_i\) for each letter \((i, \mathrm{true})\) and \(g_i^{-1}\) for each letter \((i, \mathrm{false})\).

def wordValue {d k : ℕ} (gens : Fin k → Equiv.Perm (List (Fin d))) (w : List (Fin k × Bool)) :
    Subgroup.closure (Set.range gens) :=
  FreeGroup.lift (fun i => ⟨gens i, Subgroup.subset_closure (Set.mem_range_self i)⟩)
    (FreeGroup.mk w)

Used by 1

Used byKourovka Problem 16.34: conjugacy in finite-state automorphism groups

DefinitionKourovka Problem 16.34: conjugacy in finite-state automorphism groups#✓fully proved

The proposition that every finitely generated group of finite-state automorphisms of a regular rooted tree has decidable conjugacy problem: for all \(d, k \in \mathbb{N}\) and all finite-state automorphisms \(g_0, \dots, g_{k-1}\) of the \(d\)-regular rooted tree, some algorithm decides, given two words in the \(g_i\) and their inverses, whether the elements they spell are conjugate in the group generated by \(g_0, \dots, g_{k-1}\).

The problem was posed by R. I. Grigorchuk, V. V. Nekrashevich and V. I. Sushchanskiĭ.

def finiteStateConjugacyDecidable : Prop :=
  ∀ (d k : ℕ) (gens : Fin k → Equiv.Perm (List (Fin d))), (∀ i, IsFiniteStateAut (gens i)) →
    ComputablePred fun uv : List (Fin k × Bool) × List (Fin k × Bool) =>
      IsConj (wordValue gens uv.1) (wordValue gens uv.2)

Uses 2 · Used by 1

Statement usesFinite-state automorphism of the regular rooted tree · Value of a word in the generators

Used byFinite-state tree automorphism groups with undecidable conjugacy problem

TheoremFinite-state tree automorphism groups with undecidable conjugacy problem#●ready to prove

The answer to Kourovka Problem 16.34 is negative: there exist \(d, k \in \mathbb{N}\) and finite-state automorphisms \(g_0, \dots, g_{k-1}\) of the \(d\)-regular rooted tree such that no algorithm decides, given two words in the \(g_i\) and their inverses, whether the elements they spell are conjugate in the group generated by \(g_0, \dots, g_{k-1}\).

Šunić and Ventura (Theorem 1.1) construct automaton groups, finitely generated groups generated by finite self-similar sets of finite-state automorphisms of a regular rooted tree, with unsolvable conjugacy problem; the Kourovka Notebook (21st issue) answers 16.34 "No, not always".

public theorem_wanted finiteStateConjugacyDecidable_refuted : ¬ finiteStateConjugacyDecidable

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 16.34 (R. I. Grigorchuk, V. V. Nekrashevich, V. I. Sushchanskiĭ); resolution: Z. Šunić and E. Ventura, The conjugacy problem in automaton groups is not solvable, J. Algebra 364 (2012), 148-154, arXiv:1010.1993, Theorem 1.1 (there exist automaton groups with unsolvable conjugacy problem; the examples are (free abelian)-by-free groups generated by finite self-similar sets of tree automorphisms); the Kourovka Notebook (21st issue) marks 16.34 solved (No, not always), https://arxiv.org/abs/1010.1993.

Uses 1

Statement usesKourovka Problem 16.34: conjugacy in finite-state automorphism groups

DefinitionAutomorphisms of the regular rooted tree (Kourovka 16.85)#✓fully proved

Let \(d\) be a natural number and let \(X^*\) be the set of finite words over the alphabet \(X = \{0, \dots, d-1\}\), the vertices of the \(d\)-regular rooted tree. A permutation \(f\) of \(X^*\) is a tree automorphism when, for all words \(u\) and \(v\), the word \(f(u)\) has the same length \(|u|\) as \(u\) and the first \(|u|\) letters of \(f(uv)\) form the word \(f(u)\), where \(uv\) denotes concatenation.

def IsTreeAut {d : ℕ} (f : Equiv.Perm (List (Fin d))) : Prop :=
  ∀ u v : List (Fin d), (f u).length = u.length ∧ (f (u ++ v)).take u.length = f u

Used by 1

Used byFinite-state automorphisms of the regular rooted tree (Kourovka 16.85)

DefinitionSection of a permutation of the tree at a vertex (Kourovka 16.85)#✓fully proved

For a natural number \(d\), let \(X^*\) be the set of finite words over \(X = \{0, \dots, d-1\}\), let \(f\) be a permutation of \(X^*\) and let \(u \in X^*\), of length \(|u|\). The section (state) of \(f\) at \(u\) is the map \(X^* \to X^*\) sending a word \(w\) to the word obtained from \(f(uw)\) by deleting its first \(|u|\) letters (all of them if it has fewer), where \(uw\) denotes concatenation.

def treeSection {d : ℕ} (f : Equiv.Perm (List (Fin d))) (u : List (Fin d)) :
    List (Fin d) → List (Fin d) :=
  fun w => (f (u ++ w)).drop u.length

Used by 1

Used byFinite-state automorphisms of the regular rooted tree (Kourovka 16.85)

DefinitionFinite-state automorphisms of the regular rooted tree (Kourovka 16.85)#✓fully proved

For a natural number \(d\), let \(X^*\) be the set of finite words over \(X = \{0, \dots, d-1\}\). A permutation \(f\) of \(X^*\) is a finite-state automorphism when it is an automorphism of the \(d\)-regular rooted tree and its sections at the vertices \(u \in X^*\) form a finite set of maps \(X^* \to X^*\).

def IsFiniteStateAut {d : ℕ} (f : Equiv.Perm (List (Fin d))) : Prop :=
  IsTreeAut f ∧ (Set.range (treeSection f)).Finite

Uses 2 · Used by 1

Statement usesAutomorphisms of the regular rooted tree (Kourovka 16.85) · Section of a permutation of the tree at a vertex (Kourovka 16.85)

Used byFaithful actions by finite-state tree automorphisms

DefinitionFaithful actions by finite-state tree automorphisms#✓fully proved

A group \(G\) acts faithfully on a regular rooted tree by finite-state automorphisms when there are a natural number \(d \ge 2\) and an injective group homomorphism \(\varphi\) from \(G\) to the group of permutations of the set of finite words over \(\{0, \dots, d-1\}\) such that \(\varphi(g)\) is a finite-state automorphism of the \(d\)-regular rooted tree for every \(g \in G\).

def ActsFaithfullyByFiniteStateAuts (G : Type) [Group G] : Prop :=
  ∃ (d : ℕ) (f : G →* Equiv.Perm (List (Fin d))), 2 ≤ d ∧ Function.Injective f ∧
    ∀ g : G, IsFiniteStateAut (f g)

Uses 1 · Used by 1

Statement usesFinite-state automorphisms of the regular rooted tree (Kourovka 16.85)

Used byFinite-state actions of free products (Kourovka Problem 16.85)

DefinitionFinite-state actions of free products (Kourovka Problem 16.85)#✓fully proved

The statement that for all groups \(G\) and \(H\), if \(G\) and \(H\) each act faithfully on a regular rooted tree by finite-state automorphisms (the two trees may have different degrees), then so does their free product \(G \ast H\).

def finiteStateFreeProduct : Prop :=
  ∀ (G H : Type) [Group G] [Group H], ActsFaithfullyByFiniteStateAuts G →
    ActsFaithfullyByFiniteStateAuts H → ActsFaithfullyByFiniteStateAuts (Monoid.Coprod G H)

Uses 1 · Used by 1

Statement usesFaithful actions by finite-state tree automorphisms

Used byFedorova–Oliynyk theorem (Kourovka Problem 16.85)

TheoremFedorova–Oliynyk theorem (Kourovka Problem 16.85)#●ready to prove

For all groups \(G\) and \(H\), if \(G\) and \(H\) each act faithfully on a regular rooted tree by finite-state automorphisms, then their free product \(G \ast H\) acts faithfully on some regular rooted tree by finite-state automorphisms.

public theorem_wanted finiteStateFreeProduct_holds : finiteStateFreeProduct

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.85 (V. I. Sushchanskiĭ); resolution: M. Fedorova and A. Oliynyk, Finite automaton actions of free products of groups, Algebra Discrete Math. 23 (2017), no. 2, 230-236, abstract (for groups G and H that act faithfully by finite state automorphisms on regular rooted trees, G ∗ H admits a faithful action by finite state automorphisms on some regular rooted tree) and Theorem 1 (FAut T_n ∗ FAut T_n is isomorphic to a subgroup of FAut T_3n); Kourovka Archive, Problem 16.85 (Yes, it can), https://admjournal.luguniv.edu.ua/index.php/adm/article/view/477.

Uses 1

Statement usesFinite-state actions of free products (Kourovka Problem 16.85)

DefinitionAutomorphisms of the regular rooted tree#✓fully proved

For a natural number \(d\), the \(d\)-regular rooted tree has as vertices the finite words over the alphabet \(\{0, \dots, d-1\}\); write \(vw\) for the concatenation of words \(v\) and \(w\). The root is the empty word and the children of a word \(v\) are the words \(vi\) for letters \(i\). A permutation \(g\) of the words is a tree automorphism when for all words \(v\) and \(w\) there is a word \(u\) of the same length as \(w\) with \(g(vw) = g(v)u\).

For a permutation of the words this says that \(g\) preserves lengths and the prefix order, so it is an automorphism of the tree as a graph.

def IsTreeAutomorphism {d : ℕ} (g : Equiv.Perm (List (Fin d))) : Prop :=
  ∀ v w : List (Fin d), ∃ u : List (Fin d), u.length = w.length ∧ g (v ++ w) = g v ++ u

Used by 1

Used byFinite-state automorphisms of a regular rooted tree

DefinitionSection of a word permutation at a vertex#✓fully proved

For a natural number \(d\), let \(g\) be a permutation of the finite words over the alphabet \(\{0, \dots, d-1\}\) and let \(v\) be a word. The section (state) of \(g\) at \(v\) is the map sending a word \(w\) to the word obtained from \(g(vw)\) by deleting its first \(|g(v)|\) letters, where \(vw\) is the concatenation of \(v\) and \(w\) and \(|g(v)|\) is the length of \(g(v)\). When \(g\) is a tree automorphism, the image of \(w\) is the word \(u\) with \(g(vw) = g(v)u\).

def treeSection {d : ℕ} (g : Equiv.Perm (List (Fin d))) (v : List (Fin d)) :
    List (Fin d) → List (Fin d) :=
  fun w => (g (v ++ w)).drop (g v).length

Used by 1

Used byFinite-state automorphisms of a regular rooted tree

DefinitionFinite-state automorphisms of a regular rooted tree#✓fully proved

For a natural number \(d\), consider the \(d\)-regular rooted tree whose vertices are the finite words over the alphabet \(\{0, \dots, d-1\}\). The group of finite-state automorphisms of this tree is the subgroup of the group of all permutations of the words generated by the tree automorphisms that have only finitely many distinct sections.

These automorphisms are closed under products and inverses, so the subgroup consists of exactly them.

def finiteStateAutomorphisms (d : ℕ) : Subgroup (Equiv.Perm (List (Fin d))) :=
  Subgroup.closure {g | IsTreeAutomorphism g ∧ (Set.range (treeSection g)).Finite}

Uses 2 · Used by 1

Statement usesAutomorphisms of the regular rooted tree · Section of a word permutation at a vertex

Used byKourovka Problem 16.86 (Sushchanskiĭ): irreducible generators of finite-state automorphism groups

DefinitionKourovka Problem 16.86 (Sushchanskiĭ): irreducible generators of finite-state automorphism groups#✓fully proved

Kourovka Problem 16.86 (Sushchanskiĭ): irreducible generators of finite-state automorphism groups. The statement that for every integer \(d \ge 2\) the group of finite-state automorphisms of the \(d\)-regular rooted tree has an irreducible system of generators: a set \(S\) of elements of the group that generates the group and no proper subset of which generates the group.

def finiteStateAutomorphismsIrreducibleGenerators : Prop :=
  ∀ d : ℕ, 2 ≤ d → ∃ S : Set (finiteStateAutomorphisms d),
    Subgroup.closure S = ⊤ ∧
      ∀ T : Set (finiteStateAutomorphisms d), T ⊂ S → Subgroup.closure T ≠ ⊤

Uses 1 · Used by 1

Statement usesFinite-state automorphisms of a regular rooted tree

Used byLavrenyuk's theorem on irreducible generators of finite-state automorphism groups

TheoremLavrenyuk's theorem on irreducible generators of finite-state automorphism groups#●ready to prove

For every integer \(d \ge 2\), the group of finite-state automorphisms of the \(d\)-regular rooted tree has an irreducible system of generators: a set \(S\) of elements of the group that generates the group and no proper subset of which generates the group.

public theorem_wanted finiteStateAutomorphismsIrreducibleGenerators_holds :
    finiteStateAutomorphismsIrreducibleGenerators

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.86 (V. I. Sushchanskiĭ); resolution: Ya. Lavrenyuk, The group of all finite-state automorphisms of a regular rooted tree has a minimal generating set, Geom. Dedicata 183 (2016), 59-67 (preprint: Minimal generating sets in wreath products, arXiv:1210.0150), arXiv:1210.0150, Theorem 3.8 (for a regular rooted tree over any alphabet of at least two letters, the group of finite-state automorphisms has a minimal generating set); Kourovka Archive, Problem 16.86 (Yes, it does), https://arxiv.org/abs/1210.0150.

Uses 1

Statement usesKourovka Problem 16.86 (Sushchanskiĭ): irreducible generators of finite-state automorphism groups

14 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.