theorem GeneralizedBNPair.Tt_le_Bt {B_idx : Type u_1} [Fintype B_idx] [DecidableEq B_idx] {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) : gbp.Tt ≤ gbp.Bt

The enlarged torus is contained in the enlarged Borel: $\tilde T = \tilde B \cap \tilde N \leq \tilde B$.

theorem GeneralizedBNPair.Bt_decomp_from_Gt {B_idx : Type u_1} [Fintype B_idx] [DecidableEq B_idx] {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (x : Gt) : x ∈ gbp.Bt → ∃ (t : Gt) (_ : t ∈ gbp.Tt) (g : Gt) (_ : g ∈ gbp.G) (_ : g ∈ gbp.Bt), x = t * g

Decomposition of $\tilde B$. Every $x \in \tilde B$ factors as $x = t \cdot g$ with $t \in \tilde T$ and $g \in G \cap \tilde B$. Specializes the $\tilde G$-decomposition to $\tilde B$.

def GeneralizedBNPair.ActsTriviallyOnTypes {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (t : Gt) : Prop

An element $t \in \tilde G$ acts trivially on types of the standard apartment: for every simple reflection $s$ and every $N$-lift $n$ of $s$, the conjugate $t n t^{-1}$ is again an $N$-lift of the same simple reflection $s$.

def GeneralizedBNPair.PreservesTypesOnBaseChbr {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (g : Gt) : Prop

$g \in \tilde G$ preserves types on the base chamber: synonym for ActsTriviallyOnTypes g, packaged to clarify the geometric meaning.

def GeneralizedBNPair.PreservesTypesOnChamber {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (g h : Gt) : Prop

$g \in \tilde G$ preserves types on the chamber $h \cdot C_0$: this means the conjugate $h^{-1} g h$ preserves types on the base chamber $C_0$.

theorem GeneralizedBNPair.TypePreservingImpliesGlobal {B_idx : Type u_1} [Fintype B_idx] [DecidableEq B_idx] {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (g h : Gt) (hpres : gbp.PreservesTypesOnChamber g h) : g ∈ gbp.G

Type-preservation is a global property. If $g \in \tilde G$ preserves types on any single chamber $h \cdot C_0$, then $g \in G$ (the type-preserving subgroup). The converse "everything in $G$ preserves types everywhere" is built into the generalized BN-pair definition; this theorem is the rigidity half: local type-preservation already forces global membership.

theorem GeneralizedBNPair.LocalTypePreservingImpliesGlobal {B_idx : Type u_1} [Fintype B_idx] [DecidableEq B_idx] {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (g h : Gt) (hpres : gbp.PreservesTypesOnChamber g h) : g ∈ gbp.G

Alias for TypePreservingImpliesGlobal emphasizing the "local-to-global" flavor: preserving types at one chamber implies $g$ belongs to the type-preserving subgroup $G$.