The strong exchange condition

Let cs : CoxeterSystem M W be a Coxeter system, let ω be a word, reduced or not, and let t be a reflection of W, that is, a conjugate of a simple reflection. The strong exchange condition says that if left multiplication by t shortens π ω, then t * π ω is spelled by ω with exactly one letter deleted:

t * π ω = π (ω.eraseIdx j) for some j < ω.length.

The letter to delete is located by the left inversion sequence cs.leftInvSeq ω, whose j-th entry s_{i_1} ⋯ s_{i_j} ⋯ s_{i_1} is precisely the reflection that deleting the j-th letter performs (CoxeterSystem.getD_leftInvSeq_mul_wordProd). Mathlib proves that every entry of the inversion sequence of a reduced word is a left inversion; the content here is the converse, that every left inversion occurs in the inversion sequence of any word — so that for a reduced word the two lists agree.

The exchange condition (the case of a simple reflection) and the deletion condition (a word that is not reduced can be shortened by deleting two of its letters) follow.

Two elementary facts about reduced words are recorded first, both read off the length equation that reducedness is: a reduced word repeats no letter adjacently, and prefixing a reduced word for s_i * w by a left descent i of w gives a reduced word for w.

Main results

• CoxeterSystem.IsReduced.isChain_ne: a reduced word has no two adjacent equal letters.
• CoxeterSystem.IsReduced.isLeftDescent_wordProd_cons: the first letter of a reduced word is a left descent of the element it spells.
• CoxeterSystem.isReduced_cons_of_isLeftDescent: a left descent i of w turns a reduced word for s_i * w into a reduced word for w.
• CoxeterSystem.isReduced_cons_of_not_isLeftDescent: if i is not a left descent of w, then i followed by a reduced word for w is a reduced word for s_i * w.
• CoxeterSystem.mem_rightInvSeq_of_isRightInversion and CoxeterSystem.mem_leftInvSeq_of_isLeftInversion: every inversion occurs in the inversion sequence of any word spelling the element.
• CoxeterSystem.mem_rightInvSeq_iff_isRightInversion and CoxeterSystem.mem_leftInvSeq_iff_isLeftInversion: the inversion sequence of a reduced word lists exactly the inversions of the element it spells.
• CoxeterSystem.strongExchange and CoxeterSystem.strongExchange_right: the strong exchange condition, in its left and right multiplication forms.
• CoxeterSystem.exchangeCondition and CoxeterSystem.exchangeCondition_right: the exchange condition, the case of a simple reflection, where the shortened word is again reduced.
• CoxeterSystem.simple_mul_eq_mul_simple_of_length_eq: if s i * w * s j has the length of w and s i * w that of w * s j, then s i * w = w * s j.
• CoxeterSystem.deletionCondition: the deletion condition, that a word which is not reduced spells the same element as the word with two of its letters deleted.
• CoxeterSystem.exists_isReduced_sublist: every word has a reduced sublist spelling the same element.

References

Mathlib/GroupTheory/Coxeter/Inversion.lean records, without proving it, that the inversion sequence of a reduced word for w consists of all of the inversions of w; that statement is CoxeterSystem.mem_rightInvSeq_iff_isRightInversion and CoxeterSystem.mem_leftInvSeq_iff_isLeftInversion below. The root-system-level statement for a Weyl group, proved from the geometry of the positive roots rather than from the reflection cocycle used here, is TauCeti.exists_wordProd_eraseIdx_eq_mul_ofIdx in TauCeti/LinearAlgebra/RootSystem/Inversions/StrongExchange.lean; it does not imply the present one, which is about an arbitrary Coxeter system.

• A. Björner and F. Brenti, Combinatorics of Coxeter Groups, Springer GTM 231 (2005), Sections 1.3 and 1.4, whose reflection cocycle this follows.
• N. Bourbaki, Groupes et algèbres de Lie, Chapitres IV-VI, Ch. IV, §1.4.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Sections 5.8 and 5.11.

Reduced words and left descents

