Braid equivalence of Coxeter words

A braid move replaces one alternating subword of length M i j by the alternating word of the same length with the two indices interchanged. Braid equivalence is the equivalence relation on words generated by these moves.

This file develops the elementary, presentation-independent part of the braid-move API. A braid move preserves length and the product represented by a word in every Coxeter system with matrix M. More generally, it preserves evaluation in any monoid whenever the chosen generators satisfy the braid relations. Braid equivalence is also stable under adding a common prefix or suffix.

Matsumoto's theorem supplies the converse for reduced words: two reduced words with the same Coxeter-group product are braid equivalent. The definitions and soundness results here isolate the relation occurring in that statement and in its monoid-valued lift formulation.

Main definitions

• CoxeterSystem.IsBraidMove: two words differ by one braid move.
• CoxeterSystem.BraidEquivalent: two words are connected by finitely many braid moves.

Main results

• CoxeterSystem.IsBraidMove.prod_map_eq: a braid move preserves evaluation in a monoid whose chosen generators satisfy the braid relations.
• CoxeterSystem.BraidEquivalent.prod_map_eq: braid equivalence preserves such evaluations.
• CoxeterSystem.BraidEquivalent.wordProd_eq: braid-equivalent words represent the same element of every Coxeter system with matrix M.
• CoxeterSystem.BraidEquivalent.isReduced_iff: braid equivalence preserves reducedness.

References

• Mathlib's Mathlib.GroupTheory.Coxeter.Basic provides CoxeterSystem.braidWord and CoxeterSystem.wordProd_braidWord_eq, on which this construction is based.
• J. E. Humphreys, Reflection Groups and Coxeter Groups
• [A. Björner and F. Brenti, Combinatorics of Coxeter Groups][bjorner2005]

inductive CoxeterSystem.IsBraidMove {B : Type u_1} (M : CoxeterMatrix B) : List B → List B → Prop

A single braid move replaces, inside a fixed context, braidWord M i j by braidWord M j i.

• mk {B : Type u_1} {M : CoxeterMatrix B} (pre suf : List B) (i j : B) : IsBraidMove M (pre ++ braidWord M i j ++ suf) (pre ++ braidWord M j i ++ suf)

def CoxeterSystem.BraidEquivalent {B : Type u_1} (M : CoxeterMatrix B) : List B → List B → Prop

Braid equivalence is the equivalence relation generated by single braid moves.

Equations

• CoxeterSystem.BraidEquivalent M = Relation.EqvGen (CoxeterSystem.IsBraidMove M)

theorem CoxeterSystem.IsBraidMove.symm {B : Type u_1} {M : CoxeterMatrix B} {word word' : List B} (h : IsBraidMove M word word') : IsBraidMove M word' word

A braid move can be traversed in the reverse direction.

