Documentation

Mathlib.GroupTheory.Coxeter.Length

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 $ℓ (w)$ , is the minimum number $ℓ$ such that $w$ can be written as a product of a sequence of $ℓ$ simple reflections: $w = s_{i_{1}} \dots s_{i_{ℓ}} .$ We prove for all $w_{1}, w_{2} \in W$ that $ℓ (w_{1} w_{2}) \leq ℓ (w_{1}) + ℓ (w_{2})$ and that $ℓ (w_{1} w_{2})$ has the same parity as $ℓ (w_{1}) + ℓ (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 $ℓ (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 $ℓ (s_{i} w) < ℓ (w)$ . We show that if $i$ is a left descent of $w$ , then $ℓ (s_{i} w) + 1 = ℓ (w)$ . On the other hand, if $i$ is not a left descent of $w$ , then $ℓ (s_{i} w) = ℓ (w) + 1$ . We similarly define right descents (CoxeterSystem.IsRightDescent) and prove analogous results.

Main definitions #

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.

Equations

cs.length w = Nat.find ⋯

Instances For

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), ω.length = cs.length w ∧ w = cs.wordProd ω

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₂ : W) :

cs.length (w₁ * w₂) ≤ cs.length w₁ + cs.length w₂

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₂ : W) :

cs.length w₁ - cs.length w₂ ≤ cs.length (w₁ * w₂)

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₂ : W) :

cs.length w₂ - cs.length w₁ ≤ cs.length (w₁ * w₂)

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₂ : 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.)

Equations

cs.lengthParity = cs.lift ⟨fun (x : B) => Multiplicative.ofAdd 1, ⋯⟩

Instances For

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₂ : 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 #

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

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

Equations

cs.IsReduced ω = (cs.length (cs.wordProd ω) = ω.length)

Instances For

@[simp]

theorem CoxeterSystem.isReduced_reverse {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.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 ω

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 : B) (i' : B) {m : ℕ} (hM : M.M i i' ≠ 0) (hm : m > M.M i i') :

¬cs.IsReduced (CoxeterSystem.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) :

The proposition that i is a left descent of w; that is, $ℓ (s_{i} w) < ℓ (w)$ .

Equations

cs.IsLeftDescent w i = (cs.length (cs.simple i * w) < cs.length w)

Instances For

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

The proposition that i is a right descent of w; that is, $ℓ (w s_{i}) < ℓ (w)$ .

Equations

cs.IsRightDescent w i = (cs.length (w * cs.simple i) < cs.length w)

Instances For

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