def GeneralizedBNPair.Blifted {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) : Subgroup Gt

The Borel subgroup $B \leq G$ pushed forward to $\tilde G$ along the inclusion $G \hookrightarrow \tilde G$.

def GeneralizedBNPair.Nlifted {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) : Subgroup Gt

The subgroup $N \leq G$ pushed forward to $\tilde G$.

def GeneralizedBNPair.Tlifted {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) : Subgroup Gt

The torus $T = B \cap N \leq G$ pushed forward to $\tilde G$.

def GeneralizedBNPair.TtInterG {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) : Subgroup Gt

The intersection $\tilde T \cap G$ inside $\tilde G$; by the axioms this coincides with the lifted $T$.

def GeneralizedBNPair.twistSubgroup {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) : Subgroup ↥gbp.Tt

The subgroup $\tilde T \cap G$ pulled back into $\tilde T$, viewed as a subgroup of $\tilde T$. Quotienting by this yields the twist group.

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

The twist group $\tilde T / (\tilde T \cap G)$, finite by axiom, which measures the non-type-preserving part of $\tilde G$.

theorem GeneralizedBNPair.trivial_action_in_G {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) (t : Gt) (ht : t ∈ gbp.Tt) (htrivial : ∀ (s : B_idx) (n : ↥gbp.strictBNPair.N), gbp.strictBNPair.π n = M.toCoxeterSystem.simple s → ∃ (n' : ↥gbp.strictBNPair.N), gbp.strictBNPair.π n' = M.toCoxeterSystem.simple s ∧ ↑↑n' = t * ↑↑n * t⁻¹) : t ∈ gbp.G

An element $t \in \tilde T$ that acts trivially on types of the base apartment lies in $G$. Specialization of the building uniqueness lemma to $\tilde T \leq \tilde B$.

theorem GeneralizedBNPair.Tt_perm_injective {B_idx : Type u_3} [Fintype B_idx] [DecidableEq B_idx] {Gt : Type u_4} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (t₁ t₂ : Gt) (ht₁ : t₁ ∈ gbp.Tt) (ht₂ : t₂ ∈ gbp.Tt) (hsame : ∀ (s : B_idx) (n : ↥gbp.strictBNPair.N), gbp.strictBNPair.π n = M.toCoxeterSystem.simple s → ∃ (n₁' : ↥gbp.strictBNPair.N) (n₂' : ↥gbp.strictBNPair.N), gbp.strictBNPair.π n₁' = gbp.strictBNPair.π n₂' ∧ ↑↑n₁' = t₁ * ↑↑n * t₁⁻¹ ∧ ↑↑n₂' = t₂ * ↑↑n * t₂⁻¹) : t₁⁻¹ * t₂ ∈ gbp.G

Injectivity of the type-permutation action of $\tilde T$. If two elements $t_1, t_2 \in \tilde T$ induce the same permutation $\sigma \in \mathrm{Sym}(S)$ on the set of simple reflections (so their conjugation actions on $N$-lifts of simple reflections agree at the level of $\pi$), then $t_1^{-1} t_2 \in G$. Equivalently, the homomorphism $\tilde T / (\tilde T \cap G) \to \mathrm{Sym}(S)$ given by the type permutation is injective.

def GeneralizedBNPair.bruhatCellGt {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (σ : Gt) (w : M.Group) : Set Gt

The "twisted" Bruhat cell $\sigma \cdot B \cdot w \cdot B \subseteq \tilde G$ for $\sigma \in \tilde T$ and $w \in W$: elements that can be written as $\sigma \cdot b_1 \cdot n \cdot b_2$ with $b_i \in B$ (lifted) and $n$ an $N$-lift of $w$.

def GeneralizedBNPair.sigmaB {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (σ : Gt) : Set Gt

The left coset $\sigma B = \{\sigma b : b \in B\} \subseteq \tilde G$.

def GeneralizedBNPair.Bsigma {B_idx : Type u_1} {Gt : Type u_2} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (σ : Gt) : Set Gt

The right coset $B\sigma = \{b\sigma : b \in B\} \subseteq \tilde G$.

theorem GeneralizedBNPair.Tlifted_le_Blifted {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.Tlifted ≤ gbp.Blifted

The lifted torus is contained in the lifted Borel: $T \leq B$ pushed forward.

theorem GeneralizedBNPair.Tlifted_le_Nlifted {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.Tlifted ≤ gbp.Nlifted

The lifted torus is contained in the lifted $N$: $T \leq N$ pushed forward.

theorem GeneralizedBNPair.T_le_Tt {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.Tlifted ≤ gbp.Tt

The lifted torus $T$ is contained in the enlarged torus $\tilde T$, since $T \leq B \leq \tilde B$ and $T \leq N \leq \tilde N$.