theorem CoxeterGroup.sigmaLinearEquiv_isLiftable {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : M.IsLiftable fun (s : B) => sigmaLinearEquiv M s

The family of reflections $\sigma_s \in GL(\mathbb{R}^B)$ satisfies the Coxeter braid relations, so it satisfies the lifting hypothesis for $M$.

noncomputable def CoxeterGroup.coxeterRepresentation {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) {W : Type u_2} [Group W] (cs : CoxeterSystem M W) : W →* (B → ℝ) ≃ₗ[ℝ] B → ℝ

The geometric representation of $W$: the group homomorphism from $W$ to $GL(\mathbb{R}^B)$ sending each simple reflection $s_i$ to $\sigma_{s_i}$.

@[simp]

theorem CoxeterGroup.coxeterRepresentation_simple {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) {W : Type u_2} [Group W] (cs : CoxeterSystem M W) (s : B) : (coxeterRepresentation M cs) (cs.simple s) = sigmaLinearEquiv M s

The geometric representation sends a simple generator $s_i$ to the corresponding reflection $\sigma_{s_i}$ as a linear equivalence.

theorem CoxeterGroup.coxeterRepresentation_wordProd_apply {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) {W : Type u_2} [Group W] (cs : CoxeterSystem M W) (word : List B) (v : B → ℝ) : ((coxeterRepresentation M cs) (cs.wordProd word)) v = wordSigma M word v

The action of $\rho(\mathtt{wordProd}\,\omega)$ on a vector $v$ is exactly the iterated reflection $\sigma_{s_{i_1}} \cdots \sigma_{s_{i_k}}(v)$ encoded by $\mathtt{wordSigma}$.