Subword expansion of products of Bruhat cells

For a Tits system, inversion carries the Bruhat cell indexed by w to the cell indexed by w⁻¹. Consequently the left-handed rank-one multiplication law also holds on the right: if s is simple, then (B w B)(B s B) is either B (w s) B or its union with B w B.

Iterating the rank-one law gives the subword expansion needed for the uniqueness part of Bruhat decomposition. If s₁, …, sₙ are simple, every element of

(B s₁ B) ⋯ (B sₙ B)

lies in the cell indexed by the product of some subword of s₁, …, sₙ. No reducedness hypothesis is needed for this upper bound.

Main results

• TauCeti.TitsSystem.inv_bruhatCell: inversion of a Weyl-indexed cell.
• TauCeti.TitsSystem.bruhatCell_mul_eq_or_eq_union_of_mem_simple_right: right multiplication by a simple cell.
• TauCeti.TitsSystem.subset_bruhatCell_mul_of_mem_simple_right and TauCeti.TitsSystem.bruhatCell_mul_subset_union_of_mem_simple_right: the adjacent cell always occurs in the product with a simple cell on the right, and nothing beyond the adjacent and the original cell does.
• TauCeti.TitsSystem.exists_sublist_of_mem_prod_bruhatCell: the subword expansion for a product of simple cells.

Roadmap

This is the next combinatorial input toward injectivity of the Weyl-to-double-coset map and the Coxeter-system consequences of a Tits system in Layer 7, "Bruhat decomposition and BN-pairs / Tits systems", of TauCetiRoadmap/ReductiveGroups/README.md.

References

• J. E. Humphreys, Linear Algebraic Groups (1975), Sections 29.1--29.2.
• T. A. Springer, Linear Algebraic Groups, second edition (1998), Section 8.3.

@[simp]

theorem TauCeti.TitsSystem.inv_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) : (T.bruhatCell w)⁻¹ = T.bruhatCell w⁻¹

Inversion carries the Bruhat cell indexed by w to the cell indexed by w⁻¹.

theorem TauCeti.TitsSystem.bruhatCell_mul_eq_or_eq_union_of_mem_simple_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.bruhatCell s = T.bruhatCell (w * s) ∪ T.bruhatCell w

Right multiplication by a simple Bruhat cell. For a Weyl-group element w and a simple reflection s, the product of their cells is either the cell at w * s or its union with the cell at w.

theorem TauCeti.TitsSystem.subset_bruhatCell_mul_of_mem_simple_right {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) {s : T.WeylGroup} (hs : s ∈ T.simple) : T.bruhatCell (w * s) ⊆ T.bruhatCell w * T.bruhatCell s

The adjacent cell always occurs in the product with a simple cell on the right.

theorem TauCeti.TitsSystem.bruhatCell_mul_subset_union_of_mem_simple_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

The product with a simple cell on the right lies in the union of the adjacent and the original cell.

theorem TauCeti.TitsSystem.exists_sublist_of_mem_prod_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) {l : List T.WeylGroup} (hs : ∀ s ∈ l, s ∈ T.simple) {g : G} (hg : g ∈ (List.map T.bruhatCell l).prod) : ∃ (q : List T.WeylGroup), q.Sublist l ∧ g ∈ T.bruhatCell q.prod

The product of simple Bruhat cells is contained in the union of the cells indexed by subwords. Explicitly, every element of that product lies in the cell indexed by the product of some sublist of the original word.