Maximal subgroups of branch groups

DefinitionVertices of the spherically homogeneous rooted tree (Kourovka 15.15)#✓fully proved

For a branching sequence \(m \colon \mathbb{N} \to \mathbb{N}\), the vertices of the spherically homogeneous rooted tree are the finite words \((x_0, \dots, x_{k-1})\) of natural numbers with \(x_i < m(i)\) for every \(i < k\). The length \(k\) 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 group (Kourovka 15.15) · Rigid level stabilizer (Kourovka 15.15) · Rigid vertex stabilizer (Kourovka 15.15)

DefinitionRigid vertex stabilizer (Kourovka 15.15)#✓fully proved

Let \(\rho\) be a homomorphism from a group \(G\) to the permutations of the vertices of the tree with branching sequence \(m\), and let \(v\) be a vertex. The rigid vertex stabilizer of \(v\) is the set of \(g \in G\) such that \(\rho(g)\) fixes every vertex \(w\) of which \(v\) is not a prefix, that is, every vertex outside the subtree rooted at \(v\).

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 the spherically homogeneous rooted tree (Kourovka 15.15)

Used byRigid level stabilizer (Kourovka 15.15)

DefinitionRigid level stabilizer (Kourovka 15.15)#✓fully proved

Let \(\rho\) be a homomorphism from a group \(G\) to the permutations of the vertices of the tree with branching sequence \(m\), and let \(n\) be a natural number. The \(n\)-th rigid level stabilizer is the subgroup of \(G\) generated by the rigid vertex stabilizers of all vertices at level \(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 the spherically homogeneous rooted tree (Kourovka 15.15) · Rigid vertex stabilizer (Kourovka 15.15)

Used byBranch group (Kourovka 15.15)

DefinitionBranch group (Kourovka 15.15)#✓fully proved

A group \(G\) is a branch group if there are a sequence \(m \colon \mathbb{N} \to \mathbb{N}\) with \(m(i) \ge 2\) for all \(i\) and an injective homomorphism \(\rho\) from \(G\) to the permutations of the vertices of the spherically homogeneous rooted tree with branching sequence \(m\) such that each \(\rho(g)\) is a tree automorphism (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 (for any two vertices \(v\) and \(w\) at the same level some \(g \in G\) has \(\rho(g)(v) = w\)), and for every \(n\) the \(n\)-th rigid level stabilizer 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 1

Statement usesVertices of the spherically homogeneous rooted tree (Kourovka 15.15) · Rigid level stabilizer (Kourovka 15.15)

Used byKourovka 15.15: maximal subgroups of finitely generated branch groups have finite index

DefinitionKourovka 15.15: maximal subgroups of finitely generated branch groups have finite index#✓fully proved

The statement (L. Bartholdi, R. I. Grigorchuk, Z. Šunić) that every maximal subgroup of every finitely generated branch group has finite index.

def branchGroupMaximalSubgroupsFiniteIndex : Prop :=
  ∀ (G : Type) [Group G], Group.FG G → IsBranchGroup G →
    ∀ M : Subgroup G, IsCoatom M → M.FiniteIndex

Uses 1 · Used by 1

Statement usesBranch group (Kourovka 15.15)

Used byA finitely generated branch group with a maximal subgroup of infinite index

TheoremA finitely generated branch group with a maximal subgroup of infinite index#●ready to prove

The Kourovka 15.15 statement that every maximal subgroup of a finitely generated branch group has finite index is false: some finitely generated branch group has a maximal subgroup of infinite index.

public theorem_wanted branchGroupMaximalSubgroupsFiniteIndex_refuted :
    ¬ branchGroupMaximalSubgroupsFiniteIndex

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 15.15 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić); resolution: I. V. Bondarenko, Finite generation of iterated wreath products, Arch. Math. (Basel) 95 (2010), no. 4, 301-308, arXiv:1002.0320, abstract and the example after Corollary 3 (a finitely generated branch group with maximal subgroups of infinite index, answering Question 14 of Bartholdi, Grigorchuk and Šunić, Branch groups); Kourovka Archive, Problem 15.15 (answer: No, not necessarily), https://arxiv.org/abs/1002.0320.

Uses 1

Statement usesKourovka 15.15: maximal subgroups of finitely generated branch groups have finite index

StructureRooted tree given by levels#✓fully proved

A locally finite rooted tree is given by finite sets \(V_n\) for \(n \ge 0\), the vertices at level \(n\), where \(V_0\) consists of the root alone, together with parent maps \(V_{n+1} \to V_n\), such that every vertex has at least two children: for every \(v \in V_n\) there are distinct \(x, y \in V_{n+1}\) whose parent is \(v\).

structure RootedTree where
  /-- The vertices at level `n`. -/
  Vertex : ℕ → Type
  /-- Every level is finite. -/
  levelFinite : ∀ n, Finite (Vertex n)
  /-- Level `0` is the root alone. -/
  rootUnique : Unique (Vertex 0)
  /-- The parent of a vertex at level `n + 1`. -/
  parent : ∀ n, Vertex (n + 1) → Vertex n
  /-- Every vertex has at least two children. -/
  twoChildren : ∀ n (v : Vertex n), ∃ x y : Vertex (n + 1), parent n x = v ∧ parent n y = v ∧ x ≠ y

Used by 6

Used byBranch action · Branch group · Descendants in a rooted tree · Rigid vertex stabilizer · Faithful level-transitive action on a rooted tree · Rigid stabilizer of a level

InductiveDescendants in a rooted tree#✓fully proved

For vertices \(v\) at level \(n\) and \(w\) at level \(m\) of a rooted tree \(T\), \(w\) is a descendant of \(v\) when \(w\) is reached from \(v\) by moving from a vertex to one of its children zero or more times: \(v\) is a descendant of itself, and a vertex at level \(k + 1\) is a descendant of \(v\) whenever its parent is.

inductive RootedTree.IsDescendant (T : RootedTree) : {n m : ℕ} → T.Vertex n → T.Vertex m → Prop
  | refl {n} (v : T.Vertex n) : RootedTree.IsDescendant T v v
  | child {n m} {v : T.Vertex n} (w : T.Vertex (m + 1))
      (h : RootedTree.IsDescendant T v (T.parent m w)) : RootedTree.IsDescendant T v w

Uses 1 · Used by 1

Statement usesRooted tree given by levels

Used byRigid vertex stabilizer

StructureFaithful level-transitive action on a rooted tree#✓fully proved

Let \(T\) be a rooted tree with vertex sets \(V_n\) at the levels \(n \ge 0\) and parent maps \(V_{n+1} \to V_n\), and let \(G\) be a group. A faithful level-transitive action of \(G\) on \(T\) consists of an action of \(G\) on each level \(V_n\) by permutations, that is, a homomorphism \(G \to \mathrm{Sym}(V_n)\) for every \(n\), such that the actions commute with the parent maps (so \(G\) acts by tree automorphisms), only the identity of \(G\) fixes every vertex of \(T\), and \(G\) acts transitively on every level \(V_n\).

structure LevelTransitiveFaithfulAction (T : RootedTree) (G : Type) [Group G] where
  /-- The action on level `n`. -/
  levelAction : ∀ n, G →* Equiv.Perm (T.Vertex n)
  /-- The level actions commute with the parent maps, so `G` acts by tree automorphisms. -/
  parent_equivariant : ∀ (g : G) (n : ℕ) (w : T.Vertex (n + 1)),
    T.parent n (levelAction (n + 1) g w) = levelAction n g (T.parent n w)
  /-- Only `1` fixes every vertex. -/
  faithful : ∀ g : G, (∀ n (v : T.Vertex n), levelAction n g v = v) → g = 1
  /-- `G` is transitive on every level. -/
  level_transitive : ∀ n (v w : T.Vertex n), ∃ g : G, levelAction n g v = w

Uses 1 · Used by 4

Statement usesRooted tree given by levels

Used byBranch action · Branch group · Rigid vertex stabilizer · Rigid stabilizer of a level

DefinitionRigid vertex stabilizer#✓fully proved

Given a faithful level-transitive action of a group \(G\) on a rooted tree \(T\) and a vertex \(v\) of \(T\), an element \(g \in G\) lies in the rigid stabilizer of \(v\) when \(g\) fixes every vertex of \(T\) that is not a descendant of \(v\).

def LevelTransitiveFaithfulAction.IsRigidAt {T : RootedTree} {G : Type} [Group G]
    (A : LevelTransitiveFaithfulAction T G) {n : ℕ} (v : T.Vertex n) (g : G) : Prop :=
  ∀ {m : ℕ} (w : T.Vertex m), ¬ T.IsDescendant v w → A.levelAction m g w = w

Uses 3 · Used by 1

Statement usesFaithful level-transitive action on a rooted tree · Rooted tree given by levels · Descendants in a rooted tree

Used byRigid stabilizer of a level

DefinitionRigid stabilizer of a level#✓fully proved

Given a faithful level-transitive action of a group \(G\) on a rooted tree \(T\) and a level \(n\), the rigid stabilizer of level \(n\) is the subgroup of \(G\) generated by the rigid stabilizers of all vertices of \(T\) at level \(n\).

def LevelTransitiveFaithfulAction.rigidLevelStabilizer {T : RootedTree} {G : Type} [Group G]
    (A : LevelTransitiveFaithfulAction T G) (n : ℕ) : Subgroup G :=
  Subgroup.closure {g : G | ∃ v : T.Vertex n, A.IsRigidAt v g}

Uses 3 · Used by 1

Statement usesFaithful level-transitive action on a rooted tree · Rigid vertex stabilizer · Rooted tree given by levels

Used byBranch action

DefinitionBranch action#✓fully proved

A faithful level-transitive action of a group \(G\) on a rooted tree \(T\) is a branch action when, for every level \(n\), the rigid stabilizer of level \(n\) has finite index in \(G\).

def LevelTransitiveFaithfulAction.IsBranchAction {T : RootedTree} {G : Type} [Group G]
    (A : LevelTransitiveFaithfulAction T G) : Prop :=
  ∀ n : ℕ, (A.rigidLevelStabilizer n).FiniteIndex

Uses 3 · Used by 1

Statement usesFaithful level-transitive action on a rooted tree · Rigid stabilizer of a level · Rooted tree given by levels

Used byBranch group

DefinitionBranch group#✓fully proved

A group \(G\) is a branch group when there exist a rooted tree \(T\) (locally finite, with every vertex having at least two children) and a faithful level-transitive action of \(G\) on \(T\) by tree automorphisms that is a branch action.

def IsBranchGroup (G : Type) [Group G] : Prop :=
  ∃ (T : RootedTree) (A : LevelTransitiveFaithfulAction T G), A.IsBranchAction

Uses 3 · Used by 1

Statement usesFaithful level-transitive action on a rooted tree · Branch action · Rooted tree given by levels

Used byKourovka 20.101: finite-index maximal subgroups of finitely generated branch groups are normal

DefinitionKourovka 20.101: finite-index maximal subgroups of finitely generated branch groups are normal#✓fully proved

Kourovka 20.101: finite-index maximal subgroups of finitely generated branch groups are normal. The statement (A. Thillaisundaram) that in every finitely generated branch group every maximal subgroup of finite index is normal.

def branchGroupFiniteIndexMaximalSubgroupsNormal : Prop :=
  ∀ (G : Type) [Group G], Group.FG G → IsBranchGroup G →
    ∀ M : Subgroup G, IsCoatom M → M.FiniteIndex → M.Normal

Uses 1 · Used by 1

Statement usesBranch group

Used byA finitely generated branch group with a non-normal maximal subgroup of finite index

TheoremA finitely generated branch group with a non-normal maximal subgroup of finite index#●ready to prove

The Kourovka 20.101 statement that every maximal subgroup of finite index of a finitely generated branch group is normal is false: some finitely generated branch group has a maximal subgroup of finite index that is not normal.

Garciarena and Petschick (2024, Theorem 4.1) construct a finitely generated branch group all of whose maximal subgroups have finite index, one of which is not normal.

public theorem_wanted branchGroupFiniteIndexMaximalSubgroupsNormal_refuted :
    ¬ branchGroupFiniteIndexMaximalSubgroupsNormal

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 20.101 (A. Thillaisundaram); resolution: M. E. Garciarena and J. M. Petschick, Maximal subgroups in torsion branch groups, preprint, arXiv:2410.06783 (2024); P. M. Neumann, Illinois J. Math. 30 (1986), 301-316, Garciarena-Petschick, Theorem 4.1: there exists a finitely generated branch group that is in MF (all maximal subgroups of finite index) but not in MN (all maximal subgroups normal); the Kourovka Notebook (21st issue) marks 20.101 solved, "No, not necessarily" (P. Neumann), https://arxiv.org/abs/2410.06783.

Uses 1

Statement usesKourovka 20.101: finite-index maximal subgroups of finitely generated branch groups are normal

13 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.