noncomputable def BNPair.standardParabolicInjective' {G : Type u_1} [Group G] {B_idx : Type u_2} [DecidableEq B_idx] [Fintype B_idx] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S₁ S₂ : Set B_idx) (h : bp.standardParabolic S₁ = bp.standardParabolic S₂) : S₁ = S₂

Axiomless form of standardParabolicInjective: distinct subsets $S_1, S_2 \subseteq S$ yield distinct standard parabolics $P_{S_1} \ne P_{S_2}$, derived directly from the BN-pair axioms (via BruhatProperties.fromAxioms).

noncomputable def BNPair.parabolicsAreSubgroups' {G : Type u_1} [Group G] {B_idx : Type u_2} [DecidableEq B_idx] [Fintype B_idx] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (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'

Axiomless form of parabolicsAreSubgroups: each $P_{S'}$ contains $1$ and is closed under multiplication and inverses, derived from the BN-pair axioms alone.

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

Every Borel subgroup $B$ is contained in any standard parabolic $P_{S'}$: since $1 \in W_{S'}$, the cell $B \cdot 1 \cdot B = B$ sits inside $P_{S'} = BW_{S'}B$.

noncomputable def BNPair.subgroupsOverB_eq_parabolic' {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), ↑P = bp.standardParabolic S'

Classification of subgroups containing $B$. Every subgroup $P \leq G$ with $B \leq P$ equals some standard parabolic $P_{S'}$, where $S' = \{s \in S : BsB \subseteq P\}$. Derived directly from the BN-pair axioms.

noncomputable def BNPair.parabolicSelfNormalizing' {G : Type u_1} [Group G] {B_idx : Type u_2} [DecidableEq B_idx] [Fintype B_idx] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S' : Set B_idx) (g : G) (hnorm : ∀ (x : G), x ∈ bp.standardParabolic S' ↔ g * x * g⁻¹ ∈ bp.standardParabolic S') : g ∈ bp.standardParabolic S'

Standard parabolics are self-normalizing (axiomless form). If $g \in G$ normalizes $P_{S'}$ in the sense $gP_{S'}g^{-1} = P_{S'}$, then $g \in P_{S'}$. That is, $N_G(P_{S'}) = P_{S'}$.

noncomputable def BNPair.parabolicsNotConjugate' {G : Type u_1} [Group G] {B_idx : Type u_2} [DecidableEq B_idx] [Fintype B_idx] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S₁ S₂ : Set B_idx) (g : G) (hconj : (fun (x : G) => g * x * g⁻¹) '' bp.standardParabolic S₁ = bp.standardParabolic S₂) : S₁ = S₂

No two distinct standard parabolics are conjugate (axiomless form). If $gP_{S_1}g^{-1} = P_{S_2}$ for some $g \in G$, then $S_1 = S_2$. Equivalently, distinct subsets $S_1 \ne S_2$ of the simple roots give parabolics that are not even conjugate in $G$.

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

Convenience alias: $B \subseteq P_{S'}$ for every $S' \subseteq S$.

noncomputable def BNPair.subgroupsOverB_eq_parabolic {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), ↑P = bp.standardParabolic S'

Convenience alias for subgroupsOverB_eq_parabolic': every subgroup containing $B$ is a standard parabolic.

noncomputable def BNPair.parabolicSelfNormalizing {G : Type u_1} [Group G] {B_idx : Type u_2} [DecidableEq B_idx] [Fintype B_idx] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S' : Set B_idx) (g : G) (hnorm : ∀ (x : G), x ∈ bp.standardParabolic S' ↔ g * x * g⁻¹ ∈ bp.standardParabolic S') : g ∈ bp.standardParabolic S'

Convenience alias: standard parabolics are self-normalizing, $N_G(P_{S'}) = P_{S'}$.

noncomputable def BNPair.parabolicsNotConjugate {G : Type u_1} [Group G] {B_idx : Type u_2} [DecidableEq B_idx] [Fintype B_idx] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (S₁ S₂ : Set B_idx) (g : G) (hconj : (fun (x : G) => g * x * g⁻¹) '' bp.standardParabolic S₁ = bp.standardParabolic S₂) : S₁ = S₂

Convenience alias: distinct standard parabolics are not $G$-conjugate.