theorem CoxeterGroup.sigma_preserves_coord {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (t s₀ : B) (hts : t ≠ s₀) (v : B → ℝ) : sigma M t v s₀ = v s₀

For $t \neq s_0$, the geometric reflection $\sigma_t$ preserves the $s_0$-coordinate.

theorem CoxeterGroup.e_self {B : Type u_1} [DecidableEq B] [Fintype B] (s : B) : e s s = 1

The $s$-coordinate of the standard basis vector $\alpha_s$ equals $1$.

theorem CoxeterGroup.sigma_injective {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (h : sigma M s = sigma M t) : s = t

Injectivity of $s \mapsto \sigma_s$: equality of two simple reflections in the geometric representation forces equality of the simple generators.

theorem CoxeterSystem.simple_injective {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Function.Injective cs.simple

The map $s \mapsto s_W$ from $S$ into $W$ is injective.

theorem CoxeterSystem.coxRep_mul_apply {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W) (v : B → ℝ) : ((CoxeterGroup.coxeterRepresentation M cs) (w₁ * w₂)) v = ((CoxeterGroup.coxeterRepresentation M cs) w₁) (((CoxeterGroup.coxeterRepresentation M cs) w₂) v)

Compatibility of the Coxeter representation with multiplication: $\rho(w_1 w_2) v = \rho(w_1)(\rho(w_2) v)$.

theorem CoxeterSystem.mem_of_simple_mem_closure {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (S' : Set B) (s₀ : B) (hs : cs.simple s₀ ∈ Subgroup.closure (cs.simple '' S')) : s₀ ∈ S'

Positivity test for parabolic subgroups: if $s_0 \in S$ but $s_{0,W}$ lies in the parabolic $W_{S'}$ generated by $\{s_W : s \in S'\}$, then $s_0 \in S'$.

theorem CoxeterSystem.parabolicSubgroup_injective {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (S₁ S₂ : Set B) (h : Subgroup.closure (cs.simple '' S₁) = Subgroup.closure (cs.simple '' S₂)) : S₁ = S₂

Parabolic subgroup injectivity: $S_1 \mapsto W_{S_1}$ is injective, i.e. $W_{S_1} = W_{S_2} \Rightarrow S_1 = S_2$.