The exchange condition for the Weyl group of a Tits system

Let (B, N) be a Tits system with Weyl group W, simple reflections S, and length function ℓ. This file proves that the pair (W, S) satisfies the exchange condition: if s is a simple reflection, w = s₁ ⋯ s_q is a product of simple reflections, and ℓ (s w) < ℓ w, then

s w = s₁ ⋯ s_{j-1} s_{j+1} ⋯ s_q

for some j, that is, s w is spelled by the same word with one letter deleted. No reducedness is assumed of the word s₁ ⋯ s_q; when it is reduced, the shortened word is reduced as well, because ℓ (s w) + 1 = ℓ w by TauCeti.TitsSystem.wordLength_simple_mul. The mirror statement for ℓ (w s) < ℓ w holds as well.

Following Bourbaki, the exchange condition is obtained from the Bruhat cells. Its combinatorial core is a rank-one statement: if (B s B)(B w B) is the single cell B (s w) B but (B s B)(B w s' B) is not the single cell B (s w s') B, then s w = w s'. Since the single-cell alternative of the rank-one multiplication law holds exactly when s increases the length, this rank-one statement yields the exchange condition for words of any length. The exchange condition is one of the characterizations of Coxeter systems (Bourbaki, Chapter IV, §1, no. 6); identifying (W, S) as a Coxeter system is not part of this file.

Main declarations

• TauCeti.TitsSystem.simple_mul_eq_mul_simple_of_bruhatCell_mul_ne: the rank-one exchange step on cells.
• TauCeti.TitsSystem.exists_eraseIdx_prod_eq_of_bruhatCell_mul_ne: the exchange condition phrased with cells, for any word whose product w has (B s B)(B w B) ≠ B (s w) B.
• TauCeti.TitsSystem.exists_eraseIdx_prod_eq_of_wordLength_lt: the exchange condition for the Weyl group of a Tits system.
• TauCeti.TitsSystem.exists_eraseIdx_prod_eq_of_wordLength_lt_right: the exchange condition for multiplication by a simple reflection on the right.
• TauCeti.TitsSystem.wordLength_simple_mul_simple_mul_simple_of_mul_ne: two simple reflections s and t that do not commute give a word s t s of length three.
• TauCeti.TitsSystem.exists_reduced_sublist: every word in simple reflections has a reduced subword with the same product.
• TauCeti.TitsSystem.simple_mem_weylClosure_iff: a subgroup generated by selected simple reflections contains no additional simple reflections.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter IV, §1, no. 5 and §2, no. 4, Theorem 2.
• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.3.
• T. A. Springer, Linear Algebraic Groups, second edition (1998), Section 8.3.

theorem TauCeti.TitsSystem.simple_mul_eq_mul_simple_of_bruhatCell_mul_ne {G : Type u} [Group G] (T : TitsSystem G) {s s' w : T.WeylGroup} (hs : s ∈ T.simple) (hs' : s' ∈ T.simple) (hw : T.bruhatCell s * T.bruhatCell w = T.bruhatCell (s * w)) (hws' : T.bruhatCell s * T.bruhatCell (w * s') ≠ T.bruhatCell (s * (w * s'))) : s * w = w * s'

The rank-one exchange step. If (B s B)(B w B) is the single cell B (s w) B while (B s B)(B w s' B) is not the single cell B (s w s') B, then s w = w s'.

theorem TauCeti.TitsSystem.exists_eraseIdx_prod_eq_of_bruhatCell_mul_ne {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) {l : List T.WeylGroup} (hl : ∀ x ∈ l, x ∈ T.simple) (h : T.bruhatCell s * T.bruhatCell l.prod ≠ T.bruhatCell (s * l.prod)) : ∃ j < l.length, s * l.prod = (l.eraseIdx j).prod

The exchange condition, in terms of cells. If w is the product of a list of simple reflections and (B s B)(B w B) is not the single cell B (s w) B, then s w is the product of the list with one letter deleted.

theorem TauCeti.TitsSystem.exists_eraseIdx_prod_eq_of_wordLength_lt {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) {l : List T.WeylGroup} (hl : ∀ x ∈ l, x ∈ T.simple) (h : T.simpleGenerators.wordLength (s * l.prod) < T.simpleGenerators.wordLength l.prod) : ∃ j < l.length, s * l.prod = (l.eraseIdx j).prod

The exchange condition. If w is the product of a list of simple reflections and the simple reflection s decreases its length, then s w is the product of the list with one letter deleted.

theorem TauCeti.TitsSystem.exists_eraseIdx_prod_eq_of_wordLength_lt_right {G : Type u} [Group G] (T : TitsSystem G) {l : List T.WeylGroup} (hl : ∀ x ∈ l, x ∈ T.simple) {s : T.WeylGroup} (hs : s ∈ T.simple) (h : T.simpleGenerators.wordLength (l.prod * s) < T.simpleGenerators.wordLength l.prod) : ∃ j < l.length, l.prod * s = (l.eraseIdx j).prod

The exchange condition on the right. If w is the product of a list of simple reflections and the simple reflection s decreases its length from the right, then w s is the product of the list with one letter deleted.

theorem TauCeti.TitsSystem.wordLength_simple_mul_simple_mul_simple_of_mul_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 * s) : T.simpleGenerators.wordLength (s * t * s) = 3

If two simple reflections s and t do not commute, then s t s has length three.

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

Every word in simple reflections contains a reduced subword with the same product. In particular, shortening a word never introduces a new simple reflection.

@[simp]

theorem TauCeti.TitsSystem.simple_mem_weylClosure_iff {G : Type u} [Group G] (T : TitsSystem G) (J : Set ↑T.simple) (s : ↑T.simple) : ↑s ∈ Subgroup.closure (Subtype.val '' J) ↔ s ∈ J

A simple reflection belongs to the subgroup generated by a selection of simple reflections exactly when it belongs to that selection.