Just infinite groups

DefinitionJust infinite groups#✓fully proved

A group \(G\) is just infinite if it is infinite and every nontrivial normal subgroup of \(G\) has finite index in \(G\).

def IsJustInfinite (G : Type*) [Group G] : Prop :=
  Infinite G ∧ ∀ N : Subgroup G, N.Normal → N ≠ ⊥ → N.FiniteIndex

Used by 1

Used byHereditarily just infinite groups

DefinitionResidually finite groups#✓fully proved

A group \(G\) is residually finite if every element \(g \ne 1\) of \(G\) lies outside some normal subgroup of finite index in \(G\).

def IsResiduallyFinite (G : Type*) [Group G] : Prop :=
  ∀ g : G, g ≠ 1 → ∃ N : Subgroup G, N.Normal ∧ N.FiniteIndex ∧ g ∉ N

Used by 1

Used byHereditarily just infinite groups

DefinitionHereditarily just infinite groups#✓fully proved

A group \(G\) is hereditarily just infinite (in the sense of Kourovka 15.18) if it is infinite, residually finite, and every nontrivial normal subgroup of \(G\), viewed as a group in its own right, is just infinite.

def IsHereditarilyJustInfinite (G : Type*) [Group G] : Prop :=
  Infinite G ∧ IsResiduallyFinite G ∧ ∀ N : Subgroup G, N.Normal → N ≠ ⊥ → IsJustInfinite N

Uses 2 · Used by 2

Statement usesJust infinite groups · Residually finite groups

Used byKourovka 15.18(b): linearity of hereditarily just infinite groups · Kourovka 15.18(a): hereditarily just infinite torsion groups

DefinitionKourovka 15.18(a): hereditarily just infinite torsion groups#✓fully proved

The proposition that there exists a finitely generated hereditarily just infinite group \(G\) that is a torsion group, i.e. every element of \(G\) has finite order.

def fgHereditarilyJustInfiniteTorsionGroup : Prop :=
  ∃ (G : Type) (_ : Group G), Group.FG G ∧ IsHereditarilyJustInfinite G ∧ ∀ g : G, IsOfFinOrder g

Uses 1 · Used by 1

Statement usesHereditarily just infinite groups

Used byFinitely generated hereditarily just infinite torsion groups exist

DefinitionKourovka 15.18(b): linearity of hereditarily just infinite groups#✓fully proved

The proposition that every finitely generated hereditarily just infinite group \(G\) is linear, i.e. that there are a field \(K\), a natural number \(n\) and an injective group homomorphism \(G \to \mathrm{GL}_n(K)\).

def fgHereditarilyJustInfiniteIsLinear : Prop :=
  ∀ (G : Type) [Group G], Group.FG G → IsHereditarilyJustInfinite G →
    ∃ (K : Type) (_ : Field K) (n : ℕ) (ρ : G →* Matrix.GeneralLinearGroup (Fin n) K),
      Function.Injective ρ

Uses 1 · Used by 1

Statement usesHereditarily just infinite groups

Used byNot every finitely generated hereditarily just infinite group is linear

TheoremFinitely generated hereditarily just infinite torsion groups exist#●ready to prove

There is a finitely generated hereditarily just infinite group \(G\) in which every element has finite order.

This answers Kourovka 15.18(a) positively, as recorded in the Kourovka Archive ("Yes, such groups exist"; Ershov and Jaikin-Zapirain).

public theorem_wanted fgHereditarilyJustInfiniteTorsionGroup_holds :
    fgHereditarilyJustInfiniteTorsionGroup

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.18 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić); resolution: M. Ershov and A. Jaikin-Zapirain, Groups of positive weighted deficiency and their applications, J. Reine Angew. Math. 677 (2013), 71-134, arXiv:1007.1489, Kourovka Archive, Problem 15.18 ((a) Yes, such groups exist; (b) No, not every); the abstract constructs finitely generated residually finite p-torsion groups and shows that every group of positive weighted deficiency has a hereditarily just infinite quotient, https://arxiv.org/abs/1007.1489.

Uses 1

Statement usesKourovka 15.18(a): hereditarily just infinite torsion groups

TheoremNot every finitely generated hereditarily just infinite group is linear#●ready to prove

There is a finitely generated hereditarily just infinite group \(G\) such that for no field \(K\) and no natural number \(n\) is there an injective group homomorphism \(G \to \mathrm{GL}_n(K)\).

This answers Kourovka 15.18(b) negatively, as recorded in the Kourovka Archive ("No, not every"; Ershov and Jaikin-Zapirain). As the problem notes, a positive answer to (b) would contradict (a): a finitely generated linear torsion group is finite, while a just infinite group is infinite.

public theorem_wanted fgHereditarilyJustInfiniteIsLinear_refuted :
    ¬ fgHereditarilyJustInfiniteIsLinear

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.18 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić); resolution: M. Ershov and A. Jaikin-Zapirain, Groups of positive weighted deficiency and their applications, J. Reine Angew. Math. 677 (2013), 71-134, arXiv:1007.1489, Kourovka Archive, Problem 15.18 ((a) Yes, such groups exist; (b) No, not every); the abstract constructs finitely generated residually finite p-torsion groups and shows that every group of positive weighted deficiency has a hereditarily just infinite quotient, https://arxiv.org/abs/1007.1489.

