theorem PropositionParabolics.B_le_closure_bruhatCell {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (w : M.Group) : bp.B ≤ Subgroup.closure (bp.bruhatCell w)

$B \leq \langle BwB \rangle$: write each $b \in B$ as $n^{-1}(nb)$ with $n, nb \in BwB$.

theorem PropositionParabolics.bruhatCell_generators_in_subgroup {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (Q : Subgroup G) (w : M.Group) (hBwB : bp.bruhatCell w ⊆ ↑Q) (hBQ : bp.B ≤ Q) : w ∈ bp.parabolicSubgroupW {s : B_idx | bp.bruhatCell (M.toCoxeterSystem.simple s) ⊆ ↑Q}

If $BwB \subseteq Q$ and $B \leq Q$, then $w$ belongs to the parabolic Weyl subgroup $W_{S_Q}$, where $S_Q = \{s \in S : BsB \subseteq Q\}$.

theorem PropositionParabolics.generators_in_closure_bruhatCell {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (w : M.Group) : w ∈ bp.parabolicSubgroupW {s : B_idx | bp.bruhatCell (M.toCoxeterSystem.simple s) ⊆ ↑(Subgroup.closure (bp.bruhatCell w))}

Applied to $Q = \langle BwB \rangle$: the element $w$ lies in the parabolic Weyl subgroup generated by those simple reflections whose Bruhat cell already lies in $\langle BwB \rangle$.

def PropositionParabolics.conjB {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (n : ↥bp.N) : Set G

The conjugate Borel $n^{-1} B n = \{n^{-1} b n : b \in B\}$.

theorem PropositionParabolics.bruhatCell_sub_closure_B_conjB {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (w : M.Group) (n : ↥bp.N) (hn : bp.π n = w) : bp.bruhatCell w ⊆ ↑(Subgroup.closure (↑bp.B ∪ conjB bp n))

$BwB \subseteq \langle B \cup n^{-1}Bn \rangle$ for any $N$-lift $n$ of $w$. Uses the key conjugation lemma N_lift_mem_subgroup_of_conj applied to $n^{-1}$.

theorem PropositionParabolics.closure_B_conjB_sub_closure_bruhatCell {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (w : M.Group) (n : ↥bp.N) (hn : bp.π n = w) : Subgroup.closure (↑bp.B ∪ conjB bp n) ≤ Subgroup.closure (bp.bruhatCell w)

$\langle B \cup n^{-1}Bn \rangle \leq \langle BwB \rangle$: both generating sets sit inside $\langle BwB \rangle$ since $n \in BwB$ and $B \leq \langle BwB \rangle$.

theorem PropositionParabolics.closure_bruhatCell_eq_closure_B_conjB {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (w : M.Group) (n : ↥bp.N) (hn : bp.π n = w) : Subgroup.closure (bp.bruhatCell w) = Subgroup.closure (↑bp.B ∪ conjB bp n)

$\langle BwB \rangle = \langle B \cup n^{-1}Bn \rangle$ for any $N$-lift $n$ of $w$. Combines the two inclusions above.

theorem PropositionParabolics.N_lift_in_closure_bruhatCell {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (w : M.Group) (s : B_idx) (hs : bp.bruhatCell (M.toCoxeterSystem.simple s) ⊆ ↑(Subgroup.closure (bp.bruhatCell w))) (n : ↥bp.N) (hn : bp.π n = M.toCoxeterSystem.simple s) : ↑n ∈ ↑(Subgroup.closure (bp.bruhatCell w))

An $N$-lift of a simple reflection $s$ already lies in $\langle BwB \rangle$ whenever the simple cell $BsB$ does.

theorem PropositionParabolics.proposition_parabolic_subgroup_of_cell {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (w : M.Group) (n : ↥bp.N) (hn : bp.π n = w) : w ∈ bp.parabolicSubgroupW {s : B_idx | bp.bruhatCell (M.toCoxeterSystem.simple s) ⊆ ↑(Subgroup.closure (bp.bruhatCell w))} ∧ Subgroup.closure (bp.bruhatCell w) = Subgroup.closure (↑bp.B ∪ conjB bp n)

Combined "Proposition" on the parabolic subgroup generated by a Bruhat cell. For any $w \in W$ and any $N$-lift $n$ of $w$, the following both hold: (i) $w$ lies in the parabolic Weyl subgroup generated by $\{s : BsB \subseteq \langle BwB \rangle\}$; (ii) $\langle BwB \rangle = \langle B \cup n^{-1}Bn \rangle$. This is the conjunction of generators_in_closure_bruhatCell and closure_bruhatCell_eq_closure_B_conjB.