theorem CoxeterGroup.wordSigma_reflection_root_neg {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word_u : List B) (j : B) : have α := wordSigma M word_u (e j); have u := cs.wordProd word_u; have t := u * cs.simple j * u⁻¹; ∀ (word_t : List B), cs.wordProd word_t = t → ∀ (v : B → ℝ), wordSigma M word_t v = generalizedReflection M α v

Conjugation identity: if $\alpha = \sigma_u(\alpha_j)$ and $t = u s_j u^{-1}$, then $\sigma_t$ acts on $\mathbb{R}^B$ as the generalized reflection $s_\alpha$ along $\alpha$. This is the Section 1.6 lemma $\beta = w\alpha \Rightarrow w s_\alpha w^{-1} = s_\beta$.

theorem CoxeterGroup.conjugate_reflection_eq {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word_u : List B) (j : B) : have α := wordSigma M word_u (e j); have u := cs.wordProd word_u; have t := u * cs.simple j * u⁻¹; ∀ (word_t : List B), cs.wordProd word_t = t → ∀ (v : B → ℝ), wordSigma M word_t v = generalizedReflection M α v

Alias of wordSigma_reflection_root_neg: the conjugated reflection acts as the generalized reflection along the conjugated root.

theorem CoxeterGroup.conj_simpleReflection_eq_generalizedReflection {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (w : W) (s : B) (v : B → ℝ) : ((coxeterRepresentation M cs) (w * cs.simple s * w⁻¹)) v = generalizedReflection M (((coxeterRepresentation M cs) w) (e s)) v

The Coxeter representation of $w s_i w^{-1}$ equals the generalized reflection along the root $w \cdot \alpha_i$.

theorem CoxeterGroup.pos_of_ascent_reflection {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word_w word_u : List B) (j : B) (hred_w : cs.IsReduced word_w) (hroot_pos : IsPositive (wordSigma M word_u (e j))) (hasc : cs.length (cs.wordProd word_w * (cs.wordProd word_u * cs.simple j * (cs.wordProd word_u)⁻¹)) > cs.length (cs.wordProd word_w)) : IsPositive (wordSigma M word_w (wordSigma M word_u (e j)))

Reflection positivity on ascent: for $\alpha = \sigma_u(\alpha_j)$ a positive root and $t = u s_j u^{-1}$, if $w$ is reduced and $\ell(wt) > \ell(w)$, then $\sigma_w(\alpha) > 0$.

theorem CoxeterGroup.neg_of_descent_reflection {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word_w word_u : List B) (j : B) (hred_w : cs.IsReduced word_w) (hroot_pos : IsPositive (wordSigma M word_u (e j))) (hdesc : cs.length (cs.wordProd word_w * (cs.wordProd word_u * cs.simple j * (cs.wordProd word_u)⁻¹)) < cs.length (cs.wordProd word_w)) : IsNegative (wordSigma M word_w (wordSigma M word_u (e j)))

Reflection negativity on descent: for $\alpha = \sigma_u(\alpha_j)$ a positive root and $t = u s_j u^{-1}$, if $w$ is reduced and $\ell(wt) < \ell(w)$, then $\sigma_w(\alpha) < 0$.