The length function on the Weyl group of a Tits system

The simple reflections of a Tits system generate its Weyl group W = N / (B ∩ N), so they form a generating family TauCeti.TitsSystem.simpleGenerators in the sense of Group.Generators. Mathlib's word length Group.Generators.wordLength with respect to that family is the length function ℓ of the Weyl group: the least number of simple reflections whose product is a given element.

Because every simple reflection is an involution, a word in the generators and their inverses evaluates to the product of the underlying list of simple reflections. This file records that translation, so that the length can be read off plain lists of simple reflections, together with the elementary estimates that the multiplication rules for Bruhat cells rest on: a simple reflection has length one, and multiplying by one changes the length by at most one.

Main declarations

• TauCeti.TitsSystem.simpleGenerators: the simple reflections as a generating family of the Weyl group.
• TauCeti.TitsSystem.wordLength_le_iff: the length is at most n exactly when the element is the product of at most n simple reflections.
• TauCeti.TitsSystem.exists_prod_eq_of_wordLength: every element is the product of a list of simple reflections whose length is its word length, that is, of a reduced word.
• TauCeti.TitsSystem.wordLength_simple: a simple reflection has length one.
• TauCeti.TitsSystem.wordLength_simple_mul_le and TauCeti.TitsSystem.wordLength_le_wordLength_simple_mul_add_one: multiplication by a simple reflection changes the length by at most one.
• TauCeti.TitsSystem.wordLength_mul_simple_eq_wordLength_simple_mul_inv: since the length is invariant under inversion, right multiplication by a simple reflection is governed by left multiplication on the inverse.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter IV, §1, no. 1 and §2, no. 4.
• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.3.

noncomputable def TauCeti.TitsSystem.simpleGenerators {G : Type u} [Group G] (T : TitsSystem G) : Group.Generators T.WeylGroup ↑T.simple

The simple reflections, as a generating family of the Weyl group.

@[simp]

theorem TauCeti.TitsSystem.simpleGenerators_val {G : Type u} [Group G] (T : TitsSystem G) : T.simpleGenerators.val = Subtype.val

The generating family of simple reflections is the inclusion of T.simple.

@[simp]

theorem TauCeti.TitsSystem.wordProd_eq_prod {G : Type u} [Group G] (T : TitsSystem G) (l : List (↑T.simple × Bool)) : T.simpleGenerators.wordProd l = (List.map (fun (x : ↑T.simple × Bool) => ↑x.1) l).prod

A word in the simple reflections and their inverses evaluates to the product of the underlying list of simple reflections.

theorem TauCeti.TitsSystem.prod_reverse_eq_inv_prod {G : Type u} [Group G] (T : TitsSystem G) {l : List T.WeylGroup} (hl : ∀ s ∈ l, s ∈ T.simple) : l.reverse.prod = l.prod⁻¹

Reversing a list of simple reflections inverts its product.

theorem TauCeti.TitsSystem.wordLength_le_iff {G : Type u} [Group G] (T : TitsSystem G) {w : T.WeylGroup} {n : ℕ} : T.simpleGenerators.wordLength w ≤ n ↔ ∃ (l : List T.WeylGroup), (∀ s ∈ l, s ∈ T.simple) ∧ l.length ≤ n ∧ l.prod = w

Length through lists of simple reflections. The length of w is at most n exactly when w is the product of a list of at most n simple reflections.

theorem TauCeti.TitsSystem.wordLength_prod_le {G : Type u} [Group G] (T : TitsSystem G) {l : List T.WeylGroup} (hl : ∀ s ∈ l, s ∈ T.simple) : T.simpleGenerators.wordLength l.prod ≤ l.length

The product of a list of simple reflections has length at most the length of the list.

theorem TauCeti.TitsSystem.exists_prod_eq_of_wordLength {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) : ∃ (l : List T.WeylGroup), (∀ s ∈ l, s ∈ T.simple) ∧ l.length = T.simpleGenerators.wordLength w ∧ l.prod = w

Every element of the Weyl group is the product of a list of simple reflections whose length is the word length of the element: a reduced word.

@[simp]

theorem TauCeti.TitsSystem.wordLength_simple {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) : T.simpleGenerators.wordLength s = 1

A simple reflection has length one.

theorem TauCeti.TitsSystem.wordLength_simple_mul_le {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) (w : T.WeylGroup) : T.simpleGenerators.wordLength (s * w) ≤ T.simpleGenerators.wordLength w + 1

Left multiplication by a simple reflection increases the length by at most one.

theorem TauCeti.TitsSystem.wordLength_mul_simple_le {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) : T.simpleGenerators.wordLength (w * s) ≤ T.simpleGenerators.wordLength w + 1

Right multiplication by a simple reflection increases the length by at most one.

theorem TauCeti.TitsSystem.wordLength_le_wordLength_simple_mul_add_one {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) (w : T.WeylGroup) : T.simpleGenerators.wordLength w ≤ T.simpleGenerators.wordLength (s * w) + 1

Left multiplication by a simple reflection decreases the length by at most one.

theorem TauCeti.TitsSystem.wordLength_le_wordLength_mul_simple_add_one {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) : T.simpleGenerators.wordLength w ≤ T.simpleGenerators.wordLength (w * s) + 1

Right multiplication by a simple reflection decreases the length by at most one.

theorem TauCeti.TitsSystem.wordLength_mul_simple_eq_wordLength_simple_mul_inv {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) : T.simpleGenerators.wordLength (w * s) = T.simpleGenerators.wordLength (s * w⁻¹)

The length of w s is the length of s w⁻¹.