Amenability and growth of branch groups

DefinitionVertices of a spherically homogeneous rooted tree (Kourovka 15.14 version)#✓fully proved

For a sequence \(m\) of natural numbers, the vertices of the spherically homogeneous rooted tree with branching sequence \(m\) are the finite words \(l_0 l_1 \cdots l_{k-1}\) of natural numbers with \(l_i < m(i)\) for every \(i < k\). The length of a word is its level and its prefixes are its ancestors.

def TreeVertex (m : ℕ → ℕ) : Type :=
  {l : List ℕ // ∀ (i : ℕ) (h : i < l.length), l[i] < m i}
Used by 3
Used byBranch groups (Kourovka 15.14 version) · Rigid level stabilizers (Kourovka 15.14 version) · Rigid vertex stabilizers (Kourovka 15.14 version)

DefinitionRigid vertex stabilizers (Kourovka 15.14 version)#✓fully proved

Let \(G\) be a group acting by permutations \(\rho\) on the vertices of the rooted tree with branching sequence \(m\), and let \(v\) be a vertex. The rigid vertex stabilizer of \(v\) is the set of elements \(g \in G\) whose support lies in the subtree rooted at \(v\): \(\rho(g)\) fixes every vertex \(w\) of which \(v\) is not a prefix.

def rigidVertexStabilizer {m : ℕ → ℕ} {G : Type*} [Group G] (ρ : G →* Equiv.Perm (TreeVertex m))
    (v : TreeVertex m) : Set G :=
  {g | ∀ w : TreeVertex m, ¬ v.1 <+: w.1 → ρ g w = w}
Uses 1 · Used by 1
Statement usesVertices of a spherically homogeneous rooted tree (Kourovka 15.14 version)
Used byRigid level stabilizers (Kourovka 15.14 version)

DefinitionRigid level stabilizers (Kourovka 15.14 version)#✓fully proved

Let \(G\) be a group acting by permutations \(\rho\) on the vertices of the rooted tree with branching sequence \(m\), and let \(n\) be a natural number. The \(n\)-th rigid level stabilizer of \(\rho\) is the subgroup of \(G\) generated by the rigid vertex stabilizers of all vertices at level \(n\), the words of length \(n\).

def rigidLevelStabilizer {m : ℕ → ℕ} {G : Type*} [Group G] (ρ : G →* Equiv.Perm (TreeVertex m))
    (n : ℕ) : Subgroup G :=
  Subgroup.closure (⋃ v ∈ {v : TreeVertex m | v.1.length = n}, rigidVertexStabilizer ρ v)
Uses 2 · Used by 1
Statement usesVertices of a spherically homogeneous rooted tree (Kourovka 15.14 version) · Rigid vertex stabilizers (Kourovka 15.14 version)
Used byBranch groups (Kourovka 15.14 version)

DefinitionBranch groups (Kourovka 15.14 version)#✓fully proved

A group \(G\) is a branch group (Kourovka 15.12) if there are a sequence \(m\) of natural numbers with \(m(i) \ge 2\) for every \(i\) and an action \(\rho\) of \(G\) by permutations of the vertices of the spherically homogeneous rooted tree with branching sequence \(m\) such that: \(\rho\) is faithful; each \(\rho(g)\) is a tree automorphism, that is, for all vertices \(v\) and \(w\), \(v\) is a prefix of \(w\) if and only if \(\rho(g)(v)\) is a prefix of \(\rho(g)(w)\); the action is level-transitive, that is, for any two vertices \(v\) and \(w\) of the same level some \(g \in G\) has \(\rho(g)(v) = w\); and for every \(n \in \mathbb{N}\) the \(n\)-th rigid level stabilizer of \(\rho\) has finite index in \(G\).

def IsBranchGroup (G : Type*) [Group G] : Prop :=
  ∃ (m : ℕ → ℕ) (_ : ∀ i, 2 ≤ m i) (ρ : G →* Equiv.Perm (TreeVertex m)),
    Function.Injective ρ ∧
    (∀ (g : G) (v w : TreeVertex m), v.1 <+: w.1 ↔ (ρ g v).1 <+: (ρ g w).1) ∧
    (∀ v w : TreeVertex m, v.1.length = w.1.length → ∃ g : G, ρ g v = w) ∧
    ∀ n : ℕ, (rigidLevelStabilizer ρ n).FiniteIndex
Uses 2 · Used by 4
Statement usesVertices of a spherically homogeneous rooted tree (Kourovka 15.14 version) · Rigid level stabilizers (Kourovka 15.14 version)
Used byKourovka Problem 15.14(c): branch groups containing free subgroups · Kourovka Problem 15.14(d): branch groups of exponential growth · Kourovka Problem 15.14(a): non-amenable branch groups · Kourovka Problem 15.14(b): non-amenable branch groups without free subgroups

DefinitionGrowth rate of a finitely generated group#✓fully proved

The growth rate ω(G, P) = limsup β_P(n)^(1/n) of a finite generating family P, where β_P(n) is the number of elements that are products of at most n generators and their inverses.

noncomputable def growthRate {G : Type*} [Group G] {k : ℕ} (P : Group.Generators G (Fin k)) : ℝ :=
  Filter.limsup (fun n : ℕ => (Nat.card {g : G // P.wordLength g ≤ n} : ℝ) ^ ((1 : ℝ) / n))
    Filter.atTop
Used by 1
Used byGroups of exponential growth

DefinitionGroups of exponential growth#✓fully proved

A group \(G\) has exponential growth when it is finitely generated and every finite generating family \(P\) of \(G\) has growth rate \(\omega(G, P) > 1\).

def HasExponentialGrowth (G : Type*) [Group G] : Prop :=
  Group.FG G ∧ ∀ (k : ℕ) (P : Group.Generators G (Fin k)), 1 < growthRate P
Uses 1 · Used by 1
Statement usesGrowth rate of a finitely generated group
Used byKourovka Problem 15.14(d): branch groups of exponential growth

DefinitionGroups containing a free subgroup of rank two#✓fully proved

A group \(G\) contains a free subgroup of rank \(2\) when there is an injective group homomorphism from the free group \(F_2\) on two generators into \(G\).

def ContainsFreeGroupRankTwo (G : Type*) [Group G] : Prop :=
  ∃ f : FreeGroup (Fin 2) →* G, Function.Injective f
Used by 2
Used byKourovka Problem 15.14(c): branch groups containing free subgroups · Kourovka Problem 15.14(b): non-amenable branch groups without free subgroups

DefinitionKourovka Problem 15.14(a): non-amenable branch groups#✓fully proved

The statement that there exists a finitely generated branch group that is not amenable.

def fgNonamenableBranchGroup : Prop :=
  ∃ (G : Type) (_ : Group G), Group.FG G ∧ IsBranchGroup G ∧ ¬ IsAmenable G
Uses 2 · Used by 1
Statement usesAmenable group (Følner condition) · Branch groups (Kourovka 15.14 version)
Used byNon-amenable branch groups exist (Kourovka 15.14(a))

DefinitionKourovka Problem 15.14(b): non-amenable branch groups without free subgroups#✓fully proved

The statement that there exists a finitely generated branch group that is not amenable and contains no free subgroup of rank \(2\).

def fgNonamenableBranchGroupWithoutFreeSubgroup : Prop :=
  ∃ (G : Type) (_ : Group G), Group.FG G ∧ IsBranchGroup G ∧ ¬ IsAmenable G ∧
    ¬ ContainsFreeGroupRankTwo G
Uses 3 · Used by 1
Statement usesAmenable group (Følner condition) · Groups containing a free subgroup of rank two · Branch groups (Kourovka 15.14 version)
Used byNon-amenable branch groups without free subgroups exist (Kourovka 15.14(b))

DefinitionKourovka Problem 15.14(c): branch groups containing free subgroups#✓fully proved

The statement that there exists a finitely generated branch group that contains a free subgroup of rank \(2\).

def fgBranchGroupContainingFreeGroup : Prop :=
  ∃ (G : Type) (_ : Group G), Group.FG G ∧ IsBranchGroup G ∧ ContainsFreeGroupRankTwo G
Uses 2 · Used by 1
Statement usesGroups containing a free subgroup of rank two · Branch groups (Kourovka 15.14 version)
Used byBranch groups containing free subgroups exist (Kourovka 15.14(c))

DefinitionKourovka Problem 15.14(d): branch groups of exponential growth#✓fully proved

The statement that there exists a finitely generated branch group of exponential growth.

def fgBranchGroupOfExponentialGrowth : Prop :=
  ∃ (G : Type) (_ : Group G), Group.FG G ∧ IsBranchGroup G ∧ HasExponentialGrowth G
Uses 2 · Used by 1
Statement usesGroups of exponential growth · Branch groups (Kourovka 15.14 version)
Used byBranch groups of exponential growth exist (Kourovka 15.14(d))

TheoremNon-amenable branch groups exist (Kourovka 15.14(a))#●ready to prove

There is a finitely generated branch group that is not amenable.

The Kourovka Archive answers 15.14(a) "Such groups do exist" (Sidki and Wilson): their finitely generated branch groups contain free subgroups of rank \(2\) and so are non-amenable.

public theorem_wanted fgNonamenableBranchGroup_holds : fgNonamenableBranchGroup
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 15.14 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić); parts (a), (c), (d) in the Archive of Solved Problems, part (b) in the main list; resolution: S. Sidki and J. S. Wilson, Free subgroups of branch groups, Arch. Math. 80 (2003), no. 5, 458-463 (parts a, c, d); S. Kionke and E. Schesler, Realizing residually finite groups as subgroups of branch groups, Bull. London Math. Soc. 56 (2024), no. 2, 536-550, arXiv:2212.07165 (part b), Kourovka Archive, Problem 15.14 (a), (c), (d): such groups do exist (Sidki and Wilson's finitely generated branch groups contain free subgroups of rank 2, the positive answer recorded under Question 15 of Bartholdi, Grigorchuk and Šunić, Branch groups); Kourovka Notebook (21st issue), Problem 15.14 (b), and Kionke and Schesler, Corollary 1.2: there is a finitely generated non-amenable torsion branch group, https://arxiv.org/abs/2212.07165.
Uses 1
Statement usesKourovka Problem 15.14(a): non-amenable branch groups

TheoremNon-amenable branch groups without free subgroups exist (Kourovka 15.14(b))#●ready to prove

There is a finitely generated branch group that is not amenable and contains no free subgroup of rank \(2\).

The Kourovka Notebook (21st issue) marks 15.14(b) solved: Kionke and Schesler constructed finitely generated non-amenable torsion branch groups, and a torsion group contains no free subgroup of rank \(2\).

public theorem_wanted fgNonamenableBranchGroupWithoutFreeSubgroup_holds :
    fgNonamenableBranchGroupWithoutFreeSubgroup
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 15.14 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić); parts (a), (c), (d) in the Archive of Solved Problems, part (b) in the main list; resolution: S. Sidki and J. S. Wilson, Free subgroups of branch groups, Arch. Math. 80 (2003), no. 5, 458-463 (parts a, c, d); S. Kionke and E. Schesler, Realizing residually finite groups as subgroups of branch groups, Bull. London Math. Soc. 56 (2024), no. 2, 536-550, arXiv:2212.07165 (part b), Kourovka Archive, Problem 15.14 (a), (c), (d): such groups do exist (Sidki and Wilson's finitely generated branch groups contain free subgroups of rank 2, the positive answer recorded under Question 15 of Bartholdi, Grigorchuk and Šunić, Branch groups); Kourovka Notebook (21st issue), Problem 15.14 (b), and Kionke and Schesler, Corollary 1.2: there is a finitely generated non-amenable torsion branch group, https://arxiv.org/abs/2212.07165.
Uses 1
Statement usesKourovka Problem 15.14(b): non-amenable branch groups without free subgroups

TheoremBranch groups containing free subgroups exist (Kourovka 15.14(c))#●ready to prove

There is a finitely generated branch group that contains a free subgroup of rank \(2\).

The Kourovka Archive answers 15.14(c) "Such groups do exist": Sidki and Wilson constructed finitely generated branch groups containing free subgroups of rank \(2\).

public theorem_wanted fgBranchGroupContainingFreeGroup_holds : fgBranchGroupContainingFreeGroup
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 15.14 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić); parts (a), (c), (d) in the Archive of Solved Problems, part (b) in the main list; resolution: S. Sidki and J. S. Wilson, Free subgroups of branch groups, Arch. Math. 80 (2003), no. 5, 458-463 (parts a, c, d); S. Kionke and E. Schesler, Realizing residually finite groups as subgroups of branch groups, Bull. London Math. Soc. 56 (2024), no. 2, 536-550, arXiv:2212.07165 (part b), Kourovka Archive, Problem 15.14 (a), (c), (d): such groups do exist (Sidki and Wilson's finitely generated branch groups contain free subgroups of rank 2, the positive answer recorded under Question 15 of Bartholdi, Grigorchuk and Šunić, Branch groups); Kourovka Notebook (21st issue), Problem 15.14 (b), and Kionke and Schesler, Corollary 1.2: there is a finitely generated non-amenable torsion branch group, https://arxiv.org/abs/2212.07165.
Uses 1
Statement usesKourovka Problem 15.14(c): branch groups containing free subgroups

TheoremBranch groups of exponential growth exist (Kourovka 15.14(d))#●ready to prove

There is a finitely generated branch group of exponential growth.

The Kourovka Archive answers 15.14(d) "Such groups do exist" (Sidki and Wilson); a finitely generated group containing a free subgroup of rank \(2\) has exponential growth.

public theorem_wanted fgBranchGroupOfExponentialGrowth_holds : fgBranchGroupOfExponentialGrowth
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 15.14 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić); parts (a), (c), (d) in the Archive of Solved Problems, part (b) in the main list; resolution: S. Sidki and J. S. Wilson, Free subgroups of branch groups, Arch. Math. 80 (2003), no. 5, 458-463 (parts a, c, d); S. Kionke and E. Schesler, Realizing residually finite groups as subgroups of branch groups, Bull. London Math. Soc. 56 (2024), no. 2, 536-550, arXiv:2212.07165 (part b), Kourovka Archive, Problem 15.14 (a), (c), (d): such groups do exist (Sidki and Wilson's finitely generated branch groups contain free subgroups of rank 2, the positive answer recorded under Question 15 of Bartholdi, Grigorchuk and Šunić, Branch groups); Kourovka Notebook (21st issue), Problem 15.14 (b), and Kionke and Schesler, Corollary 1.2: there is a finitely generated non-amenable torsion branch group, https://arxiv.org/abs/2212.07165.
Uses 1
Statement usesKourovka Problem 15.14(d): branch groups of exponential growth
11 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.