Gromov's theorem on groups of polynomial growth

Reference:

• Wikipedia

def GromovPolynomialGrowth.CayleyBall {G : Type u_1} [Group G] (S : Set G) (n : ℕ) : Set G

The CayleyBall is the ball of radius n in the Cayley graph of a group G with generating set S.

Equations

• GromovPolynomialGrowth.CayleyBall S n = {g : G | ∃ (l : List G), l.length ≤ n ∧ (∀ s ∈ l, s ∈ S ∨ s⁻¹ ∈ S) ∧ l.prod = g}

noncomputable def GromovPolynomialGrowth.GrowthFunction {G : Type u_1} [Group G] (S : Set G) (n : ℕ) : ℕ

The GrowthFunction of a group G with respect to a set S counts the number of group elements that can be reached by words of length at most n in S.

Equations

• GromovPolynomialGrowth.GrowthFunction S n = (GromovPolynomialGrowth.CayleyBall S n).ncard

theorem GromovPolynomialGrowth.one_mem_CayleyBall {G : Type u_1} [Group G] (S : Set G) (n : ℕ) : 1 ∈ CayleyBall S n

The identity is always in the Cayley ball of radius n for any n ≥ 0.

theorem GromovPolynomialGrowth.CayleyBall_monotone {G : Type u_1} [Group G] (S : Set G) {m n : ℕ} (h : m ≤ n) : CayleyBall S m ⊆ CayleyBall S n

The Cayley ball is monotonic in radius.

theorem GromovPolynomialGrowth.CayleyBall_mul {G : Type u_1} [Group G] (S : Set G) {g h : G} {m n : ℕ} (hg : g ∈ CayleyBall S m) (hh : h ∈ CayleyBall S n) : g * h ∈ CayleyBall S (m + n)

Closure property: if g, h ∈ CayleyBall S m, CayleyBall S n respectively, then gh ∈ CayleyBall S (m + n).

theorem GromovPolynomialGrowth.CayleyBall_inv {G : Type u_1} [Group G] (S : Set G) {g : G} {n : ℕ} (hg : g ∈ CayleyBall S n) : g⁻¹ ∈ CayleyBall S n

If g ∈ CayleyBall S n, then g⁻¹ ∈ CayleyBall S n.

def GromovPolynomialGrowth.HasPolynomialGrowth (G : Type u_1) [Group G] : Prop

A group HasPolynomialGrowth if there exists a finite generating set such that the growth function is bounded above by a polynomial.

Equations

• One or more equations did not get rendered due to their size.

theorem GromovPolynomialGrowth.GromovPolynomialGrowthTheorem (G : Type u_1) [Group G] [Group.FG G] : HasPolynomialGrowth G ↔ Group.IsVirtuallyNilpotent G

Gromov's Polynomial Growth Theorem : A finitely generated group has polynomial growth if and only if it is virtually nilpotent.