Uniqueness in Bruhat decomposition

The Bruhat cells of a Tits system are indexed injectively by its Weyl group. Together with the covering theorem, this gives the disjoint decomposition G = ⨆ w ∈ W, B w B: every element belongs to exactly one Weyl-indexed cell. Consequently containment of cells is equality of their indices, and a cell contained in a union of two cells is one of the two.

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_injective {G : Type u} [Group G] (T : TitsSystem G) : Function.Injective T.bruhatCell

Distinct Weyl elements index distinct Bruhat cells.

@[simp]

theorem TauCeti.TitsSystem.bruhatCell_inj {G : Type u} [Group G] (T : TitsSystem G) {w v : T.WeylGroup} : T.bruhatCell w = T.bruhatCell v ↔ w = v

Equality of Bruhat cells is equality of their Weyl indices.

theorem TauCeti.TitsSystem.eq_of_mem_bruhatCell_of_mem {G : Type u} [Group G] (T : TitsSystem G) {g : G} {w v : T.WeylGroup} (hw : g ∈ T.bruhatCell w) (hv : g ∈ T.bruhatCell v) : w = v

Two cells sharing an element have the same Weyl index.

@[simp]

theorem TauCeti.TitsSystem.bruhatCell_subset_iff {G : Type u} [Group G] (T : TitsSystem G) {w v : T.WeylGroup} : T.bruhatCell w ⊆ T.bruhatCell v ↔ w = v

Containment of Bruhat cells is equality of their Weyl indices.

theorem TauCeti.TitsSystem.eq_or_eq_of_bruhatCell_subset_union {G : Type u} [Group G] (T : TitsSystem G) {w u v : T.WeylGroup} (h : T.bruhatCell w ⊆ T.bruhatCell u ∪ T.bruhatCell v) : w = u ∨ w = v

A Bruhat cell contained in the union of two cells is one of them.

@[simp]

theorem TauCeti.TitsSystem.disjoint_bruhatCell_iff {G : Type u} [Group G] (T : TitsSystem G) {w v : T.WeylGroup} : Disjoint (T.bruhatCell w) (T.bruhatCell v) ↔ w ≠ v

Two Bruhat cells are disjoint exactly when their Weyl indices differ.

theorem TauCeti.TitsSystem.existsUnique_mem_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) (g : G) : ∃! w : T.WeylGroup, g ∈ T.bruhatCell w

Bruhat decomposition: every group element belongs to a unique Weyl-indexed cell.