structure GeneralizedBNPair {B_idx : Type u_1} (Gt : Type u_2) [Group Gt] (M : CoxeterMatrix B_idx) : Type (max u_1 u_2)

A generalized BN-pair (in the sense of Bourbaki §IV.2.6, Section 5.5): an ambient group $\tilde G$ with a normal finite-index subgroup $G$ carrying a strict BN-pair $(B, N, T, W)$, together with enlarged subgroups $\tilde B \supseteq B$, $\tilde N \supseteq N$ and $\tilde T = \tilde B \cap \tilde N$ satisfying the analogues of the Bruhat decomposition $\tilde G = \tilde T \cdot \bigsqcup_w BwB$, plus compatibility conditions making $\tilde T$ normalize $B$, $N$, and act on the set $S$ of simple reflections by permutations, with finite "twist group" $\tilde T / (\tilde T \cap G)$.

• G : Subgroup Gt
• strictBNPair : BNPair (↥self.G) M
• Bt : Subgroup Gt
• Nt : Subgroup Gt
• Tt : Subgroup Gt
• Tt_eq : self.Tt = self.Bt ⊓ self.Nt
• B_le_Bt : Subgroup.map self.G.subtype self.strictBNPair.B ≤ self.Bt
• N_le_Nt : Subgroup.map self.G.subtype self.strictBNPair.N ≤ self.Nt
• G_normal : self.G.Normal
• finiteIndex : self.G.FiniteIndex
• Tt_normalizes_B (t : Gt) : t ∈ self.Tt → ∀ b ∈ Subgroup.map self.G.subtype self.strictBNPair.B, t * b * t⁻¹ ∈ Subgroup.map self.G.subtype self.strictBNPair.B
• Tt_normalizes_N (t : Gt) : t ∈ self.Tt → ∀ n ∈ Subgroup.map self.G.subtype self.strictBNPair.N, t * n * t⁻¹ ∈ Subgroup.map self.G.subtype self.strictBNPair.N
• TtInterG_eq : self.Tt ⊓ self.G = Subgroup.map self.G.subtype self.strictBNPair.T
• Nt_decomp (x : Gt) : x ∈ self.Nt → ∃ (t : Gt) (_ : t ∈ self.Tt) (n : Gt) (_ : n ∈ Subgroup.map self.G.subtype self.strictBNPair.N), x = t * n
• Tt_stabilizes_S (t : Gt) : t ∈ self.Tt → ∃ (σ : Equiv.Perm B_idx), ∀ (s : B_idx) (n : ↥self.strictBNPair.N), self.strictBNPair.π n = M.toCoxeterSystem.simple s → ∃ (n' : ↥self.strictBNPair.N), self.strictBNPair.π n' = M.toCoxeterSystem.simple (σ s) ∧ ↑↑n' = t * ↑↑n * t⁻¹
• Tt_inter_Nlifted_eq : self.Tt ⊓ Subgroup.map self.G.subtype self.strictBNPair.N = Subgroup.map self.G.subtype self.strictBNPair.T
• generalized_bruhat (g : Gt) : ∃ (σ : Gt) (_ : σ ∈ self.Tt) (w : M.Group) (b₁ : Gt) (_ : b₁ ∈ Subgroup.map self.G.subtype self.strictBNPair.B) (n : Gt) (_ : n ∈ Subgroup.map self.G.subtype self.strictBNPair.N) (b₂ : Gt) (_ : b₂ ∈ Subgroup.map self.G.subtype self.strictBNPair.B), (∃ (n' : ↥self.strictBNPair.N), self.strictBNPair.π n' = w ∧ ↑↑n' = n) ∧ g = σ * b₁ * n * b₂
• generalized_bruhat_disjoint (σ₁ σ₂ : Gt) : σ₁ ∈ self.Tt → σ₂ ∈ self.Tt → ∀ (w₁ w₂ : M.Group), (∃ (g : Gt), (∃ (b₁ : Gt) (_ : b₁ ∈ Subgroup.map self.G.subtype self.strictBNPair.B) (n : Gt) (_ : n ∈ Subgroup.map self.G.subtype self.strictBNPair.N) (b₂ : Gt) (_ : b₂ ∈ Subgroup.map self.G.subtype self.strictBNPair.B), (∃ (n' : ↥self.strictBNPair.N), self.strictBNPair.π n' = w₁ ∧ ↑↑n' = n) ∧ g = σ₁ * b₁ * n * b₂) ∧ ∃ (b₁ : Gt) (_ : b₁ ∈ Subgroup.map self.G.subtype self.strictBNPair.B) (n : Gt) (_ : n ∈ Subgroup.map self.G.subtype self.strictBNPair.N) (b₂ : Gt) (_ : b₂ ∈ Subgroup.map self.G.subtype self.strictBNPair.B), (∃ (n' : ↥self.strictBNPair.N), self.strictBNPair.π n' = w₂ ∧ ↑↑n' = n) ∧ g = σ₂ * b₁ * n * b₂) → (∃ (t : Gt) (_ : t ∈ Subgroup.map self.G.subtype self.strictBNPair.T), σ₁ = σ₂ * t) ∧ w₁ = w₂
• coset_mul_rule (σ : Gt) : σ ∈ self.Tt → ∀ (w : M.Group) (g : Gt), (∃ (b₁ : Gt) (_ : b₁ ∈ Subgroup.map self.G.subtype self.strictBNPair.B) (n : Gt) (_ : n ∈ Subgroup.map self.G.subtype self.strictBNPair.N) (b₂ : Gt) (_ : b₂ ∈ Subgroup.map self.G.subtype self.strictBNPair.B), (∃ (n' : ↥self.strictBNPair.N), self.strictBNPair.π n' = w ∧ ↑↑n' = n) ∧ g = σ * b₁ * n * b₂) ↔ ∃ (b₁ : Gt) (_ : b₁ ∈ Subgroup.map self.G.subtype self.strictBNPair.B) (n : Gt) (_ : n ∈ Subgroup.map self.G.subtype self.strictBNPair.N) (b₂ : Gt) (_ : b₂ ∈ Subgroup.map self.G.subtype self.strictBNPair.B), (∃ (n' : ↥self.strictBNPair.N), self.strictBNPair.π n' = w ∧ ↑↑n' = n) ∧ g = b₁ * σ * n * b₂
• coset_conj_rule (σ : Gt) : σ ∈ self.Tt → ∀ (w : M.Group) (g : Gt), (∃ (b₁ : Gt) (_ : b₁ ∈ Subgroup.map self.G.subtype self.strictBNPair.B) (n : Gt) (_ : n ∈ Subgroup.map self.G.subtype self.strictBNPair.N) (b₂ : Gt) (_ : b₂ ∈ Subgroup.map self.G.subtype self.strictBNPair.B), (∃ (n' : ↥self.strictBNPair.N), self.strictBNPair.π n' = w ∧ ↑↑n' = n) ∧ g = σ * b₁ * n * b₂) ↔ ∃ (b₁ : Gt) (_ : b₁ ∈ Subgroup.map self.G.subtype self.strictBNPair.B) (n : Gt) (_ : n ∈ Subgroup.map self.G.subtype self.strictBNPair.N) (b₂ : Gt) (_ : b₂ ∈ Subgroup.map self.G.subtype self.strictBNPair.B), (∃ (n' : ↥self.strictBNPair.N) (nw : ↥self.strictBNPair.N), self.strictBNPair.π nw = w ∧ ↑↑n' = n ∧ ↑↑n' = σ * ↑↑nw * σ⁻¹) ∧ g = b₁ * n * b₂ * σ
• twist_group_finite : Finite (↥self.Tt ⧸ (self.Tt ⊓ self.G).subgroupOf self.Tt)

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

Decomposition of $\tilde G$. Every $x \in \tilde G$ factors as $x = t \cdot g$ with $t \in \tilde T$ and $g \in G$, reflecting the coset structure $\tilde G / G \cong \tilde T / (\tilde T \cap G)$.

theorem GeneralizedBNPair.building_uniqueness_lemma {B_idx : Type u_2} [Fintype B_idx] [DecidableEq B_idx] {Gt : Type u_3} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (t : Gt) : t ∈ gbp.Bt → (∀ (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

Building uniqueness lemma. An element $t \in \tilde B$ that fixes every chamber of the standard apartment (i.e. acts trivially on the set $S$ of types of simple reflections by conjugating $N$-lifts to $N$-lifts of the same simple reflection) must already lie in $G$.

theorem GeneralizedBNPair.strong_transitivity_for_types {B_idx : Type u_2} [Fintype B_idx] [DecidableEq B_idx] {Gt : Type u_3} [Group Gt] {M : CoxeterMatrix B_idx} (gbp : GeneralizedBNPair Gt M) (g : Gt) : (∀ (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' = g * ↑↑n * g⁻¹) → ∃ (h' : Gt) (_ : h' ∈ gbp.G) (_ : h' * g ∈ gbp.Bt), ∀ (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' = h' * g * ↑↑n * (h' * g)⁻¹

Strong transitivity for type-preserving elements. Any $g \in \tilde G$ that already acts trivially on types can be moved by left-multiplication with some $h' \in G$ into $\tilde B$, while remaining type-preserving. This is the "transitivity on chambers" half of strong transitivity, restricted to type-preserving elements.