def BNPair.parabolicSubgroupW {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} : BNPair G M → (S' : Set B_idx) → Subgroup M.Group

The parabolic Weyl subgroup $W_{S'} = \langle s : s \in S' \rangle \leq W$ generated by the simple reflections indexed by $S' \subseteq S$.

def BNPair.standardParabolic {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S' : Set B_idx) : Set G

The standard parabolic subgroup $P_{S'} = BW_{S'}B = \bigcup_{w \in W_{S'}} BwB$ in a BN-pair, viewed as a subset of $G$.

def BNPair.IsStandardParabolic {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (P : Subgroup G) : Prop

A subgroup $P \leq G$ is a standard parabolic if $P = P_{S'}$ for some $S' \subseteq S$.

def BNPair.IsParabolic {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (P : Subgroup G) : Prop

A subgroup $P \leq G$ is parabolic if it is a $G$-conjugate of some standard parabolic $P_{S'}$.

structure BNPair.BruhatProperties {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : Prop

The package of derived properties of the Bruhat decomposition needed to prove the parabolic theorems: cells are pairwise disjoint and cover $G$, behave well under inversion and multiplication within a parabolic, and the standard parabolics are self-normalizing and pairwise non-conjugate. These are consequences of the BN-pair axioms, collected here for downstream use.

• cell_disjoint (w w' : M.Group) : (bp.bruhatCell w ∩ bp.bruhatCell w').Nonempty → w = w'
• cell_cover (g : G) : ∃ (w : M.Group), g ∈ bp.bruhatCell w
• cell_inv (w : M.Group) (g : G) : g ∈ bp.bruhatCell w → g⁻¹ ∈ bp.bruhatCell w⁻¹
• cell_mul_in_parabolic (S' : Set B_idx) (w w' : M.Group) : w ∈ bp.parabolicSubgroupW S' → w' ∈ bp.parabolicSubgroupW S' → ∀ (g₁ g₂ : G), g₁ ∈ bp.bruhatCell w → g₂ ∈ bp.bruhatCell w' → ∃ u ∈ ↑(bp.parabolicSubgroupW S'), g₁ * g₂ ∈ bp.bruhatCell u
• parabolicW_injective (S₁ S₂ : Set B_idx) : bp.parabolicSubgroupW S₁ = bp.parabolicSubgroupW S₂ → S₁ = S₂
• subgroup_over_B_eq_parabolic (P : Subgroup G) : bp.B ≤ P → ∃ (S' : Set B_idx), ↑P = bp.standardParabolic S'
• normalizer_in_parabolic (S' : Set B_idx) (g : G) : (∀ (x : G), x ∈ bp.standardParabolic S' ↔ g * x * g⁻¹ ∈ bp.standardParabolic S') → g ∈ bp.standardParabolic S'
• conjugator_in_target (S₁ S₂ : Set B_idx) (g : G) : (fun (x : G) => g * x * g⁻¹) '' bp.standardParabolic S₁ = bp.standardParabolic S₂ → g ∈ bp.standardParabolic S₂
• cell_mul_finite (w w' : M.Group) : ∃ (us : Finset M.Group), setMul (bp.bruhatCell w) (bp.bruhatCell w') ⊆ ⋃ u ∈ us, bp.bruhatCell u

theorem BNPair.exists_mem_bruhatCell {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (w : M.Group) : (bp.bruhatCell w).Nonempty

Every Bruhat cell $BwB$ is nonempty: pick any $N$-lift $n$ of $w$ to witness it.

theorem BNPair.mem_conj_image_self {G : Type u_1} [Group G] (P : Set G) (g : G) (h : g ∈ (fun (x : G) => g * x * g⁻¹) '' P) : g ∈ P

If $g \in gPg^{-1}$ then in fact $g \in P$: cancelling the conjugation gives $p = g$.

theorem BNPair.conj_image_eq {G : Type u_1} [Group G] (P Q : Set G) (g : G) (hgQ : g ∈ Q) (hP_mul : ∀ (x y : G), x ∈ P → y ∈ P → x * y ∈ P) (hP_inv : ∀ x ∈ P, x⁻¹ ∈ P) (hconj : (fun (x : G) => g * x * g⁻¹) '' P = Q) : P = Q

If $P$ is closed under multiplication and inverse, $g \in Q$, and $gPg^{-1} = Q$, then $P = Q$: the conjugator $g$ already lies in $P$, so conjugation by $g$ is an automorphism of $P$.

theorem BNPair.standardParabolicInjective {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (S₁ S₂ : Set B_idx) (h : bp.standardParabolic S₁ = bp.standardParabolic S₂) : S₁ = S₂

Injectivity of the standard parabolics. Distinct subsets $S_1, S_2 \subseteq S$ give distinct parabolics: if $P_{S_1} = P_{S_2}$ then $S_1 = S_2$. Equivalently, the map $S' \mapsto P_{S'}$ from subsets of $S$ to subgroups of $G$ containing $B$ is injective.

theorem BNPair.parabolicsAreSubgroups {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (S' : Set B_idx) : 1 ∈ bp.standardParabolic S' ∧ (∀ (x y : G), x ∈ bp.standardParabolic S' → y ∈ bp.standardParabolic S' → x * y ∈ bp.standardParabolic S') ∧ ∀ x ∈ bp.standardParabolic S', x⁻¹ ∈ bp.standardParabolic S'

Parabolics are subgroups. Each standard parabolic $P_{S'} = BW_{S'}B$ contains the identity and is closed under multiplication and inverses, so it is a subgroup of $G$.

def BNPair.weylGroupOfParabolic {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (P : Subgroup G) : bp.B ≤ P → Set M.Group

The Weyl-side description of a subgroup $P$ containing $B$: the set $\{w \in W : BwB \subseteq P\}$. For $P = P_{S'}$ this recovers $W_{S'}$.