theorem SubgroupOverB.cell_sub_of_mem {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (P : Subgroup G) (hBP : bp.B ≤ P) (w : M.Group) (g : G) (hgP : g ∈ ↑P) (hgW : g ∈ bp.bruhatCell w) : bp.bruhatCell w ⊆ ↑P

If $B \leq P$ and some $g \in BwB$ lies in $P$, then the whole Bruhat cell $BwB$ is contained in $P$. Proof: factor $g$ in $BnB$ form, deduce $n \in P$, then any other lift $n'$ of $w$ differs from $n$ by a $T \subseteq B \subseteq P$ element.

theorem SubgroupOverB.N_rep_mem_P_of_parabolicW {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (P : Subgroup G) (hBP : bp.B ≤ P) (S' : Set B_idx) (hS' : ∀ s ∈ S', bp.bruhatCell (M.toCoxeterSystem.simple s) ⊆ ↑P) (w : M.Group) (hw : w ∈ bp.parabolicSubgroupW S') (n : ↥bp.N) (hn : bp.π n = w) : ↑n ∈ ↑P

If every simple cell $BsB$ for $s \in S'$ is contained in $P$, and $B \leq P$, then every $N$-lift $n$ of any $w \in W_{S'}$ lies in $P$. Proof by induction on a reduced expression of $w$ in the simple reflections of $S'$.

theorem SubgroupOverB.standardParabolic_sub {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (P : Subgroup G) (hBP : bp.B ≤ P) (S' : Set B_idx) (hS' : ∀ s ∈ S', bp.bruhatCell (M.toCoxeterSystem.simple s) ⊆ ↑P) : bp.standardParabolic S' ⊆ ↑P

$P_{S'} \subseteq P$ whenever $B \leq P$ and every simple cell $BsB$ for $s \in S'$ is in $P$: combine N_rep_mem_P_of_parabolicW with the $BwB$ factorization.

theorem SubgroupOverB.bn3_gives_element_in_BsB {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (s : B_idx) (n_s : ↥bp.N) (hn_s : bp.π n_s = M.toCoxeterSystem.simple s) : ∃ x ∈ bp.bruhatCell (M.toCoxeterSystem.simple s), ∃ y ∈ bp.bruhatCell (M.toCoxeterSystem.simple s), x⁻¹ * y ∈ bp.bruhatCell (M.toCoxeterSystem.simple s)

Concrete consequence of axiom BN3: for each simple reflection $s$ there exist $x, y \in BsB$ with $x^{-1} y \in BsB$. Uses the BN-pair axiom that some $b_0 \in B$ has $n_s b_0 n_s^{-1} \notin B$, hence the product $(n_s)^{-1} (b_0 n_s^{-1})$ produces an element living in $BsB$ rather than collapsing to $B$.

theorem SubgroupOverB.w_mem_parabolicW_of_cell_sub {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (P : Subgroup G) (hBP : bp.B ≤ P) (S' : Set B_idx) (hS'_def : S' = {s : B_idx | bp.bruhatCell (M.toCoxeterSystem.simple s) ⊆ ↑P}) (w : M.Group) (hw : bp.bruhatCell w ⊆ ↑P) : w ∈ bp.parabolicSubgroupW S'

Reverse direction of the classification of subgroups over $B$. If $BwB \subseteq P$ (with $B \leq P$), then $w \in W_{S'}$ where $S' = \{s : BsB \subseteq P\}$. Proof by strong induction on $\ell(w)$: pick a right descent $s$, observe that $BsB \subseteq P$ via bn3_gives_element_in_BsB and cell_sub_of_mem, then deduce $B(ws)B \subseteq P$ and apply the induction hypothesis to $ws$.

theorem SubgroupOverB.subgroup_over_B_eq_parabolic_from_bnpair {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (P : Subgroup G) : bp.B ≤ P → ∃ (S' : Set B_idx), ↑P = bp.standardParabolic S'

Classification of subgroups containing $B$ (Bourbaki §IV.2.6, Theorem 3). Every subgroup $P \leq G$ with $B \leq P$ equals the standard parabolic $P_{S'}$ where $S' = \{s \in S : BsB \subseteq P\}$. Combines cell_sub_of_mem, w_mem_parabolicW_of_cell_sub, and standardParabolic_sub.