The length function, reduced words, and descents

Throughout this file, B is a type and M : CoxeterMatrix B is a Coxeter matrix. cs : CoxeterSystem M W is a Coxeter system; that is, W is a group, and cs holds the data of a group isomorphism W ≃* M.group, where M.group refers to the quotient of the free group on B by the Coxeter relations given by the matrix M. See Mathlib/GroupTheory/Coxeter/Basic.lean for more details.

Given any element $w \in W$, its length (CoxeterSystem.length), denoted $\ell(w)$, is the minimum number $\ell$ such that $w$ can be written as a product of a sequence of $\ell$ simple reflections: $$w = s_{i_1} \cdots s_{i_\ell}.$$ We prove for all $w_1, w_2 \in W$ that $\ell (w_1 w_2) \leq \ell (w_1) + \ell (w_2)$ and that $\ell (w_1 w_2)$ has the same parity as $\ell (w_1) + \ell (w_2)$.

We define a reduced word (CoxeterSystem.IsReduced) for an element $w \in W$ to be a way of writing $w$ as a product of exactly $\ell(w)$ simple reflections. Every element of $W$ has a reduced word.

We say that $i \in B$ is a left descent (CoxeterSystem.IsLeftDescent) of $w \in W$ if $\ell(s_i w) < \ell(w)$. We show that if $i$ is a left descent of $w$, then $\ell(s_i w) + 1 = \ell(w)$. On the other hand, if $i$ is not a left descent of $w$, then $\ell(s_i w) = \ell(w) + 1$. We similarly define right descents (CoxeterSystem.IsRightDescent) and prove analogous results.

Main definitions

• cs.length
• cs.IsReduced
• cs.IsLeftDescent
• cs.IsRightDescent

References

• A. Björner and F. Brenti, Combinatorics of Coxeter Groups

Length

noncomputable def CoxeterSystem.length {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) : ℕ

The length of w; i.e., the minimum number of simple reflections that must be multiplied to form w.

def CoxeterSystem.IsReduced {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : Prop

The proposition that ω is reduced; that is, it has minimal length among all words that represent the same element of W.

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

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

@[deprecated CoxeterSystem.exists_isReduced (since := "2026-03-25")]

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

Alias of CoxeterSystem.exists_isReduced.

@[deprecated CoxeterSystem.exists_isReduced (since := "2026-03-25")]

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

Alias of CoxeterSystem.exists_isReduced.

theorem CoxeterSystem.length_wordProd_le {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : cs.length (cs.wordProd ω) ≤ ω.length

@[simp]

theorem CoxeterSystem.length_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : cs.length 1 = 0

@[simp]

theorem CoxeterSystem.length_eq_zero_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} : cs.length w = 0 ↔ w = 1

@[simp]

theorem CoxeterSystem.length_inv {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) : cs.length w⁻¹ = cs.length w

theorem CoxeterSystem.length_mul_le {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W) : cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂

theorem CoxeterSystem.length_le_length_mul_add_left {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W) : cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁

theorem CoxeterSystem.length_le_length_mul_add_right {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W) : cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂

@[deprecated CoxeterSystem.length_le_length_mul_add_right (since := "2026-03-25")]

theorem CoxeterSystem.length_mul_ge_length_sub_length {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W) : cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)

@[deprecated CoxeterSystem.length_le_length_mul_add_left (since := "2026-03-25")]

theorem CoxeterSystem.length_mul_ge_length_sub_length' {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W) : cs.length w₂ - cs.length w₁ ≤ cs.length (w₁ * w₂)

@[deprecated "use `length_le_length_mul_add_left` and `length_le_length_mul_add_right" (since := "2026-03-25")]

theorem CoxeterSystem.length_mul_ge_max {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W) : max (cs.length w₁ - cs.length w₂) (cs.length w₂ - cs.length w₁) ≤ cs.length (w₁ * w₂)

