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

If $v$ is $B$-orthogonal to $e_s$, then the reflection $\sigma_s$ fixes $v$: $\sigma_s(v) = v$.

theorem CoxeterGroup.sigma_comp_fixes_orthogonal {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v : B → ℝ) (hs : bilinForm M v (e s) = 0) (ht : bilinForm M v (e t) = 0) : sigma M s (sigma M t v) = v

If $v$ is $B$-orthogonal to both $e_s$ and $e_t$, then $\sigma_s \sigma_t$ fixes $v$.

theorem CoxeterGroup.sigma_comp_e_s {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) : sigma M s (sigma M t (e s)) = fun (u : B) => (4 * formVal M s t ^ 2 - 1) * e s u - 2 * formVal M s t * e t u

Explicit formula for $\sigma_s \sigma_t$ applied to $e_s$ in terms of the matrix entry $B_{s,t}$.

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

Explicit formula for $\sigma_s \sigma_t$ applied to $e_t$.

structure CoxeterGroup.BraidRelationHyp {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Prop

The braid relation hypothesis on the geometric representation: for every pair $s, t$ with finite Coxeter order $m(s,t)$, the composition $\sigma_s \sigma_t$ has order dividing $m(s,t)$ on the representation.

• braid_power_eq_one (s t : B) : M.M s t ≠ 0 → ∀ (v : B → ℝ), (fun (w : B → ℝ) => sigma M s (sigma M t w))^[M.M s t] v = v