Uses 1

Statement usesKourovka 15.18(b): linearity of hereditarily just infinite groups

DefinitionVertices of a spherically homogeneous rooted tree#✓fully proved

For a sequence \(m : \mathbb{N} \to \mathbb{N}\) of branching indices, the vertices of the spherically homogeneous rooted tree with branching sequence \(m\) are the finite words \(x_0 x_1 \cdots x_{\ell-1}\) of natural numbers with \(x_i < m(i)\) for every \(i < \ell\). 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 · Rigid level stabilizer · Rigid vertex stabilizer

DefinitionRigid vertex stabilizer#✓fully proved

Let \(\rho\) be a homomorphism from a group \(G\) to the group of permutations of 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\) such that \(\rho(g)\) fixes every vertex that does not have \(v\) as a prefix, that is, the elements whose support (the set of vertices they move) lies in 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 a spherically homogeneous rooted tree

Used byRigid level stabilizer

DefinitionRigid level stabilizer#✓fully proved

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

Used byBranch groups

DefinitionBranch groups#✓fully proved

A group \(G\) is a branch group (Kourovka 15.12) if there are a sequence \(m : \mathbb{N} \to \mathbb{N}\) with \(m(i) \ge 2\) for all \(i\) and a homomorphism \(\rho\) from \(G\) to the group of permutations of the vertices of the rooted tree with branching sequence \(m\) such that \(\rho\) is injective; every \(\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 there is \(g \in G\) with \(\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 a spherically homogeneous rooted tree · Rigid level stabilizer

Used byThe branch question for just infinite groups of intermediate growth

DefinitionGrowth rate of a finite generating family#✓fully proved

Let \(P\) be a generating family of a group \(G\) indexed by \(\{0, \dots, k-1\}\), and let \(\beta_P(n)\) be the number of elements of \(G\) whose word length with respect to \(P\) is at most \(n\), that is, which are products of at most \(n\) members of \(P\) and their inverses. The growth rate of \(P\) is the real number \(\omega(G, P) = \limsup_{n \to \infty} \beta_P(n)^{1/n}\).

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 intermediate growth

DefinitionJust infinite groups#✓fully proved

A group \(G\) is just infinite if it is infinite and every nontrivial normal subgroup of \(G\) has finite index, that is, all proper quotients of \(G\) are finite.

def IsJustInfinite (G : Type*) [Group G] : Prop :=
  Infinite G ∧ ∀ N : Subgroup G, N.Normal → N ≠ ⊥ → N.FiniteIndex

Used by 1

Used byThe branch question for just infinite groups of intermediate growth

DefinitionGroups of intermediate growth#✓fully proved

A group \(G\) has intermediate growth if it is finitely generated and, for every natural number \(k\) and every generating family \(P\) of \(G\) indexed by \(\{0, \dots, k-1\}\), the growth rate of \(P\) is at most \(1\) (subexponential growth) and \(P\) does not have polynomial growth.

def HasIntermediateGrowth (G : Type*) [Group G] : Prop :=
  Group.FG G ∧ ∀ (k : ℕ) (P : Group.Generators G (Fin k)),
    growthRate P ≤ 1 ∧ ¬ P.HasPolynomialGrowth

Uses 2 · Used by 1

Statement usesPolynomial growth · Growth rate of a finite generating family

Used byThe branch question for just infinite groups of intermediate growth

DefinitionThe branch question for just infinite groups of intermediate growth#✓fully proved

Kourovka Problem 15.17 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić) is the assertion that every finitely generated just infinite group of intermediate growth is a branch group.

def justInfiniteIntermediateGrowthIsBranch : Prop :=
  ∀ (G : Type) [Group G], Group.FG G → IsJustInfinite G → HasIntermediateGrowth G →
    IsBranchGroup G

Uses 3 · Used by 1

Statement usesGroups of intermediate growth · Branch groups · Just infinite groups

Used byJust infinite groups of intermediate growth need not be branch groups

TheoremJust infinite groups of intermediate growth need not be branch groups#●ready to prove

It is not the case that every finitely generated just infinite group of intermediate growth is a branch group: the Kourovka Archive answers Problem 15.17 "No, not every".

Nekrashevych constructed infinite finitely generated simple groups of intermediate growth. Such a group is just infinite, and it is not a branch group: its rigid level stabilizers, nontrivial normal subgroups of finite index, would be the whole group, which they split as a direct product of at least two nontrivial factors.

public theorem_wanted justInfiniteIntermediateGrowthIsBranch_refuted :
    ¬ justInfiniteIntermediateGrowthIsBranch

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.17 (L. Bartholdi, R. I. Grigorchuk, Z. Šunić); resolution: V. Nekrashevych, Palindromic subshifts and simple periodic groups of intermediate growth, Ann. of Math. (2) 187 (2018), no. 3, 667-719, abstract (infinite finitely generated periodic groups of intermediate growth, among them the first simple groups of intermediate growth); Kourovka Archive, Problem 15.17 (answer: No, not every; there exist simple finitely generated groups of intermediate growth; the Archive prints the volume as 87), https://arxiv.org/abs/1601.01033.

Uses 1

Statement usesThe branch question for just infinite groups of intermediate growth

13 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.