def CoxeterSystem.lengthParity {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : W →* Multiplicative (ZMod 2)

The homomorphism that sends each element w : W to the parity of the length of w. (See lengthParity_eq_ofAdd_length.)

theorem CoxeterSystem.lengthParity_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.lengthParity (cs.simple i) = Multiplicative.ofAdd 1

theorem CoxeterSystem.lengthParity_comp_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : ⇑cs.lengthParity ∘ cs.simple = fun (x : B) => Multiplicative.ofAdd 1

theorem CoxeterSystem.lengthParity_eq_ofAdd_length {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) : cs.lengthParity w = Multiplicative.ofAdd ↑(cs.length w)

theorem CoxeterSystem.length_mul_mod_two {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W) : cs.length (w₁ * w₂) % 2 = (cs.length w₁ + cs.length w₂) % 2

@[simp]

theorem CoxeterSystem.length_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : cs.length (cs.simple i) = 1

theorem CoxeterSystem.length_eq_one_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} : cs.length w = 1 ↔ ∃ (i : B), w = cs.simple i

theorem CoxeterSystem.length_mul_simple_ne {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : cs.length (w * cs.simple i) ≠ cs.length w

theorem CoxeterSystem.length_simple_mul_ne {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : cs.length (cs.simple i * w) ≠ cs.length w

theorem CoxeterSystem.length_mul_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : cs.length (w * cs.simple i) = cs.length w + 1 ∨ cs.length (w * cs.simple i) + 1 = cs.length w

theorem CoxeterSystem.length_simple_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w

Reduced words

@[simp]

theorem CoxeterSystem.isReduced_reverse_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) : cs.IsReduced ω.reverse ↔ cs.IsReduced ω

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

theorem CoxeterSystem.IsReduced.take {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {ω : List B} (hω : cs.IsReduced ω) (j : ℕ) : cs.IsReduced (List.take j ω)

theorem CoxeterSystem.IsReduced.drop {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {ω : List B} (hω : cs.IsReduced ω) (j : ℕ) : cs.IsReduced (List.drop j ω)

theorem CoxeterSystem.not_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 i i' ≠ 0) (hm : m > M.M i i') : ¬cs.IsReduced (alternatingWord i i' m)

Descents

def CoxeterSystem.IsLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : Prop

The proposition that i is a left descent of w; that is, $\ell(s_i w) < \ell(w)$.

def CoxeterSystem.IsRightDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) : Prop

The proposition that i is a right descent of w; that is, $\ell(w s_i) < \ell(w)$.

theorem CoxeterSystem.not_isLeftDescent_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : ¬cs.IsLeftDescent 1 i

theorem CoxeterSystem.not_isRightDescent_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) : ¬cs.IsRightDescent 1 i

theorem CoxeterSystem.isLeftDescent_inv_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B} : cs.IsLeftDescent w⁻¹ i ↔ cs.IsRightDescent w i

theorem CoxeterSystem.isRightDescent_inv_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B} : cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i

theorem CoxeterSystem.exists_leftDescent_of_ne_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} (hw : w ≠ 1) : ∃ (i : B), cs.IsLeftDescent w i

theorem CoxeterSystem.exists_rightDescent_of_ne_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} (hw : w ≠ 1) : ∃ (i : B), cs.IsRightDescent w i

theorem CoxeterSystem.isLeftDescent_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B} : cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) + 1 = cs.length w

theorem CoxeterSystem.not_isLeftDescent_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B} : ¬cs.IsLeftDescent w i ↔ cs.length (cs.simple i * w) = cs.length w + 1

theorem CoxeterSystem.isRightDescent_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B} : cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) + 1 = cs.length w

theorem CoxeterSystem.not_isRightDescent_iff {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B} : ¬cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) = cs.length w + 1

theorem CoxeterSystem.isLeftDescent_iff_not_isLeftDescent_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B} : cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (cs.simple i * w) i

theorem CoxeterSystem.isRightDescent_iff_not_isRightDescent_mul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B} : cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i