Bruhat decomposition of a Tits system

For a Tits system (B, N), every element of the ambient group belongs to a double coset B n B represented by an element n ∈ N. Thus the canonical map from N to B \ G / B is surjective, and the union of the Bruhat cells is the whole group.

The file also establishes the left rank-one multiplication law. If s is simple and w belongs to the Weyl group, then (B s B)(B w B) is either B (s w) B or B (s w) B ∪ B w B. This sharpens the subset appearing among the Tits-system axioms: the adjacent cell always occurs, and the product can acquire only the original cell in addition.

The proof uses the multiplication axiom first for a simple reflection. Since the simple reflections generate W = N / (B ∩ N) and are involutions, induction in W shows that left multiplication by any Bruhat cell preserves the union of the cells. That union is consequently a subgroup containing both B and N, hence is all of G by the generation axiom.

Inversion, the corresponding right multiplication law, and the subword expansion of a product of simple cells are developed in TauCeti.GroupTheory.TitsSystem.Bruhat.Subword.

Main declarations

• TauCeti.TitsSystem.bruhatCells: the union of the double cosets B n B, for n ∈ N.
• TauCeti.TitsSystem.bruhatCell: the Bruhat cell indexed by an element of the Weyl group.
• TauCeti.TitsSystem.mem_bruhatCell_iff: membership in a Weyl-indexed Bruhat cell in terms of a representative in N.
• TauCeti.TitsSystem.exists_mem_bruhatCell: every Weyl-indexed Bruhat cell contains a representative from N.
• TauCeti.TitsSystem.subgroupB_mul_bruhatCell and TauCeti.TitsSystem.bruhatCell_mul_subgroupB: the identity cell B is absorbed by every cell.
• TauCeti.TitsSystem.bruhatCells_eq_univ: the Bruhat cells cover the ambient group.
• TauCeti.TitsSystem.bruhatCell_mul_eq_or_eq_union_of_mem_simple: multiplication on the left by a simple Bruhat cell gives either the adjacent cell or its union with the original cell.
• TauCeti.TitsSystem.subset_bruhatCell_mul_of_mem_simple and TauCeti.TitsSystem.bruhatCell_mul_subset_union_of_mem_simple: the adjacent cell always occurs in the product with a simple cell on the left, and nothing beyond the adjacent and the original cell does.
• TauCeti.TitsSystem.bruhatCell_mul_self_eq_union_of_mem_simple: the square of a simple cell is its union with the identity cell.
• TauCeti.TitsSystem.exists_mem_doubleCoset: every group element lies in a cell represented by N.
• TauCeti.TitsSystem.doubleCosetMk_surjective: the induced map N → B \ G / B is surjective.

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.

This supplies the abstract Bruhat decomposition in Layer 7, "Bruhat decomposition and BN-pairs / Tits systems", of the ReductiveGroups roadmap.

def TauCeti.TitsSystem.bruhatCells {G : Type u} [Group G] (T : TitsSystem G) : Set G

The union of the Bruhat cells B n B represented by elements n of N.

theorem TauCeti.TitsSystem.mem_bruhatCells_iff {G : Type u} [Group G] (T : TitsSystem G) (g : G) : g ∈ T.bruhatCells ↔ ∃ (n : ↥T.subgroupN), g ∈ DoubleCoset.doubleCoset ↑n ↑T.subgroupB ↑T.subgroupB

An element lies in the union of Bruhat cells exactly when it lies in a cell represented by an element of N.

noncomputable def TauCeti.TitsSystem.bruhatCell {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) : Set G

The Bruhat cell B w B indexed by an element w of the Weyl group.

@[simp]

theorem TauCeti.TitsSystem.bruhatCell_mk {G : Type u} [Group G] (T : TitsSystem G) (n : ↥T.subgroupN) : T.bruhatCell ↑n = DoubleCoset.doubleCoset ↑n ↑T.subgroupB ↑T.subgroupB

The Bruhat cell at the class of n ∈ N is the double coset B n B.

