Matsumoto's theorem

Any two reduced words representing the same element of a Coxeter group are connected by braid moves. Consequently, generators in an arbitrary monoid satisfying the braid relations have a well-defined value along reduced words. The generators need not be involutions, so this value need not be a monoid homomorphism.

The relational statement is TauCeti.braidEquivalent_of_isReduced_wordProd_eq; the evaluation statement is TauCeti.matsumoto. Both apply to arbitrary Coxeter systems, including infinite groups and infinite Coxeter-matrix entries. TauCeti.existsUnique_reducedWordLift expresses the result as a universal property: there is a unique function on the group agreeing with evaluation of every reduced word.

The two sides of a braid move are themselves reduced words (CoxeterSystem.isReduced_braidWord); more generally an alternating word is reduced as long as its length is at most the Coxeter-matrix entry (CoxeterSystem.isReduced_alternatingWord).

Implementation notes

Induction on length cancels a common first letter. For different first letters, Tits' rank-two parabolic lemma supplies two reduced expressions with a common suffix and braid-related prefixes. The geometric representation identifies the length of those prefixes with the Coxeter-matrix entry. Induction then joins the original words to these expressions.

References

• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Section 1.9.
• A. Björner and F. Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), Section 3.3.

theorem TauCeti.braidEquivalent_of_isReduced_wordProd_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω ω' : List B} (hω : cs.IsReduced ω) (hω' : cs.IsReduced ω') (hprod : cs.wordProd ω = cs.wordProd ω') : CoxeterSystem.BraidEquivalent M ω ω'

Matsumoto's theorem, relational form. Two reduced words representing the same element of a Coxeter group are connected by braid moves.

theorem TauCeti.braidEquivalent_iff_wordProd_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω ω' : List B} (hω : cs.IsReduced ω) (hω' : cs.IsReduced ω') : CoxeterSystem.BraidEquivalent M ω ω' ↔ cs.wordProd ω = cs.wordProd ω'

For reduced words, braid equivalence is exactly equality of the represented Coxeter-group elements.

theorem TauCeti.matsumoto {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_3} [Monoid G] (f : B → G) (hbraid : ∀ (i j : B), (List.map f (CoxeterSystem.braidWord M i j)).prod = (List.map f (CoxeterSystem.braidWord M j i)).prod) {ω ω' : List B} (hω : cs.IsReduced ω) (hω' : cs.IsReduced ω') (hprod : cs.wordProd ω = cs.wordProd ω') : (List.map f ω).prod = (List.map f ω').prod

Matsumoto's theorem, monoid-valued form. If the chosen generators satisfy all braid relations, evaluating a reduced word depends only on the element it represents. No square relations are required of the generators.

theorem CoxeterSystem.isReduced_alternatingWord {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i i' : B} {m : ℕ} (hm : m ≤ M.M i i' ∨ M.M i i' = 0) : cs.IsReduced (alternatingWord i i' m)

Alternating words are reduced up to the Coxeter-matrix entry: the word alternatingWord i i' m is reduced whenever m ≤ M i i', and for every m when M i i' = 0 (read as ∞). This is the converse of Mathlib's CoxeterSystem.not_isReduced_alternatingWord.

theorem CoxeterSystem.isReduced_braidWord {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) : cs.IsReduced (braidWord M i i')

Braid words are reduced: the two sides of the braid relation at (i, i') are reduced words.

theorem TauCeti.existsUnique_reducedWordLift {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_3} [Monoid G] (f : B → G) (hbraid : ∀ (i j : B), (List.map f (CoxeterSystem.braidWord M i j)).prod = (List.map f (CoxeterSystem.braidWord M j i)).prod) : ∃! F : W → G, ∀ (ω : List B), cs.IsReduced ω → F (cs.wordProd ω) = (List.map f ω).prod

Generators satisfying the braid relations extend uniquely to a function on the Coxeter group whose value on every reduced expression is the product of those generators.