theorem CoxeterSystem.IsReduced.isChain_ne {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {ω : List B} (hω : cs.IsReduced ω) : List.IsChain (fun (x1 x2 : B) => x1 ≠ x2) ω

A reduced word has no two adjacent equal letters. Deleting such a pair leaves the product unchanged and the word shorter, so the original word was not of minimal length.

theorem CoxeterSystem.IsReduced.isLeftDescent_wordProd_cons {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {a : B} {ω : List B} (hω : cs.IsReduced (a :: ω)) : cs.IsLeftDescent (cs.wordProd (a :: ω)) a

The first letter of a reduced word is a left descent of the element it spells.

theorem CoxeterSystem.isReduced_cons_of_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {w : W} (hd : cs.IsLeftDescent w i) {ω : List B} (hω : cs.IsReduced ω) (hprod : cs.wordProd ω = cs.simple i * w) : cs.IsReduced (i :: ω)

A left descent i of w turns a reduced word for cs.simple i * w into a reduced word for w: the length equation it must satisfy is exactly the defining property of a left descent.

theorem CoxeterSystem.isReduced_cons_of_not_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i : B} {w : W} (hd : ¬cs.IsLeftDescent w i) {ω : List B} (hω : cs.IsReduced ω) (hprod : cs.wordProd ω = w) : cs.IsReduced (i :: ω)

If i is not a left descent of w, then prefixing i to a reduced word for w gives a reduced word for cs.simple i * w.

The reflection cocycle

The inversion sequence lists the inversions

theorem CoxeterSystem.mem_rightInvSeq_of_isRightInversion {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) {t : W} (ht : cs.IsRightInversion (cs.wordProd ω) t) : t ∈ cs.rightInvSeq ω

Every right inversion occurs in the right inversion sequence of any word spelling the element. This is the strong exchange condition in its membership form; no reducedness is needed.

theorem CoxeterSystem.mem_leftInvSeq_of_isLeftInversion {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) {t : W} (ht : cs.IsLeftInversion (cs.wordProd ω) t) : t ∈ cs.leftInvSeq ω

Every left inversion occurs in the left inversion sequence of any word spelling the element.

@[simp]

theorem CoxeterSystem.mem_rightInvSeq_iff_isRightInversion {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : cs.IsReduced ω) {t : W} : t ∈ cs.rightInvSeq ω ↔ cs.IsRightInversion (cs.wordProd ω) t

The right inversion sequence of a reduced word lists exactly the right inversions of the element it spells. The forward implication is CoxeterSystem.isRightInversion_of_mem_rightInvSeq; the converse holds for any word.

@[simp]

theorem CoxeterSystem.mem_leftInvSeq_iff_isLeftInversion {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : cs.IsReduced ω) {t : W} : t ∈ cs.leftInvSeq ω ↔ cs.IsLeftInversion (cs.wordProd ω) t

The left inversion sequence of a reduced word lists exactly the left inversions of the element it spells.

The strong exchange condition

theorem CoxeterSystem.strongExchange {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} {t : W} (ht : cs.IsLeftInversion (cs.wordProd ω) t) : ∃ j < ω.length, t * cs.wordProd ω = cs.wordProd (ω.eraseIdx j)

The strong exchange condition. If a reflection t shortens the element spelled by the word ω on the left, then t * π ω is spelled by ω with one letter deleted. The word ω need not be reduced.

theorem CoxeterSystem.strongExchange_right {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} {t : W} (ht : cs.IsRightInversion (cs.wordProd ω) t) : ∃ j < ω.length, cs.wordProd ω * t = cs.wordProd (ω.eraseIdx j)

The strong exchange condition, in the form for multiplication on the right.

theorem CoxeterSystem.exchangeCondition {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : cs.IsReduced ω) {i : B} (hi : cs.IsLeftDescent (cs.wordProd ω) i) : ∃ j < ω.length, cs.simple i * cs.wordProd ω = cs.wordProd (ω.eraseIdx j) ∧ cs.IsReduced (ω.eraseIdx j)

The exchange condition: if a simple reflection is a left descent of the element spelled by a reduced word, then multiplying by it deletes one letter of the word, and the shortened word is again reduced. Unlike in strongExchange, the length drops by exactly one here, so the hypothesis that ω is reduced buys the reducedness of ω.eraseIdx j.

theorem CoxeterSystem.exchangeCondition_right {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : cs.IsReduced ω) {i : B} (hi : cs.IsRightDescent (cs.wordProd ω) i) : ∃ j < ω.length, cs.wordProd ω * cs.simple i = cs.wordProd (ω.eraseIdx j) ∧ cs.IsReduced (ω.eraseIdx j)

The exchange condition, in the form for multiplication on the right.

theorem CoxeterSystem.simple_mul_eq_mul_simple_of_length_eq {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {i j : B} {w : W} (h₁ : cs.length (cs.simple i * w * cs.simple j) = cs.length w) (h₂ : cs.length (cs.simple i * w) = cs.length (w * cs.simple j)) : cs.simple i * w = w * cs.simple j

If ℓ (s i * w * s j) = ℓ w and ℓ (s i * w) = ℓ (w * s j), then s i * w = w * s j. This is the case in which multiplying w by s i on the left and by s j on the right cannot be told apart by lengths alone; it is what makes the left and right regular actions of an Iwahori–Hecke algebra commute (J. E. Humphreys, Reflection Groups and Coxeter Groups, Chapter 7).

The deletion condition

theorem CoxeterSystem.deletionCondition {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B} (hω : ¬cs.IsReduced ω) : ∃ (j : ℕ) (k : ℕ), j < k ∧ k < ω.length ∧ cs.wordProd ω = cs.wordProd ((ω.eraseIdx k).eraseIdx j)

The deletion condition: a word that is not reduced spells the same element as the word with two of its letters deleted.

theorem CoxeterSystem.exists_isReduced_sublist {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : ∃ (σ : List B), σ.Sublist ω ∧ cs.IsReduced σ ∧ cs.wordProd σ = cs.wordProd ω

Every word has a reduced sublist spelling the same element. This shrinks an arbitrary word to a reduced one without leaving the sublists of the original, so a subword of a given word can always be taken to be a reduced word for the element it spells.