theorem CoxeterSystem.IsBraidMove.append_left {B : Type u_1} {M : CoxeterMatrix B} (pre : List B) {word word' : List B} (h : IsBraidMove M word word') : IsBraidMove M (pre ++ word) (pre ++ word')

Adding a common prefix preserves a braid move.

theorem CoxeterSystem.IsBraidMove.append_right {B : Type u_1} {M : CoxeterMatrix B} {word word' : List B} (h : IsBraidMove M word word') (suf : List B) : IsBraidMove M (word ++ suf) (word' ++ suf)

Adding a common suffix preserves a braid move.

theorem CoxeterSystem.IsBraidMove.length_eq {B : Type u_1} {M : CoxeterMatrix B} {word word' : List B} (h : IsBraidMove M word word') : word.length = word'.length

A braid move does not change the length of a word.

theorem CoxeterSystem.IsBraidMove.prod_map_eq {B : Type u_1} {G : Type u_3} {M : CoxeterMatrix B} [Monoid G] (f : B → G) (hbraid : ∀ (i j : B), (List.map f (braidWord M i j)).prod = (List.map f (braidWord M j i)).prod) {word word' : List B} (h : IsBraidMove M word word') : (List.map f word).prod = (List.map f word').prod

A braid move preserves evaluation in any monoid whose chosen generators satisfy the braid relations.

theorem CoxeterSystem.IsBraidMove.wordProd_eq {B : Type u_1} {W : Type u_2} {M : CoxeterMatrix B} [Group W] (cs : CoxeterSystem M W) {word word' : List B} (h : IsBraidMove M word word') : cs.wordProd word = cs.wordProd word'

A braid move preserves the element represented by a word in a Coxeter system.

theorem CoxeterSystem.BraidEquivalent.refl {B : Type u_1} {M : CoxeterMatrix B} (word : List B) : BraidEquivalent M word word

Every word is braid equivalent to itself.

theorem CoxeterSystem.BraidEquivalent.symm {B : Type u_1} {M : CoxeterMatrix B} {word word' : List B} (h : BraidEquivalent M word word') : BraidEquivalent M word' word

Braid equivalence is symmetric.

theorem CoxeterSystem.BraidEquivalent.trans {B : Type u_1} {M : CoxeterMatrix B} {word word' word'' : List B} (h : BraidEquivalent M word word') (h' : BraidEquivalent M word' word'') : BraidEquivalent M word word''

Braid equivalence is transitive.

theorem CoxeterSystem.BraidEquivalent.of_isBraidMove {B : Type u_1} {M : CoxeterMatrix B} {word word' : List B} (h : IsBraidMove M word word') : BraidEquivalent M word word'

A single braid move gives a braid equivalence.

theorem CoxeterSystem.BraidEquivalent.induction_on {B : Type u_1} {M : CoxeterMatrix B} {P : List B → List B → Prop} {word word' : List B} (h : BraidEquivalent M word word') (move : ∀ {word word' : List B}, IsBraidMove M word word' → P word word') (refl : ∀ (word : List B), P word word) (symm : ∀ {word word' : List B}, P word word' → P word' word) (trans : ∀ {word word' word'' : List B}, P word word' → P word' word'' → P word word'') : P word word'

To prove a property of braid-equivalent words, it suffices to check single braid moves and that the property is reflexive, symmetric, and transitive.

theorem CoxeterSystem.BraidEquivalent.append_left {B : Type u_1} {M : CoxeterMatrix B} (pre : List B) {word word' : List B} (h : BraidEquivalent M word word') : BraidEquivalent M (pre ++ word) (pre ++ word')

Adding a common prefix preserves braid equivalence.

theorem CoxeterSystem.BraidEquivalent.append_right {B : Type u_1} {M : CoxeterMatrix B} {word word' : List B} (h : BraidEquivalent M word word') (suf : List B) : BraidEquivalent M (word ++ suf) (word' ++ suf)

Adding a common suffix preserves braid equivalence.

theorem CoxeterSystem.BraidEquivalent.append {B : Type u_1} {M : CoxeterMatrix B} {word₁ word₁' word₂ word₂' : List B} (h₁ : BraidEquivalent M word₁ word₁') (h₂ : BraidEquivalent M word₂ word₂') : BraidEquivalent M (word₁ ++ word₂) (word₁' ++ word₂')

Appending braid-equivalent words gives braid-equivalent words.

theorem CoxeterSystem.BraidEquivalent.length_eq {B : Type u_1} {M : CoxeterMatrix B} {word word' : List B} (h : BraidEquivalent M word word') : word.length = word'.length

Braid-equivalent words have the same length.

theorem CoxeterSystem.BraidEquivalent.prod_map_eq {B : Type u_1} {G : Type u_3} {M : CoxeterMatrix B} [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) {word word' : List B} (h : BraidEquivalent M word word') : (List.map f word).prod = (List.map f word').prod

Braid equivalence preserves evaluation in any monoid whose chosen generators satisfy the braid relations.

theorem CoxeterSystem.BraidEquivalent.wordProd_eq {B : Type u_1} {W : Type u_2} {M : CoxeterMatrix B} [Group W] (cs : CoxeterSystem M W) {word word' : List B} (h : BraidEquivalent M word word') : cs.wordProd word = cs.wordProd word'

Braid-equivalent words represent the same element of a Coxeter system.

theorem CoxeterSystem.BraidEquivalent.isReduced_iff {B : Type u_1} {W : Type u_2} {M : CoxeterMatrix B} [Group W] (cs : CoxeterSystem M W) {word word' : List B} (h : BraidEquivalent M word word') : cs.IsReduced word ↔ cs.IsReduced word'

Braid equivalence preserves reducedness in a Coxeter system.

theorem CoxeterSystem.BraidEquivalent.braidWord {B : Type u_1} {M : CoxeterMatrix B} (i j : B) : BraidEquivalent M (CoxeterSystem.braidWord M i j) (CoxeterSystem.braidWord M j i)

The two braid words for a pair of indices are braid equivalent.