Elementary facts about Coxeter words

This file evaluates Mathlib's alternating words through an arbitrary family, and specialises that evaluation to the lengths the braid relations are read off at. It also records the degenerate rank-zero case: a Coxeter system whose simple reflections are indexed by an empty type has a trivial group.

Main results

• TauCeti.prod_map_alternatingWord: an alternating word of length m, evaluated through any family f. This is the shape in which a braid relation is checked against a family that is not yet known to satisfy it, so it cannot be routed through CoxeterSystem.prod_alternatingWord_eq_mul_pow, which evaluates only the simple reflections themselves. The evaluations at lengths 2 and 3 are special cases.
• TauCeti.reverse_alternatingWord_two_mul: reversing an alternating word of even length swaps its two letters.
• TauCeti.subsingleton_of_isEmpty_index: a Coxeter system of rank zero has a trivial group.

theorem TauCeti.prod_map_alternatingWord {B : Type u_1} {N : Type u_2} [Monoid N] (f : B → N) (i i' : B) (m : ℕ) : (List.map f (CoxeterSystem.alternatingWord i i' m)).prod = (if Even m then 1 else f i') * (f i * f i') ^ (m / 2)

An alternating word of length m, evaluated through any family f. Unlike CoxeterSystem.prod_alternatingWord_eq_mul_pow, which evaluates the word at the simple reflections of a Coxeter system, this holds for an arbitrary family, so it is available while checking that a family satisfies the braid relations.

theorem TauCeti.prod_map_alternatingWord_two {B : Type u_1} {N : Type u_2} [Monoid N] (f : B → N) (i i' : B) : (List.map f (CoxeterSystem.alternatingWord i i' 2)).prod = f i * f i'

An alternating word of length 2, evaluated through any family f.

theorem TauCeti.prod_map_alternatingWord_three {B : Type u_1} {N : Type u_2} [Monoid N] (f : B → N) (i i' : B) : (List.map f (CoxeterSystem.alternatingWord i i' 3)).prod = f i' * f i * f i'

An alternating word of length 3, evaluated through any family f.

Alternating words of even length

theorem TauCeti.reverse_alternatingWord_two_mul {B : Type u_1} (i i' : B) (m : ℕ) : (CoxeterSystem.alternatingWord i i' (2 * m)).reverse = CoxeterSystem.alternatingWord i' i (2 * m)

Reversing an alternating word of even length swaps its two letters.

Rank zero

theorem TauCeti.subsingleton_of_isEmpty_index {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) [IsEmpty B] : Subsingleton W

A Coxeter system whose simple reflections are indexed by an empty type has a trivial group: every element is the product of a word in the generators, and the only such word is empty.