Evaluation of words

A generating family P : Group.Generators G ι indexed by ι gives rise to an evaluation map P.wordProd : List (ι × Bool) → G.

Main definitions

• Group.Generators.wordProd: the canonical map from a word List (ι × Bool) over a generating family ι to the corresponding group G. It sends each (i, true) to P.val i and (i, false) to (P.val i)⁻¹.

Implementation notes

• The API in this file is modelled on the word API for Coxeter groups (CoxeterSystem.wordProd).
• List (ι × Bool) is the canonical way to write words which evaluate to FreeGroup elements through FreeGroup.mk.

Tags

word, generating set, geometric group theory

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

The canonical map from a word List (ι × Bool) over a generating family ι to its corresponding group G.

Equations

• P.wordProd l = P.lift (FreeGroup.mk l)

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

The canonical map from a word List (ι × Bool) over a generating family ι to its corresponding additive group G.

Equations

• P.wordSum l = P.lift (FreeAddGroup.mk l)

theorem Group.Generators.wordProd_surjective {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) : Function.Surjective P.wordProd

Every element of G is the product of some word over a generating family.

theorem AddGroup.Generators.wordSum_surjective {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) : Function.Surjective P.wordSum

Every element of G is the sum of some word over a generating family.

@[simp]

theorem Group.Generators.wordProd_nil {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) : P.wordProd [] = 1

@[simp]

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

@[simp]

theorem Group.Generators.wordProd_singleton {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (i : ι) (b : Bool) : P.wordProd [(i, b)] = bif b then P.val i else (P.val i)⁻¹

@[simp]

theorem AddGroup.Generators.wordSum_singleton {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (i : ι) (b : Bool) : P.wordSum [(i, b)] = bif b then P.val i else -P.val i

theorem Group.Generators.wordProd_cons {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (i : ι) (b : Bool) (l : List (ι × Bool)) : P.wordProd ((i, b) :: l) = (bif b then P.val i else (P.val i)⁻¹) * P.wordProd l

theorem AddGroup.Generators.wordSum_cons {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (i : ι) (b : Bool) (l : List (ι × Bool)) : P.wordSum ((i, b) :: l) = (bif b then P.val i else -P.val i) + P.wordSum l

theorem Group.Generators.wordProd_append {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (l₁ l₂ : List (ι × Bool)) : P.wordProd (l₁ ++ l₂) = P.wordProd l₁ * P.wordProd l₂

theorem AddGroup.Generators.wordSum_append {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (l₁ l₂ : List (ι × Bool)) : P.wordSum (l₁ ++ l₂) = P.wordSum l₁ + P.wordSum l₂

theorem Group.Generators.wordProd_invRev {G : Type u_1} {ι : Type u_2} [Group G] (P : Generators G ι) (l : List (ι × Bool)) : P.wordProd (FreeGroup.invRev l) = (P.wordProd l)⁻¹

theorem AddGroup.Generators.wordSum_negRev {G : Type u_1} {ι : Type u_2} [AddGroup G] (P : Generators G ι) (l : List (ι × Bool)) : P.wordSum (FreeAddGroup.negRev l) = -P.wordSum l