theorem NormalizerParabolic.B_sub_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'

$B \subseteq P_{S'}$ via the trivial cell $B = B \cdot 1 \cdot B$ in $P_{S'} = \bigcup_{w \in W_{S'}} BwB$.

theorem NormalizerParabolic.standardParabolic_mul {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) {x y : G} (hx : x ∈ bp.standardParabolic S') (hy : y ∈ bp.standardParabolic S') : x * y ∈ bp.standardParabolic S'

Standard parabolics are closed under multiplication: $P_{S'} \cdot P_{S'} \subseteq P_{S'}$. Follows from CellMulParabolic.cell_mul_in_parabolic_from_bnpair.

theorem NormalizerParabolic.standardParabolic_inv {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S' : Set B_idx) {x : G} (hx : x ∈ bp.standardParabolic S') : x⁻¹ ∈ bp.standardParabolic S'

Standard parabolics are closed under inversion: if $x \in BwB \subseteq P_{S'}$ then $x^{-1} \in Bw^{-1}B$, and $w^{-1} \in W_{S'}$ still.

theorem NormalizerParabolic.N_lift_mem_subgroup_of_conj {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) (hBQ : bp.B ≤ Q) (w : M.Group) (n : ↥bp.N) (hn : bp.π n = w) (hn_conj : ∀ b ∈ bp.B, ↑n * b * (↑n)⁻¹ ∈ ↑Q) : ↑n ∈ ↑Q

Key technical lemma for self-normalization. Let $Q$ be a subgroup containing $B$, and let $n$ be an $N$-lift of $w \in W$ such that $nBn^{-1} \subseteq Q$. Then $n \in Q$. Proved by induction on the length of $w$, using a "BN3"-style trick: descend by a simple reflection and use that conjugates of the cell of a simple reflection produce $B$ or $BsB$ elements that already lie in $Q$.

theorem NormalizerParabolic.bruhatCell_sub_of_conj {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) (hBQ : bp.B ≤ Q) (w : M.Group) (n : ↥bp.N) (hn : bp.π n = w) (hn_conj : ∀ b ∈ bp.B, ↑n * b * (↑n)⁻¹ ∈ ↑Q) : bp.bruhatCell w ⊆ ↑Q

Strengthening of N_lift_mem_subgroup_of_conj: under the same hypotheses, the entire Bruhat cell $BwB$ is contained in $Q$, not just the chosen lift $n$.

theorem NormalizerParabolic.normalizer_in_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) (S' : Set B_idx) (g : G) : (∀ (x : G), x ∈ bp.standardParabolic S' ↔ g * x * g⁻¹ ∈ bp.standardParabolic S') → g ∈ bp.standardParabolic S'

Standard parabolics are self-normalizing. If $g \in G$ satisfies $gP_{S'}g^{-1} = P_{S'}$ in the sense that conjugation by $g$ preserves membership in $P_{S'}$, then $g \in P_{S'}$. Equivalently $N_G(P_{S'}) = P_{S'}$. Proof: write $g = b_1 n b_2$ by Bruhat, deduce that $n$ normalizes $B$ modulo $P_{S'}$, and apply bruhatCell_sub_of_conj to conclude that the entire cell $BwB$ (and hence $g$) lies in $P_{S'}$.

theorem NormalizerParabolic.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)

The Borel $B$ is contained in the subgroup generated by any Bruhat cell $BwB$: write $b = n^{-1} \cdot (nb)$ where $n$ and $nb$ both lie in the cell.

theorem NormalizerParabolic.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$ for a subgroup $Q$ containing $B$, then $w \in W_{S_Q}$ where $S_Q = \{s : BsB \subseteq Q\}$. Specialization of w_mem_parabolicW_of_cell_sub to the canonical $S' = S_Q$.

theorem NormalizerParabolic.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))}

Specializing bruhatCell_generators_in_subgroup to $Q = \langle BwB \rangle$: the element $w$ lies in the parabolic Weyl subgroup generated by those simple reflections $s$ whose cell $BsB$ is already inside $\langle BwB \rangle$.

theorem NormalizerParabolic.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$ lies in $\langle BwB \rangle$ whenever the simple cell $BsB$ does. Direct from lift_mem_bruhatCell.

def NormalizerParabolic.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\}$ as a subset of $G$, used to present $\langle BwB \rangle$ as $\langle B \cup n^{-1}Bn \rangle$.

theorem NormalizerParabolic.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))

One inclusion of the equality $\langle BwB \rangle = \langle B \cup n^{-1}Bn \rangle$: every element of $BwB$ already lies in $\langle B \cup n^{-1}Bn \rangle$. Uses N_lift_mem_subgroup_of_conj applied to $n^{-1}$.

theorem NormalizerParabolic.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)

The other inclusion: $\langle B \cup n^{-1}Bn \rangle \leq \langle BwB \rangle$. Both generating sets lie in $\langle BwB \rangle$ since $n \in BwB$ and $B \subseteq \langle BwB \rangle$.

theorem NormalizerParabolic.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)

Generating description of $\langle BwB \rangle$. The subgroup of $G$ generated by the Bruhat cell $BwB$ coincides with the subgroup generated by $B \cup n^{-1}Bn$, for any choice of $N$-lift $n$ of $w$. Combines bruhatCell_sub_closure_B_conjB and closure_B_conjB_sub_closure_bruhatCell.