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

A BN-pair (Tits system) on a group $G$ relative to a Coxeter matrix $M$: data of subgroups $B, N, T = B \cap N$ together with a surjection $\pi : N \twoheadrightarrow W = M.\text{Group}$ whose kernel is $T$, such that $B \cup N$ generates $G$. The Coxeter group $W = N/T$ acts as the Weyl group; the cells $BwB$ partition $G$ (Bruhat decomposition).

• B : Subgroup G
• N : Subgroup G
• T : Subgroup G
• T_eq : self.T = self.B ⊓ self.N
• π : ↥self.N →* M.Group
• π_surj : Function.Surjective ⇑self.π
• π_ker (n : ↥self.N) : self.π n = 1 ↔ ↑n ∈ self.T
• generates : Subgroup.closure (↑self.B ∪ ↑self.N) = ⊤

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

The Bruhat cell $C(w) = BwB \subseteq G$ associated to $w \in W$: the set of $g$ of the form $b_1 \, n \, b_2$ with $b_1, b_2 \in B$ and $n \in N$ a lift of $w$.

def setMul {G : Type u_1} [Group G] (X Y : Set G) : Set G

Pointwise product $X \cdot Y = \{xy : x \in X, y \in Y\}$ of two subsets of a group.

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

The set of lifts in $N$ of a simple reflection $s \in S$ along $\pi : N \twoheadrightarrow W$.

structure BNPairAxioms {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : Prop

The defining axioms of a Tits system: multiplication rules $C(w) \cdot C(s) \subseteq C(ws)$ when $\ell(ws) > \ell(w)$, and $C(w) \cdot C(s) \subseteq C(ws) \cup C(w)$ otherwise, together with the non-normality condition $\exists b \in B, nbn^{-1} \notin B$ for each lift $n$ of a simple $s$.

• cell_mul_length_increasing (w : M.Group) (s : B_idx) : M.toCoxeterSystem.length (w * M.toCoxeterSystem.simple s) > M.toCoxeterSystem.length w → setMul (bp.bruhatCell w) (bp.bruhatCell (M.toCoxeterSystem.simple s)) ⊆ bp.bruhatCell (w * M.toCoxeterSystem.simple s)
• cell_mul_length_decreasing (w : M.Group) (s : B_idx) : M.toCoxeterSystem.length (w * M.toCoxeterSystem.simple s) < M.toCoxeterSystem.length w → setMul (bp.bruhatCell w) (bp.bruhatCell (M.toCoxeterSystem.simple s)) ⊆ bp.bruhatCell (w * M.toCoxeterSystem.simple s) ∪ bp.bruhatCell w
• conjugate_not_sub (s : B_idx) (n : ↥bp.N) : bp.π n = M.toCoxeterSystem.simple s → ∃ (b : ↥bp.B), ↑n * ↑b * (↑n)⁻¹ ∉ bp.B