Products of double cosets in a two-cell decomposition

Suppose the group G is the union of a subgroup B and a single double coset B n B with n² ∈ B, as happens for the Bruhat decomposition of a group of Lie rank one. Then left multiplication by the big cell B n B sends a double coset B w B, with w ∈ B or w ∈ n B, into the union of B (n w) B and B w B. This is the multiplication axiom of a Tits system of rank one.

Main statements

• Subgroup.doubleCoset_mul_doubleCoset_subset_union: in a two-cell decomposition G = B ∪ B n B with n² ∈ B, the product (B n B) (B w B) lies in B (n w) B ∪ B w B.

References

• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.1.

theorem Subgroup.doubleCoset_mul_doubleCoset_subset_union {G : Type u_1} [Group G] (B : Subgroup G) {n w : G} (hn : n * n ∈ B) (hw : w ∈ B ∨ n⁻¹ * w ∈ B) (hbruhat : ∀ (g : G), g ∈ B ∨ g ∈ DoubleCoset.doubleCoset n ↑B ↑B) : DoubleCoset.doubleCoset n ↑B ↑B * DoubleCoset.doubleCoset w ↑B ↑B ⊆ DoubleCoset.doubleCoset (n * w) ↑B ↑B ∪ DoubleCoset.doubleCoset w ↑B ↑B

In the presence of a two-cell decomposition G = B ∪ B n B with n² ∈ B, left multiplication of a cell B w B, where w ∈ B or w ∈ n B, by B n B produces at most B (n w) B and B w B.