Documentation

TauCeti.GroupTheory.TitsSystem.Bruhat.Length

Bruhat cell multiplication and the length function #

Let (B, N) be a Tits system with Weyl group W and length function ℓ, the word length with respect to the simple reflections. The rank-one multiplication law leaves two possibilities for the product of a simple cell with an arbitrary cell:

(B s B)(B w B) = B (s w) B    or    (B s B)(B w B) = B (s w) B ∪ B w B.

This file decides between them by the length function: the first alternative holds exactly when ℓ (s w) > ℓ w, the second exactly when ℓ (s w) < ℓ w (Bourbaki, Chapter IV, §2, no. 4, Theorem 2). Multiplication of Bruhat cells by simple cells is thereby governed entirely by the length function on the Weyl group, which is the input for the exchange condition in TauCeti.GroupTheory.TitsSystem.Bruhat.Exchange.

Conversely the cells control the length: since one of the two alternatives always holds, a simple reflection never preserves the length, ℓ (s w) = ℓ w ± 1.

Every statement has a _right variant for multiplication by a simple cell on the right, because inversion carries the cell at w to the cell at w⁻¹ and preserves the length.

Main declarations #

References #

The rank-one law decided by the length function #

source
@[simp]
theorem TauCeti.TitsSystem.bruhatCell_mul_eq_of_wordLength_le {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) {w : T.WeylGroup} (hw : T.simpleGenerators.wordLength w ≤ T.simpleGenerators.wordLength (s * w)) :
T.bruhatCell s * T.bruhatCell w = T.bruhatCell (s * w)

Length-increasing multiplication. If ℓ w ≤ ℓ (s w), then (B s B)(B w B) = B (s w) B.

source
@[simp]
theorem TauCeti.TitsSystem.bruhatCell_mul_eq_union_of_wordLength_lt {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) {w : T.WeylGroup} (hw : T.simpleGenerators.wordLength (s * w) < T.simpleGenerators.wordLength w) :
T.bruhatCell s * T.bruhatCell w = T.bruhatCell (s * w) ∪ T.bruhatCell w

Length-decreasing multiplication. If ℓ (s w) < ℓ w, then (B s B)(B w B) = B (s w) B ∪ B w B.

source
theorem TauCeti.TitsSystem.wordLength_simple_mul_ne {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

A simple reflection never preserves the length.

source
theorem TauCeti.TitsSystem.wordLength_simple_mul {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 ∨ T.simpleGenerators.wordLength (s * w) + 1 = T.simpleGenerators.wordLength w

A simple reflection changes the length by exactly one on the left.

source
theorem TauCeti.TitsSystem.wordLength_simple_mul_simple_of_ne {G : Type u} [Group G] (T : TitsSystem G) {s t : T.WeylGroup} (hs : s ∈ T.simple) (ht : t ∈ T.simple) (hst : s ≠ t) :
T.simpleGenerators.wordLength (s * t) = 2

The product of two distinct simple reflections has length two.

source
@[simp]
theorem TauCeti.TitsSystem.bruhatCell_mul_eq_iff_wordLength_lt {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) (w : T.WeylGroup) :
T.bruhatCell s * T.bruhatCell w = T.bruhatCell (s * w) ↔ T.simpleGenerators.wordLength w < T.simpleGenerators.wordLength (s * w)

The two alternatives of the rank-one law are decided by the length: (B s B)(B w B) is the single cell B (s w) B exactly when s increases the length of w.

source
@[simp]
theorem TauCeti.TitsSystem.bruhatCell_mul_eq_union_iff_wordLength_lt {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) (w : T.WeylGroup) :
T.bruhatCell s * T.bruhatCell w = T.bruhatCell (s * w) ∪ T.bruhatCell w ↔ T.simpleGenerators.wordLength (s * w) < T.simpleGenerators.wordLength w

The two alternatives of the rank-one law are decided by the length: (B s B)(B w B) is the union B (s w) B ∪ B w B exactly when s decreases the length of w.

The right-handed versions #

source
theorem TauCeti.TitsSystem.wordLength_mul_simple_ne {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

A simple reflection never preserves the length, on the right.

source
theorem TauCeti.TitsSystem.wordLength_mul_simple {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 ∨ T.simpleGenerators.wordLength (w * s) + 1 = T.simpleGenerators.wordLength w

A simple reflection changes the length by exactly one on the right.

source
@[simp]
theorem TauCeti.TitsSystem.bruhatCell_mul_eq_of_wordLength_le_right {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) (hw : T.simpleGenerators.wordLength w ≤ T.simpleGenerators.wordLength (w * s)) :
T.bruhatCell w * T.bruhatCell s = T.bruhatCell (w * s)

Length-increasing multiplication on the right. If ℓ w ≤ ℓ (w s), then (B w B)(B s B) = B (w s) B.

source
@[simp]
theorem TauCeti.TitsSystem.bruhatCell_mul_eq_union_of_wordLength_lt_right {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) (hw : T.simpleGenerators.wordLength (w * s) < T.simpleGenerators.wordLength w) :
T.bruhatCell w * T.bruhatCell s = T.bruhatCell (w * s) ∪ T.bruhatCell w

Length-decreasing multiplication on the right. If ℓ (w s) < ℓ w, then (B w B)(B s B) = B (w s) B ∪ B w B.

source
@[simp]
theorem TauCeti.TitsSystem.bruhatCell_mul_eq_iff_wordLength_lt_right {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) :
T.bruhatCell w * T.bruhatCell s = T.bruhatCell (w * s) ↔ T.simpleGenerators.wordLength w < T.simpleGenerators.wordLength (w * s)

On the right, (B w B)(B s B) is the single cell B (w s) B exactly when s increases the length of w.

source
@[simp]
theorem TauCeti.TitsSystem.bruhatCell_mul_eq_union_iff_wordLength_lt_right {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) :
T.bruhatCell w * T.bruhatCell s = T.bruhatCell (w * s) ∪ T.bruhatCell w ↔ T.simpleGenerators.wordLength (w * s) < T.simpleGenerators.wordLength w

On the right, (B w B)(B s B) is the union B (w s) B ∪ B w B exactly when s decreases the length of w.