theorem TauCeti.TitsSystem.mem_bruhatCell_iff {G : Type u} [Group G] (T : TitsSystem G) {g : G} {w : T.WeylGroup} : g ∈ T.bruhatCell w ↔ ∃ (n : ↥T.subgroupN), ↑n = w ∧ g ∈ DoubleCoset.doubleCoset ↑n ↑T.subgroupB ↑T.subgroupB

Membership in a Weyl-indexed Bruhat cell is witnessed by some representative in N.

theorem TauCeti.TitsSystem.bruhatCell_eq_doubleCoset {G : Type u} [Group G] (T : TitsSystem G) {g : G} {w : T.WeylGroup} (hg : g ∈ T.bruhatCell w) : T.bruhatCell w = DoubleCoset.doubleCoset g ↑T.subgroupB ↑T.subgroupB

A Bruhat cell is the double coset of any of its elements.

theorem TauCeti.TitsSystem.exists_mem_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) : ∃ (n : ↥T.subgroupN), ↑n = w ∧ ↑n ∈ T.bruhatCell w

Every Weyl-indexed Bruhat cell contains a representative from the normalizer subgroup.

@[simp]

theorem TauCeti.TitsSystem.bruhatCell_one {G : Type u} [Group G] (T : TitsSystem G) : T.bruhatCell 1 = ↑T.subgroupB

The Bruhat cell indexed by the identity of the Weyl group is B.

@[simp]

theorem TauCeti.TitsSystem.subgroupB_mul_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) : ↑T.subgroupB * T.bruhatCell w = T.bruhatCell w

The identity cell B (see TauCeti.TitsSystem.bruhatCell_one) is absorbed on the left: B (B w B) = B w B.

@[simp]

theorem TauCeti.TitsSystem.bruhatCell_mul_subgroupB {G : Type u} [Group G] (T : TitsSystem G) (w : T.WeylGroup) : T.bruhatCell w * ↑T.subgroupB = T.bruhatCell w

The identity cell B (see TauCeti.TitsSystem.bruhatCell_one) is absorbed on the right: (B w B) B = B w B.

theorem TauCeti.TitsSystem.bruhatCells_eq_iUnion_bruhatCell {G : Type u} [Group G] (T : TitsSystem G) : T.bruhatCells = ⋃ (w : T.WeylGroup), T.bruhatCell w

The union over N defining bruhatCells can equivalently be indexed canonically by the Weyl group.

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

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

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

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

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

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

@[simp]

theorem TauCeti.TitsSystem.bruhatCell_mul_self_eq_union_of_mem_simple {G : Type u} [Group G] (T : TitsSystem G) {s : T.WeylGroup} (hs : s ∈ T.simple) : T.bruhatCell s * T.bruhatCell s = T.bruhatCell 1 ∪ T.bruhatCell s

The square of a simple Bruhat cell is the union of that cell with the identity cell: (B s B)(B s B) = B ∪ B s B.

The nondegeneracy axiom rules out the smaller alternative in TauCeti.TitsSystem.bruhatCell_mul_eq_or_eq_union_of_mem_simple.

@[simp]

theorem TauCeti.TitsSystem.bruhatCells_eq_univ {G : Type u} [Group G] (T : TitsSystem G) : T.bruhatCells = Set.univ

The Bruhat cells cover the ambient group.

theorem TauCeti.TitsSystem.exists_mem_doubleCoset {G : Type u} [Group G] (T : TitsSystem G) (g : G) : ∃ (n : ↥T.subgroupN), g ∈ DoubleCoset.doubleCoset ↑n ↑T.subgroupB ↑T.subgroupB

Every element of the ambient group belongs to a Bruhat cell represented by an element of N.

theorem TauCeti.TitsSystem.doubleCosetMk_surjective {G : Type u} [Group G] (T : TitsSystem G) : Function.Surjective fun (n : ↥T.subgroupN) => DoubleCoset.mk T.subgroupB T.subgroupB ↑n

The canonical map from N to the double-coset quotient B \ G / B is surjective.