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}

theorem GromovPolynomialGrowth.cayleyBall_zero {G : Type u_1} [Group G] (S : Set G) : CayleyBall S 0 = {1}

theorem GromovPolynomialGrowth.cayleyBall_finite {G : Type u_1} [Group G] {S : Set G} (hS : S.Finite) (n : ℕ) : (CayleyBall S n).Finite

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.growthFunction_zero {G : Type u_1} [Group G] (S : Set G) : GrowthFunction S 0 = 1

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.

theorem GromovPolynomialGrowth.mem_cayleyBall_one_of_mem {G : Type u_1} [Group G] {S : Set G} {g : G} (hg : g ∈ S) : g ∈ CayleyBall S 1

theorem GromovPolynomialGrowth.exists_cayleyBall_mem_of_closure_eq_top {G : Type u_1} [Group G] {S : Set G} (h : Subgroup.closure S = ⊤) (g : G) : ∃ (n : ℕ), g ∈ CayleyBall S n

theorem GromovPolynomialGrowth.tendsto_atTop_growthFunction_of_infinite {G : Type u_1} [Group G] [Infinite G] {S : Set G} (hS : S.Finite) (h : Subgroup.closure S = ⊤) : Filter.Tendsto (GrowthFunction S) Filter.atTop Filter.atTop

In an infinite group, the growth function with respect to a finite generating set is unbounded.

theorem GromovPolynomialGrowth.growthFunction_not_polynomial_of_infinite {G : Type u_1} [Group G] [Infinite G] {S : Set G} (hS : S.Finite) (h : Subgroup.closure S = ⊤) {C : ℝ} (d : ℕ) : ∃ (n : ℕ), C * ↑n ^ d < ↑(GrowthFunction S n)

Infinite groups do not satisfy polynomial growth over ℕ for any degree d because when d = 0 this reduces to the unbounded nature of growthFunction while n = 0 works when d ≠ 0. Thus a finitely-generated infinite nilpotent group would be a counter-example to Gromov's theorem when quantifying over all of ℕ, and so n = 0 should be excluded.

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.