theorem FiniteReflectionGroups.RootSystem.weylGroupMem_maps_roots {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) {g : E → E} (hg : Φ.WeylGroupMem g) (β : E) : β ∈ Φ.roots → g β ∈ Φ.roots

Every element of the Weyl group maps the root system to itself.

theorem FiniteReflectionGroups.foldr_refl_comp_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (αs₁ αs₂ : List E) (x : E) : List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id αs₁ (List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id αs₂ x) = List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id (αs₁ ++ αs₂) x

Composition of two right-folded reflection products equals the fold over the concatenation.

theorem FiniteReflectionGroups.RootSystem.weylGroupMem_is_composition {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) {g : E → E} (hg : Φ.WeylGroupMem g) : ∃ (αs : List E), (∀ a ∈ αs, a ∈ Φ.roots) ∧ g = List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id αs

Every Weyl-group element is a finite composition of reflections $s_{α_1} \cdots s_{α_k}$ with $α_i ∈ Φ$.

theorem FiniteReflectionGroups.foldr_refl_is_linear {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (αs : List E) : ∃ (L : E →ₗ[ℝ] E), ∀ (v : E), L v = List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id αs v

A composition of reflections is a linear map.

theorem FiniteReflectionGroups.foldr_refl_eq_of_agree_on_roots {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (αs₁ αs₂ : List E) (S : Set E) (hS : Submodule.span ℝ S = ⊤) (h : ∀ x ∈ S, List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id αs₁ x = List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id αs₂ x) : List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id αs₁ = List.foldr (fun (a : E) (f : E → E) => linearReflection a ∘ f) id αs₂

Two reflection compositions that agree on a spanning set are equal as functions.

noncomputable def FiniteReflectionGroups.restrictToRoots {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) (g : E → E) : ↥Φ.roots → ↥Φ.roots

Restriction of an endomorphism $g$ of $E$ to the finite set $Φ$ of roots, falling back to the identity when $g$ does not preserve roots.

theorem FiniteReflectionGroups.restrictToRoots_val {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) {g : E → E} (hg : Φ.WeylGroupMem g) (β : ↥Φ.roots) : ↑(restrictToRoots Φ g β) = g ↑β

For Weyl-group elements the restriction agrees with $g$ on the roots.

theorem FiniteReflectionGroups.linearReflection_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (α : E) (hα : α ≠ 0) : linearReflection α α = -α

A reflection sends its defining root to its negative: $s_α(α) = -α$.

theorem FiniteReflectionGroups.RootSystem.neg_mem_roots {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) {α : E} (hα : α ∈ Φ.roots) : -α ∈ Φ.roots

Root systems are stable under negation: if $α ∈ Φ$ then $-α ∈ Φ$.

theorem FiniteReflectionGroups.foldr_comp_append {α : Type u_2} (l₁ l₂ : List (α → α)) : List.foldr (fun (x1 x2 : α → α) => x1 ∘ x2) id l₁ ∘ List.foldr (fun (x1 x2 : α → α) => x1 ∘ x2) id l₂ = List.foldr (fun (x1 x2 : α → α) => x1 ∘ x2) id (l₁ ++ l₂)

The right-fold of $\circ$ over a list distributes over list append.

theorem FiniteReflectionGroups.ofFn_linearReflection_append {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n₁ n₂ : ℕ} (αs₁ : Fin n₁ → E) (αs₂ : Fin n₂ → E) : (List.ofFn fun (i : Fin (n₁ + n₂)) => linearReflection (Fin.append αs₁ αs₂ i)) = (List.ofFn fun (i : Fin n₁) => linearReflection (αs₁ i)) ++ List.ofFn fun (i : Fin n₂) => linearReflection (αs₂ i)

List.ofFn of a Fin.append of two reflection families equals the concatenation of the individual List.ofFns.

theorem FiniteReflectionGroups.RootSystem.list_foldr_weylGroupMem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) (αs : List E) (hαs : ∀ a ∈ αs, a ∈ Φ.roots) : Φ.WeylGroupMem (List.foldr (fun (a : E) (g : E → E) => linearReflection a ∘ g) id αs)

Any right-fold of reflections by roots is an element of the Weyl group.