The cyclic subgroup generated by a simple reflection $s$ has exactly two elements: $\langle s \rangle = \{1, s\}$, since $s^2 = 1$.
Every simple reflection $s$ is a right descent of the longest element $w_0$: $\ell(w_0 s) < \ell(w_0)$. Otherwise $w_0 s$ would be longer than $w_0$, contradicting maximality.
Right-multiplying the longest element $w_0$ by any simple reflection $s$ decreases length by exactly one: $\ell(w_0 s) = \ell(w_0) - 1$.
Every simple reflection $s$ is a left descent of $w_0$: $\ell(sw_0) < \ell(w_0)$.
Left-multiplying $w_0$ by any simple reflection $s$ decreases length by one: $\ell(s w_0) = \ell(w_0) - 1$.
The longest element is an involution: $w_0^2 = 1$. Since $\ell(w_0^{-1}) = \ell(w_0)$, $w_0^{-1}$ is also a maximal-length element, and uniqueness forces $w_0^{-1} = w_0$.
Type-preserving involution induced by $w_0$. If $w_0$ conjugates each cyclic parabolic $\langle s \rangle$ to another cyclic parabolic $\langle s' \rangle$, then in fact $w_0 \cdot s \cdot w_0^{-1} = s'$ on the nose (not just on the closures). Eliminates the "$=1$" case using $\ell(s) = 1$.
A spherical BN-pair: a BN-pair whose Weyl group $W$ is finite. Axiomatized by existence of a longest element $w_0$ (unique, of maximal length), the fact that $w_0$ conjugates each simple reflection to another simple reflection (an involution on $S$), and structural identities relating the torus, Borel and Levi components needed for the opposite-parabolic / Levi-decomposition theory of finite Coxeter / Tits systems.
- π_surj : Function.Surjective ⇑self.π
- w₀ : M.Group
- w₀_unique (w : M.Group) : (∀ (v : M.Group), M.toCoxeterSystem.length v ≤ M.toCoxeterSystem.length w) → w = self.w₀
- w₀_conj_parabolic (s : B_idx) : ∃ (s' : B_idx), Subgroup.closure {self.w₀ * M.toCoxeterSystem.simple s * self.w₀⁻¹} = Subgroup.closure {M.toCoxeterSystem.simple s'}
- levi_normalization (T : Set B_idx) (n : ↥self.N) : self.π n = self.w₀ → ∀ g ∈ self.standardParabolic T, (fun (s : G) => g * s * g⁻¹) '' (self.standardParabolic T ∩ (fun (s : G) => ↑n * s * (↑n)⁻¹) '' self.standardParabolic T) ⊆ self.standardParabolic T
- levi_weyl_group (T : Set B_idx) (n : ↥self.N) : self.π n = self.w₀ → ∀ (w : M.Group), w ∈ ↑(self.parabolicSubgroupW T) ↔ self.bruhatCell w ⊆ self.standardParabolic T ∩ (fun (s : G) => ↑n * s * (↑n)⁻¹) '' self.standardParabolic T
Instances For
The longest element $w_0$ of a spherical Weyl group, exposed as a definition.
Instances For
$w_0$ is an involution: $w_0^2 = 1$.
$w_0$ permutes the simple reflections by conjugation: for each $s$ there is $s'$ with $w_0 s w_0^{-1} = s'$.
Restatement of w₀_sq in product form: $w_0 \cdot w_0 = 1$.
$w_0^{-1} = w_0$, equivalent to $w_0^2 = 1$.
Conjugation of a subset $S \subseteq G$ by a single element $g$: $gSg^{-1}$.
Instances For
Conjugation of $S \subseteq G$ by a chosen $N$-lift of a Weyl element $w$.
Instances For
The opposite Borel $B^- = n_{w_0} B n_{w_0}^{-1}$, obtained by conjugating $B$ through a chosen $N$-lift of $w_0$.
Instances For
The opposite parabolic $P_T^- = n_{w_0} P_T n_{w_0}^{-1}$, for $T \subseteq S$.
Instances For
The Levi component $L = B \cap B^-$ of the BN-pair, the intersection of $B$ with its opposite.
Instances For
The Levi component of a parabolic $L_T = P_T \cap P_T^-$, generalizing
leviComponent (which is the case $T = \emptyset$).
Instances For
Specification of the noncomputably chosen $N$-lift of $w_0$: its image under $\pi$ is $w_0$.
Alias for w₀_conj_simple emphasizing that $w_0$ induces an automorphism (a permutation)
of the index set $S$ of simple reflections.
The $w_0$-induced permutation of $S$ is an involution. Conjugation by $w_0$ maps each simple reflection to another simple reflection, and this map is its own inverse: if $w_0 s w_0^{-1} = s'$ then $w_0 s' w_0^{-1} = s$. Direct consequence of $w_0^2 = 1$.
Unfolding equation for leviComponent: $L = B \cap n_{w_0} B n_{w_0}^{-1}$, made
explicit at the level of choose for the noncomputable $N$-lift.
Unfolding equation for leviComponentGeneral: $L_T = P_T \cap n_{w_0} P_T n_{w_0}^{-1}$.