The word metric

The word length of an element is the length of a shortest representing word, over a generating family given by Group.Generators. The word length defines a norm on G inducing the word metric dist g h = ‖g⁻¹ * h‖.

Main definitions

• Group.Generators.wordLength: the word length of an element of G with respect to a generating family P.
• Group.Generators.IsGeodesic: a word is geodesic if it is of minimal length among the words representing the same group element.
• Group.Generators.wordNorm: the word length as a norm on G.
• Group.Generators.normedGroup: the normed group structure on G induced by wordNorm. This gives rise to a word metric on G.

Main results

• Group.Generators.exists_isGeodesic: every element of G is represented by some geodesic word.

Implementation notes

• The API in this file is modelled on the length API for Coxeter groups (CoxeterSystem.length).
• We define wordLength in terms of sInf instead of Nat.find to avoid having to produce the DecidablePred instance. The junk value 0 on ∅ is never reached because every group element has at least one word representing it.The definition of wordLength has no useful defeqs and is characterized by wordLength_le_iff, so we tag it with @[no_expose].

TODO

• Relate the word metric to the distance in the Cayley graph.

Tags

word metric, word length, geometric group theory

Definition of word length

noncomputable def Group.Generators.wordLength {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (g : G) : ℕ

The word length of g with respect to the generating family P.

Equations

• P.wordLength g = sInf {n : ℕ | ∃ (l : List (ι × Bool)), P.wordProd l = g ∧ l.length = n}

noncomputable def AddGroup.Generators.wordLength {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (g : G) : ℕ

The word length of g with respect to the generating family P.

Equations

• P.wordLength g = sInf {n : ℕ | ∃ (l : List (ι × Bool)), P.wordSum l = g ∧ l.length = n}

Geodesic words

def Group.Generators.IsGeodesic {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (l : List (ι × Bool)) : Prop

A word l is geodesic if its length is exactly the word length of the group element it represents.

Equations

• P.IsGeodesic l = (P.wordLength (P.wordProd l) = l.length)

def AddGroup.Generators.IsGeodesic {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (l : List (ι × Bool)) : Prop

A word l is geodesic if its length is exactly the word length of the group element it represents.

Equations

• P.IsGeodesic l = (P.wordLength (P.wordSum l) = l.length)

theorem Group.Generators.IsGeodesic.eq {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) {l : List (ι × Bool)} (hl : P.IsGeodesic l) : P.wordLength (P.wordProd l) = l.length

theorem AddGroup.Generators.IsGeodesic.eq {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) {l : List (ι × Bool)} (hl : P.IsGeodesic l) : P.wordLength (P.wordSum l) = l.length

theorem Group.Generators.exists_isGeodesic {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (g : G) : ∃ (l : List (ι × Bool)), P.IsGeodesic l ∧ P.wordProd l = g

Every group element has a geodesic word representative.

theorem AddGroup.Generators.exists_isGeodesic {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (g : G) : ∃ (l : List (ι × Bool)), P.IsGeodesic l ∧ P.wordSum l = g

Every additive group element has a geodesic word representative.

Word length

theorem Group.Generators.wordLength_wordProd_le {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (l : List (ι × Bool)) : P.wordLength (P.wordProd l) ≤ l.length

theorem AddGroup.Generators.wordLength_wordSum_le {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (l : List (ι × Bool)) : P.wordLength (P.wordSum l) ≤ l.length

theorem Group.Generators.wordLength_le_iff {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (g : G) {n : ℕ} : P.wordLength g ≤ n ↔ ∃ (l : List (ι × Bool)), l.length ≤ n ∧ P.wordProd l = g

The characterisation of word length: the word length of a group element is less or equal to n if and only if there exists a word l of length at most n which evaluates to g.

theorem AddGroup.Generators.wordLength_le_iff {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (g : G) {n : ℕ} : P.wordLength g ≤ n ↔ ∃ (l : List (ι × Bool)), l.length ≤ n ∧ P.wordSum l = g

The characterisation of word length: the word length of an additive group element is less or equal to n if and only if there exists a word l of length at most n which evaluates to g.

@[simp]

theorem Group.Generators.wordLength_eq_zero_iff {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) {g : G} : P.wordLength g = 0 ↔ g = 1

@[simp]

theorem AddGroup.Generators.wordLength_eq_zero_iff {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) {g : G} : P.wordLength g = 0 ↔ g = 0

@[simp]

theorem Group.Generators.wordLength_one {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) : P.wordLength 1 = 0

@[simp]

theorem AddGroup.Generators.wordLength_zero {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) : P.wordLength 0 = 0

@[simp]

theorem Group.Generators.wordLength_inv {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (g : G) : P.wordLength g⁻¹ = P.wordLength g

@[simp]

theorem AddGroup.Generators.wordLength_neg {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (g : G) : P.wordLength (-g) = P.wordLength g

theorem Group.Generators.wordLength_mul_le {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (g h : G) : P.wordLength (g * h) ≤ P.wordLength g + P.wordLength h

theorem AddGroup.Generators.wordLength_add_le {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (g h : G) : P.wordLength (g + h) ≤ P.wordLength g + P.wordLength h

noncomputable def Group.Generators.groupNorm {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) : GroupNorm G

The wordLength with respect to a generating family P defines a norm on G.

Equations

• P.groupNorm = { toFun := fun (g : G) => ↑(P.wordLength g), map_one' := ⋯, mul_le' := ⋯, inv' := ⋯, eq_one_of_map_eq_zero' := ⋯ }

noncomputable def AddGroup.Generators.addGroupNorm {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) : AddGroupNorm G

The wordLength with respect to a generating family P defines a norm on the additive group G.

Equations

• P.addGroupNorm = { toFun := fun (g : G) => ↑(P.wordLength g), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }

Word metric

@[instance_reducible]

noncomputable def Group.Generators.normedGroup {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) : NormedGroup G

The wordLength with respect to a generating family P gives G the structure of a normed group.

Equations

• P.normedGroup = P.groupNorm.toNormedGroup

@[instance_reducible]

noncomputable def AddGroup.Generators.normedAddGroup {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) : NormedAddGroup G

The wordLength with respect to a generating family P gives G the structure of a normed additive group.

Equations

• P.normedAddGroup = P.addGroupNorm.toNormedAddGroup