Power quotients of hyperbolic groups

DefinitionPower subgroup#✓fully proved

For a group \(G\) and a natural number \(n\), \(G^n\) is the subgroup of \(G\) generated by the \(n\)-th powers \(g^n\) of all elements \(g \in G\).

def powerSubgroup (G : Type*) [Group G] (n : ℕ) : Subgroup G :=
  Subgroup.closure (Set.range fun g : G => g ^ n)

Used by 2

Used byKourovka Problem 11.74(a) (infinite power quotients of hyperbolic groups) · Kourovka Problem 11.74(b) (trivial intersection of power subgroups)

DefinitionKourovka Problem 11.74(a) (infinite power quotients of hyperbolic groups)#✓fully proved

For every word-hyperbolic group \(G\) that is not virtually cyclic (non-elementary), there is an integer \(n \ge 1\) such that the subgroup \(G^n\) generated by the \(n\)-th powers of the elements of \(G\) has infinite index in \(G\), i.e. the quotient \(G / G^n\) is infinite.

The problem is due to M. Gromov and A. Yu. Olshanskii.

def powerQuotientInfinite : Prop :=
  ∀ (G : Type) [Group G], Group.IsHyperbolic G → ¬ Group.IsVirtuallyCyclic G →
    ∃ n : ℕ, 1 ≤ n ∧ ¬ (powerSubgroup G n).FiniteIndex

Uses 2 · Used by 1

Statement usesWord-hyperbolic groups · Power subgroup

Used byNon-elementary hyperbolic groups have infinite power quotients

DefinitionKourovka Problem 11.74(b) (trivial intersection of power subgroups)#✓fully proved

For every word-hyperbolic group \(G\) that is not virtually cyclic (non-elementary), the only element of \(G\) lying in the subgroup \(G^n\) generated by the \(n\)-th powers for every integer \(n \ge 1\) is the identity, i.e. \(\bigcap_{n \ge 1} G^n = 1\).

The problem is due to A. Yu. Olshanskii.

def powerSubgroupsTrivialIntersection : Prop :=
  ∀ (G : Type) [Group G], Group.IsHyperbolic G → ¬ Group.IsVirtuallyCyclic G →
    ∀ g : G, (∀ n : ℕ, 1 ≤ n → g ∈ powerSubgroup G n) → g = 1

Uses 2 · Used by 1

Statement usesWord-hyperbolic groups · Power subgroup

Used byPower subgroups of a non-elementary hyperbolic group intersect trivially

TheoremNon-elementary hyperbolic groups have infinite power quotients#●ready to prove

For every word-hyperbolic group \(G\) that is not virtually cyclic, there is an integer \(n \ge 1\) such that the subgroup \(G^n\) generated by the \(n\)-th powers of the elements of \(G\) has infinite index in \(G\), i.e. the quotient \(G / G^n\) is infinite.

This answers Kourovka Problem 11.74(a) ("Yes, it is"); the proof is due to Ivanov and Olshanskii.

public theorem_wanted powerQuotientInfinite_holds : powerQuotientInfinite

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 11.74 (A. Yu. Olshanskii); resolution: S. V. Ivanov and A. Yu. Olshanskii, Trans. Amer. Math. Soc. 348, no. 6 (1996), 2091-2138, Kourovka Archive, Problem 11.74: "a) Yes, it is; b) Yes, it is", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 11.74(a) (infinite power quotients of hyperbolic groups)

TheoremPower subgroups of a non-elementary hyperbolic group intersect trivially#●ready to prove

For every word-hyperbolic group \(G\) that is not virtually cyclic, the only element of \(G\) lying in the subgroup \(G^n\) generated by the \(n\)-th powers for every integer \(n \ge 1\) is the identity, i.e. \(\bigcap_{n \ge 1} G^n = 1\).

This answers Kourovka Problem 11.74(b) ("Yes, it is"); the proof is due to Ivanov and Olshanskii.

public theorem_wanted powerSubgroupsTrivialIntersection_holds : powerSubgroupsTrivialIntersection

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 11.74 (A. Yu. Olshanskii); resolution: S. V. Ivanov and A. Yu. Olshanskii, Trans. Amer. Math. Soc. 348, no. 6 (1996), 2091-2138, Kourovka Archive, Problem 11.74: "a) Yes, it is; b) Yes, it is", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 11.74(b) (trivial intersection of power subgroups)

3 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.