Hyperbolic groups

DefinitionWord-hyperbolic groups#✓fully proved

A group \(G\) is word-hyperbolic if there are a finite index set \(\iota\) and a family \((s_i)_{i \in \iota}\) of elements generating \(G\) such that \(G\), equipped with the word metric of this generating family, is \(\delta\)-hyperbolic for some real number \(\delta\).

def IsHyperbolic (G : Type*) [Group G] : Prop :=
  ∃ (ι : Type) (_ : Finite ι) (P : Group.Generators G ι) (δ : ℝ),
    @Metric.IsDeltaHyperbolic G P.normedGroup.toMetricSpace.toPseudoMetricSpace δ

Uses 1 · Used by 6

Statement usesGromov \(\delta\)-hyperbolic space

Used byWord-hyperbolic groups are finitely generated · The trivial group is word-hyperbolic · Kourovka Problem 11.74(a) (infinite power quotients of hyperbolic groups) · Kourovka Problem 11.74(b) (trivial intersection of power subgroups) · Decidability of the elementary theory of torsion-free hyperbolic groups · Kourovka Problem 14.19 (hyperbolic groups and the Noetherian Equation Property)

TheoremWord-hyperbolic groups are finitely generated#✓fully proved

Every word-hyperbolic group is finitely generated.

theorem IsHyperbolic.fg (h : IsHyperbolic G) : Group.FG G

Uses 2

Statement usesWord-hyperbolic groups

Proof usesGromov \(\delta\)-hyperbolic space

TheoremThe trivial group is word-hyperbolic#✓fully proved

Every trivial group is word-hyperbolic: the empty family generates it, and its word metric is \(0\)-hyperbolic.

theorem IsHyperbolic.of_subsingleton (G : Type*) [Group G] [Subsingleton G] : IsHyperbolic G

Uses 2

Statement usesWord-hyperbolic groups

Proof usesGromov \(\delta\)-hyperbolic space

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.