def BNPair.doubleCoset {G : Type u_1} [Group G] (P Q : Set G) (g : G) : Set G

The $(P, Q)$-double coset of $g$ in $G$: the set $PgQ = \{pgq : p \in P,\ q \in Q\}$.

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

The $(P_{S_1}, P_{S_2})$-double coset of $g$: $P_{S_1} \cdot g \cdot P_{S_2}$.

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

The Weyl-side $(W_{S_1}, W_{S_2})$-double coset of $w \in W$: $W_{S_1} \cdot w \cdot W_{S_2} \subseteq W$.

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

The set of all $(P_{S_1}, P_{S_2})$-double cosets in $G$, i.e. $P_{S_1} \backslash G / P_{S_2}$ as a collection of subsets of $G$.

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

The set of all $(W_{S_1}, W_{S_2})$-double cosets in $W$, i.e. $W_{S_1} \backslash W / W_{S_2}$.

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

The image of a Weyl double coset under the assignment $w \mapsto P_{S_1} \cdot n \cdot P_{S_2}$ for any $N$-lift $n$ of $w$. Realizes the bijection $W_{S_1} \backslash W / W_{S_2} \to P_{S_1} \backslash G / P_{S_2}$.