noncomputable def FiniteReflectionGroups.linearReflection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (α v : E) : E

Linear reflection across the hyperplane orthogonal to $α$: $s_α(v) = v - (2⟨α,v⟩/⟨α,α⟩)·α$.

noncomputable def FiniteReflectionGroups.linearReflectionLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (α : E) : E →ₗ[ℝ] E

Linear reflection $s_α$ packaged as an $ℝ$-linear map.

@[simp]

theorem FiniteReflectionGroups.linearReflectionLM_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (α v : E) : (linearReflectionLM α) v = linearReflection α v

The linear-map version of $s_α$ agrees with the function version.

noncomputable def FiniteReflectionGroups.coroot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (α : E) : E

The coroot of $α$: $\check α = (2 / ⟨α,α⟩)·α$.

structure FiniteReflectionGroups.RootSystem (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Type u_2

A (finite) root system in an inner product space: a nonempty finite set $Φ$ of nonzero vectors that spans $E$ and is closed under reflection $s_α(β) ∈ Φ$ for all $α,β ∈ Φ$.

• roots : Finset E
• roots_ne_zero (α : E) : α ∈ self.roots → α ≠ 0
• roots_nonempty : self.roots.Nonempty
• reflection_closed (α : E) : α ∈ self.roots → ∀ β ∈ self.roots, linearReflection α β ∈ self.roots
• roots_span : Submodule.span ℝ ↑self.roots = ⊤

def FiniteReflectionGroups.RootSystem.IsReduced {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) : Prop

A root system is reduced if the only roots proportional to $α$ are $±α$.

def FiniteReflectionGroups.RootSystem.IsCrystallographic {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) : Prop

A root system is crystallographic if every pairing $⟨α, \check β⟩$ is an integer.

def FiniteReflectionGroups.RootSystem.corootSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) : Set E

The set of coroots $\{\check α : α ∈ Φ\}$.

def FiniteReflectionGroups.RootSystem.positiveRootSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) (f : E → ℝ) : Set E

Positive roots relative to a separating linear functional $f$: those $α ∈ Φ$ with $f(α) > 0$.

def FiniteReflectionGroups.RootSystem.negativeRootSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) (f : E → ℝ) : Set E

Negative roots relative to $f$: those $α ∈ Φ$ with $f(α) < 0$.

def FiniteReflectionGroups.RootSystem.IsSimpleRoot {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) (f : E → ℝ) (α : E) : Prop

A positive root $α$ is simple relative to $f$ if it is not a sum of two positive roots.

def FiniteReflectionGroups.RootSystem.simpleRootSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) (f : E → ℝ) : Set E

The set of simple roots relative to a separating functional $f$.

inductive FiniteReflectionGroups.RootSystem.WeylGroupMem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) : (E → E) → Prop

Inductive definition of membership in the Weyl group, generated by reflections $s_α$ for $α ∈ Φ$ under composition.

• id {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Φ : RootSystem E} : Φ.WeylGroupMem _root_.id
• gen {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Φ : RootSystem E} (α : E) (hα : α ∈ Φ.roots) : Φ.WeylGroupMem (linearReflection α)
• comp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Φ : RootSystem E} (f g : E → E) : Φ.WeylGroupMem f → Φ.WeylGroupMem g → Φ.WeylGroupMem (f ∘ g)

def FiniteReflectionGroups.RootSystem.weylGroupSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (Φ : RootSystem E) : Set (E → E)

The underlying set of the Weyl group inside $E → E$.