theorem BNPair.B_subset_standardParabolic {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S' : Set B_idx) : ↑bp.B ⊆ bp.standardParabolic S'

The Borel $B$ is contained in every standard parabolic $P_{S'} = BW_{S'}B$, via the trivial cell $B \cdot 1 \cdot B = B$.

theorem BNPair.lift_mem_bruhatCell {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (n : ↥bp.N) : ↑n ∈ bp.bruhatCell (bp.π n)

Any $N$-lift $n$ of $w = \pi(n)$ lies in its own Bruhat cell: $n \in BnB \subseteq B \cdot n \cdot B$.

theorem BNPair.bruhatCell_subset_standardParabolic {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S' : Set B_idx) (w : M.Group) (hw : w ∈ bp.parabolicSubgroupW S') : bp.bruhatCell w ⊆ bp.standardParabolic S'

If $w \in W_{S'}$ then the Bruhat cell $BwB$ is contained in the standard parabolic $P_{S'} = \bigcup_{u \in W_{S'}} BuB$.

theorem BNPair.bruhatCell_mul_B_right' {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g b : G} (hg : g ∈ bp.bruhatCell w) (hb : b ∈ bp.B) : g * b ∈ bp.bruhatCell w

Bruhat cells absorb right multiplication by $B$: if $g \in BwB$ and $b \in B$ then $gb \in BwB$.

theorem BNPair.bruhatCell_mul_B_left' {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g b : G} (hb : b ∈ bp.B) (hg : g ∈ bp.bruhatCell w) : b * g ∈ bp.bruhatCell w

Bruhat cells absorb left multiplication by $B$: if $b \in B$ and $g \in BwB$ then $bg \in BwB$.

theorem BNPair.simple_inv_eq {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (s : B_idx) : (M.toCoxeterSystem.simple s)⁻¹ = M.toCoxeterSystem.simple s

Simple reflections are involutions in $W$: $s^{-1} = s$ for every $s \in S$.

theorem BNPair.cell_mul_simple_right_coset {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S₂ : Set B_idx) (v : M.Group) (s : B_idx) (hs : s ∈ S₂) (g₁ g₂ : G) (hg₁ : g₁ ∈ bp.bruhatCell v) (hg₂ : g₂ ∈ bp.bruhatCell (M.toCoxeterSystem.simple s)) : ∃ (v' : M.Group), (∃ u₂ ∈ ↑(bp.parabolicSubgroupW S₂), v' = v * u₂) ∧ g₁ * g₂ ∈ bp.bruhatCell v'

Right multiplication by a single simple-reflection cell: $BvB \cdot BsB$ lands in $Bv'B$ for some $v' = vu_2$ with $u_2 \in W_{S_2}$. The exchange condition picks either $v' = vs$ or $v' = v$.

theorem BNPair.cell_mul_right_coset {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S₂ : Set B_idx) (v u₂ : M.Group) (hu₂ : u₂ ∈ bp.parabolicSubgroupW S₂) (g₁ g₂ : G) (hg₁ : g₁ ∈ bp.bruhatCell v) (hg₂ : g₂ ∈ bp.bruhatCell u₂) : ∃ (v' : M.Group), (∃ u₂' ∈ ↑(bp.parabolicSubgroupW S₂), v' = v * u₂') ∧ g₁ * g₂ ∈ bp.bruhatCell v'

Right cell-by-coset multiplication. For $u_2 \in W_{S_2}$, the product $BvB \cdot Bu_2B$ is contained in $\bigcup_{u_2' \in W_{S_2}} B(vu_2')B$. Proved by induction on a word for $u_2$ in the simple reflections of $S_2$, using cell_mul_simple_right_coset at each step.

theorem BNPair.cell_mul_simple_left {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (bd : bp.BruhatProperties) (v : M.Group) (s : B_idx) (g₁ g₂ : G) (hg₁ : g₁ ∈ bp.bruhatCell (M.toCoxeterSystem.simple s)) (hg₂ : g₂ ∈ bp.bruhatCell v) : g₁ * g₂ ∈ bp.bruhatCell (M.toCoxeterSystem.simple s * v) ∨ g₁ * g₂ ∈ bp.bruhatCell v

Left multiplication by a simple-reflection cell: $BsB \cdot BvB$ lies in either $B(sv)B$ or $BvB$, depending on whether $\ell(sv) > \ell(v)$. Dual to cell_mul_simple_right_coset, proved by inverting and applying that result.

theorem BNPair.cell_mul_left_coset {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (bd : bp.BruhatProperties) (S₁ : Set B_idx) (u₁ v : M.Group) (hu₁ : u₁ ∈ bp.parabolicSubgroupW S₁) (g₁ g₂ : G) (hg₁ : g₁ ∈ bp.bruhatCell u₁) (hg₂ : g₂ ∈ bp.bruhatCell v) : ∃ (v' : M.Group), (∃ u₁' ∈ ↑(bp.parabolicSubgroupW S₁), v' = u₁' * v) ∧ g₁ * g₂ ∈ bp.bruhatCell v'

Left cell-by-coset multiplication. For $u_1 \in W_{S_1}$, the product $Bu_1B \cdot BvB$ lands in $\bigcup_{u_1' \in W_{S_1}} B(u_1'v)B$. Dual to cell_mul_right_coset, proved by induction on a word for $u_1$ in simple reflections.

theorem BNPair.doubleCoset_injectivity {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (bd : bp.BruhatProperties) (S₁ S₂ : Set B_idx) (w w' : M.Group) (g : G) (hg_cell : g ∈ bp.bruhatCell w') (hg_coset : ∃ p₁ ∈ bp.standardParabolic S₁, ∃ p₂ ∈ bp.standardParabolic S₂, ∃ (n : ↥bp.N), bp.π n = w ∧ g = p₁ * ↑n * p₂) : w' ∈ bp.weylDoubleCoset S₁ S₂ w

Injectivity of the double-coset map $W_{S_1} \backslash W / W_{S_2} \to P_{S_1} \backslash G / P_{S_2}$. If $g \in Bw'B$ also admits a factorization $g = p_1 \cdot n \cdot p_2$ with $p_i \in P_{S_i}$ and $\pi(n) = w$, then $w'$ and $w$ represent the same $W_{S_1}\text{-}W_{S_2}$ double coset in $W$. Proved by combining cell_mul_right_coset and cell_mul_left_coset to bring the right-hand expression into $Bv'B$ with $v' \in W_{S_1} w W_{S_2}$, then using cell-disjointness.

theorem BNPair.doubleCoset_bijection {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (bd : bp.BruhatProperties) (S₁ S₂ : Set B_idx) (w w' : M.Group) : w' ∈ bp.weylDoubleCoset S₁ S₂ w ↔ ∀ (n : ↥bp.N), bp.π n = w → ∀ (n' : ↥bp.N), bp.π n' = w' → ↑n' ∈ doubleCoset (bp.standardParabolic S₁) (bp.standardParabolic S₂) ↑n

Main theorem of §5.4 (Bourbaki): the bijection $W_{S_1} \backslash W / W_{S_2} \;\longleftrightarrow\; P_{S_1} \backslash G / P_{S_2}$, sending $W_{S_1} w W_{S_2}$ to $P_{S_1} \cdot n \cdot P_{S_2}$ for any $N$-lift $n$ of $w$. Concretely: $w' \in W_{S_1} w W_{S_2}$ iff for every pair of $N$-lifts $n \in \pi^{-1}(w)$, $n' \in \pi^{-1}(w')$ we have $n' \in P_{S_1} n P_{S_2}$. The forward direction is a direct computation using the parabolic subgroup structure; the reverse direction is doubleCoset_injectivity.