The identity Bruhat cell is disjoint from the other cells

The Weyl group of a Tits system is N / (B ∩ N), so a representative in N lying in B represents the identity. Consequently the identity double coset B cannot meet the Bruhat cell of any nonidentity Weyl element. This file records that first separation result for the Bruhat cells of a Tits system.

In particular, by TauCeti.TitsSystem.simple_ne_one, it is the length-zero/one base case for the injectivity part of Bruhat decomposition: the Weyl-indexed cell at a simple reflection is genuinely a new cell, rather than another presentation of B.

Main declarations

• TauCeti.TitsSystem.bruhatCell_one_disjoint_bruhatCell proves that the identity cell and the cell of a nonidentity Weyl element are disjoint.
• TauCeti.TitsSystem.bruhatCell_ne_bruhatCell_one is the corresponding non-equality of cells.

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.

theorem TauCeti.TitsSystem.bruhatCell_one_disjoint_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) {w : T.WeylGroup} (hw : w ≠ 1) : Disjoint (T.bruhatCell 1) (T.bruhatCell w)

The identity Bruhat cell is disjoint from the Bruhat cell of every nonidentity Weyl element.

theorem TauCeti.TitsSystem.bruhatCell_ne_bruhatCell_one {G : Type u} [Group G] (T : TitsSystem G) {w : T.WeylGroup} (hw : w ≠ 1) : T.bruhatCell w ≠ T.bruhatCell 1

The Bruhat cell of a nonidentity Weyl element is not the identity Bruhat cell.