def BNPair.apartmentActionFun {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (n : ↥bp.N) (w : M.Group) : M.Group

The action of $N$ on the standard apartment $W$ by left translation: $n \cdot w = \pi(n) \cdot w$.

theorem BNPair.T_acts_trivially_on_apartment {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (n : ↥bp.N) (hn : ↑n ∈ bp.T) (w : M.Group) : bp.apartmentActionFun n w = w

Elements of $T = B \cap N$ act trivially on the apartment $W$: $\pi(t) = 1$ for $t \in T$, hence $t \cdot w = w$ for every $w \in W$.

theorem BNPair.T_subgroupOf_eq_ker {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : bp.T.subgroupOf bp.N = bp.π.ker

T-kernel lemma (§5.2): the torus $T$, viewed as a subgroup of $N$, coincides with the kernel of the projection $\pi : N \to W$. Equivalently $T = \pi^{-1}(1)$.

instance BNPair.T_normal_in_N {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : (bp.T.subgroupOf bp.N).Normal

$T$ is normal in $N$, since $T = \ker \pi$ as a subgroup of $N$.

noncomputable def BNPair.quotientToW {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : ↥bp.N ⧸ bp.T.subgroupOf bp.N →* M.Group

The induced homomorphism $N/T \to W$ obtained by descending $\pi : N \to W$ through its kernel $T$.

theorem BNPair.quotientToW_injective {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : Function.Injective ⇑bp.quotientToW

$N/T \to W$ is injective: its kernel equals $T/T = 1$.

theorem BNPair.quotientToW_surjective {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : Function.Surjective ⇑bp.quotientToW

$N/T \to W$ is surjective, since $\pi : N \to W$ is already surjective.

theorem BNPair.quotientToW_bijective {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : Function.Bijective ⇑bp.quotientToW

$N/T \to W$ is bijective.

noncomputable def BNPair.quotientIso {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : ↥bp.N ⧸ bp.T.subgroupOf bp.N ≃* M.Group

The isomorphism $N/T \cong W$. Packages quotientToW and its bijectivity into a group isomorphism, identifying the Weyl group $W$ of the Coxeter system with the quotient $N/T$ of the BN-pair.