noncomputable def CoxeterGroup.sigmaLin {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : Module.End ℝ (B → ℝ)

The simple reflection $\sigma_s$ packaged as an $\mathbb{R}$-linear endomorphism of $\mathbb{R}^B$.

theorem CoxeterGroup.bilinForm_sigma_general {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v : B → ℝ) : bilinForm M (sigma M t v) (e s) = bilinForm M v (e s) - 2 * bilinForm M v (e t) * formVal M t s

General reflection formula: $\langle \sigma_t v, e_s\rangle = \langle v, e_s\rangle

• 2\langle v, e_t\rangle\langle e_t, e_s\rangle$.

theorem CoxeterGroup.bilinForm_sigma_e {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v : B → ℝ) : bilinForm M (sigma M s v) (e s) = -bilinForm M v (e s)

The simple reflection negates the pairing against its own simple root: $\langle \sigma_s v, e_s\rangle = -\langle v, e_s\rangle$.

theorem CoxeterGroup.sigma_sq {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : sigmaLin M s * sigmaLin M s = 1

Simple reflections are involutions: $\sigma_s^2 = \mathrm{id}$.

theorem CoxeterGroup.sigmaLin_e_self {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : (sigmaLin M s) (e s) = -e s

$\sigma_s$ sends its simple root $e_s$ to $-e_s$.

theorem CoxeterGroup.sigmaLin_e {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (_hst : s ≠ t) : (sigmaLin M s) (e t) = fun (u : B) => e t u - 2 * formVal M s t * e s u

Coordinate formula for the action of $\sigma_s$ on a distinct simple root $e_t$.