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

Special subsets of $G$: left cosets $g \cdot P_{S'}$ of a proper standard parabolic $P_{S'}$ ($S' \subsetneq S$). These index the chambers and facets of the building.

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

The left coset $g \cdot P_{S'}$ of the standard parabolic indexed by $S'$.

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

The fundamental coset at the identity: the standard parabolic $P_{S'}$ itself.

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

The conjugate parabolic $g P_{S'} g^{-1}$ — the image of $P_{S'}$ under conjugation by $g$.

theorem BNPair.coset_element_in_target {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (g h : G) (S₁ S₂ : Set B_idx) (hcontain : bp.leftCoset g S₁ ⊆ bp.leftCoset h S₂) : ∃ q ∈ bp.standardParabolic S₂, g = h * q

If $g P_{S_1} \subseteq h P_{S_2}$ then $g \in h P_{S_2}$, witnessed by some $q \in P_{S_2}$.

theorem BNPair.coset_inclusion_implies_subgroup_inclusion {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (g h : G) (S₁ S₂ : Set B_idx) (hcontain : bp.leftCoset g S₁ ⊆ bp.leftCoset h S₂) : bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂

Coset inclusion forces inclusion of the underlying parabolics: $g P_{S_1} \subseteq h P_{S_2}$ implies $P_{S_1} \subseteq P_{S_2}$.

theorem BNPair.conjugation_well_defined {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (g h : G) (S' : Set B_idx) (heq : bp.leftCoset g S' = bp.leftCoset h S') : bp.conjugateParabolic g S' = bp.conjugateParabolic h S'

The conjugation map descends to cosets: if $g P_{S'} = h P_{S'}$ then $g P_{S'} g^{-1} = h P_{S'} h^{-1}$.

theorem BNPair.conjugation_mono {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (g h : G) (S₁ S₂ : Set B_idx) (hcontain : bp.leftCoset g S₁ ⊆ bp.leftCoset h S₂) : bp.conjugateParabolic g S₁ ⊆ bp.conjugateParabolic h S₂

Conjugation respects the inclusion order on coset facets: $g P_{S_1} \subseteq h P_{S_2}$ implies $g P_{S_1} g^{-1} \subseteq h P_{S_2} h^{-1}$.

theorem BNPair.labelling_well_defined {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (g h : G) (S₁ S₂ : Set B_idx) (heq : bp.leftCoset g S₁ = bp.leftCoset h S₂) : S₁ = S₂

The type (parabolic-index $S'$) of a coset facet is well-defined: if $g P_{S_1} = h P_{S_2}$ as subsets of $G$, then $S_1 = S_2$. This makes the building's labelling unambiguous.

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

The fundamental apartment expressed as a set of $B$-cosets: $\{nB : n \in N\}$.

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

The $g$-translate $g \cdot \mathcal{A}$ of the fundamental apartment: $\{(gn)B : n \in N\}$.

theorem BNPair.conjugation_equivariant {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (g h : G) (S' : Set B_idx) : bp.conjugateParabolic (g * h) S' = (fun (x : G) => g * x * g⁻¹) '' bp.conjugateParabolic h S'

Equivariance: $(gh) P_{S'} (gh)^{-1} = g \cdot (h P_{S'} h^{-1}) \cdot g^{-1}$.

theorem BNPair.leftCoset_left_action {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (g h : G) (S' : Set B_idx) : (fun (x : G) => g * x) '' bp.leftCoset h S' = bp.leftCoset (g * h) S'

Left multiplication by $g$ on a coset $h P_{S'}$ gives the coset $(gh) P_{S'}$.

theorem BNPair.B_mem_standardParabolic {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (S' : Set B_idx) (b : G) (hb : b ∈ bp.B) : b ∈ bp.standardParabolic S'

$B$ is contained in every standard parabolic $P_{S'}$.

theorem BNPair.leftCoset_right_mul_eq {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (g : G) (S' : Set B_idx) (p : G) (hp : p ∈ bp.standardParabolic S') : bp.leftCoset g S' = bp.leftCoset (g * p) S'

Right multiplication by $p \in P_{S'}$ does not change the coset: $gP_{S'} = (gp) P_{S'}$.

theorem BNPair.bruhat_common_apartment {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (g₁ g₂ : G) : ∃ (g : G), bp.leftCoset g₁ ∅ ∈ bp.translatedApartmentCosets g ∧ bp.leftCoset g₂ ∅ ∈ bp.translatedApartmentCosets g

Building axiom (B1): any two chambers $g_1 B, g_2 B$ lie in a common apartment. Concretely, there exists $g \in G$ such that both $g_1 B$ and $g_2 B$ belong to $g \cdot \mathcal{A}$.

theorem BNPair.conjugator_in_target_of_subset {B_idx : Type u_3} [DecidableEq B_idx] {G : Type u_4} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) (S₁ S₂ : Set B_idx) (g : G) (hsub : (fun (x : G) => g * x * g⁻¹) '' bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂) : g ∈ bp.standardParabolic S₂

If conjugation by $g$ sends $P_{S_1}$ into $P_{S_2}$, then $g$ itself lies in $P_{S_2}$. A self-normalization property of standard parabolics.

theorem BNPair.subgroup_inclusion_of_conj_inclusion {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) (S₁ S₂ : Set B_idx) (g : G) (hsub : (fun (x : G) => g * x * g⁻¹) '' bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂) : bp.standardParabolic S₁ ⊆ bp.standardParabolic S₂

From $g P_{S_1} g^{-1} \subseteq P_{S_2}$ deduce the direct inclusion $P_{S_1} \subseteq P_{S_2}$.

theorem BNPair.conjugation_reflects_order {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) (g h : G) (S₁ S₂ : Set B_idx) (hcontain : bp.conjugateParabolic g S₁ ⊆ bp.conjugateParabolic h S₂) : bp.leftCoset g S₁ ⊆ bp.leftCoset h S₂

Reverse direction of conjugation_mono: inclusion of conjugate parabolics $g P_{S_1} g^{-1} \subseteq h P_{S_2} h^{-1}$ implies inclusion of cosets $g P_{S_1} \subseteq h P_{S_2}$.

theorem BNPair.conjugation_preserves_order {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) (g h : G) (S₁ S₂ : Set B_idx) : bp.leftCoset g S₁ ⊆ bp.leftCoset h S₂ ↔ bp.conjugateParabolic g S₁ ⊆ bp.conjugateParabolic h S₂

Equivalence: coset inclusion $\Leftrightarrow$ conjugate-parabolic inclusion. This is the order-preservation half of the poset isomorphism between cosets and conjugate parabolics.

theorem BNPair.conjugation_order_iff {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) (g h : G) (S₁ S₂ : Set B_idx) : bp.leftCoset g S₁ ⊆ bp.leftCoset h S₂ ↔ bp.conjugateParabolic g S₁ ⊆ bp.conjugateParabolic h S₂

Synonym wrapper around conjugation_preserves_order.

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

Proper parabolics: conjugates $g P_{S'} g^{-1}$ of proper standard parabolics ($S' \subsetneq S$).

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

Concrete representative of the conjugation map sending a coset $gP_{S'}$ to its conjugate parabolic.

theorem BNPair.conjugation_injective_on_cosets {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) (g h : G) (S₁ S₂ : Set B_idx) (heq : bp.conjugateParabolic g S₁ = bp.conjugateParabolic h S₂) : bp.leftCoset g S₁ = bp.leftCoset h S₂

Injectivity at the coset level: equal conjugate parabolics force equal cosets.

theorem BNPair.poset_isomorphism_specialSubsets_properParabolics {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) : (∀ (g h : G) (S₁ S₂ : Set B_idx), bp.leftCoset g S₁ ⊆ bp.leftCoset h S₂ ↔ bp.conjugateParabolic g S₁ ⊆ bp.conjugateParabolic h S₂) ∧ (∀ (g h : G) (S' : Set B_idx), bp.leftCoset g S' = bp.leftCoset h S' → bp.conjugateParabolic g S' = bp.conjugateParabolic h S') ∧ (∀ (g h : G) (S₁ S₂ : Set B_idx), bp.conjugateParabolic g S₁ = bp.conjugateParabolic h S₂ → bp.leftCoset g S₁ = bp.leftCoset h S₂) ∧ (∀ Q ∈ bp.properParabolics, ∃ (g : G) (S' : Set B_idx), S' ≠ Set.univ ∧ Q = bp.conjugateParabolic g S') ∧ ∀ (g h : G) (S' : Set B_idx), bp.conjugateParabolic (g * h) S' = (fun (x : G) => g * x * g⁻¹) '' bp.conjugateParabolic h S'

Bundle theorem: the conjugation map gives a poset isomorphism between the special subsets (left cosets $gP_{S'}$) and proper parabolic subgroups ($gP_{S'}g^{-1}$). Encodes inclusion-iff, well-definedness, injectivity, surjectivity, and equivariance simultaneously.

noncomputable def BNPair.specialSubsetReprG {B_idx : Type u_1} {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (X : ↑bp.specialSubsets) : G

Choose a group-element representative $g$ such that $X = g P_{S'}$ for a special subset $X$.

noncomputable def BNPair.specialSubsetReprS {B_idx : Type u_1} {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (X : ↑bp.specialSubsets) : Set B_idx

Choose a parabolic-type representative $S'$ such that $X = g P_{S'}$ for a special subset $X$.

theorem BNPair.specialSubsetRepr_prop {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (X : ↑bp.specialSubsets) : bp.specialSubsetReprS X ≠ Set.univ ∧ ↑X = bp.leftCoset (bp.specialSubsetReprG X) (bp.specialSubsetReprS X)

Defining property of the chosen representatives: $S' \neq S$ and $X$ equals $g P_{S'}$.

theorem BNPair.specialSubsetRepr_ne_univ {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (X : ↑bp.specialSubsets) : bp.specialSubsetReprS X ≠ Set.univ

First conjunct of specialSubsetRepr_prop: the chosen $S'$ is a proper subset.

theorem BNPair.specialSubsetRepr_eq {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (X : ↑bp.specialSubsets) : ↑X = bp.leftCoset (bp.specialSubsetReprG X) (bp.specialSubsetReprS X)

Second conjunct: $X$ equals the coset $g P_{S'}$ formed from the chosen representatives.

noncomputable def BNPair.properParabolicReprG {B_idx : Type u_1} {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (Q : ↑bp.properParabolics) : G

Choose a conjugator $g$ such that $Q = g P_{S'} g^{-1}$ for a proper parabolic $Q$.

noncomputable def BNPair.properParabolicReprS {B_idx : Type u_1} {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (Q : ↑bp.properParabolics) : Set B_idx

Choose the parabolic type $S'$ such that $Q = g P_{S'} g^{-1}$ for a proper parabolic $Q$.

theorem BNPair.properParabolicRepr_prop {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (Q : ↑bp.properParabolics) : bp.properParabolicReprS Q ≠ Set.univ ∧ ↑Q = bp.conjugateParabolic (bp.properParabolicReprG Q) (bp.properParabolicReprS Q)

Defining property of the chosen representatives: $S' \neq S$ and $Q$ equals the conjugate parabolic.

theorem BNPair.properParabolicRepr_ne_univ {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (Q : ↑bp.properParabolics) : bp.properParabolicReprS Q ≠ Set.univ

The chosen $S'$ is a proper subset.

theorem BNPair.properParabolicRepr_eq {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (Q : ↑bp.properParabolics) : ↑Q = bp.conjugateParabolic (bp.properParabolicReprG Q) (bp.properParabolicReprS Q)

$Q$ equals the conjugate parabolic $g P_{S'} g^{-1}$ formed from the chosen representatives.

noncomputable def BNPair.conjugationForward {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (X : ↑bp.specialSubsets) : ↑bp.properParabolics

Forward map of the poset isomorphism: a special subset $X = g P_{S'}$ is sent to the proper parabolic $g P_{S'} g^{-1}$.

noncomputable def BNPair.conjugationBackward {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (Q : ↑bp.properParabolics) : ↑bp.specialSubsets

Inverse map of the poset isomorphism: a proper parabolic $Q = g P_{S'} g^{-1}$ is sent back to the coset $g P_{S'}$.

noncomputable def BNPair.poset_orderIso_specialSubsets_properParabolics {B_idx : Type u_1} [DecidableEq B_idx] {G : Type u_2} [Group G] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) : ↑bp.specialSubsets ≃o ↑bp.properParabolics

Order isomorphism $\text{specialSubsets} \;\simeq_o\; \text{properParabolics}$ realized by conjugation. The two maps are mutual inverses, and inclusion of cosets corresponds to inclusion of conjugate parabolics.