Reflections of the root system of a Cartan subalgebra #
For a finite-dimensional Lie algebra L with non-degenerate Killing form over a field of
characteristic zero, and a splitting Cartan subalgebra H, Mathlib packages the roots of H as a
root system LieAlgebra.IsKilling.rootSystem H inside the dual Module.Dual K H. This file reads
its reflections back in Lie-theoretic terms: the reflection in a root α sends a form χ to
χ - χ(α^∨) • α, where α^∨ is the coroot LieAlgebra.IsKilling.coroot α.
Main results #
Ado.coe_rootSystem_reflection_apply: the reflection of the root system in a root, read as a function on the Cartan subalgebra.
@[simp]
theorem
Ado.coe_rootSystem_reflection_apply
{K : Type u_1}
{L : Type u_2}
[Field K]
[CharZero K]
[LieRing L]
[LieAlgebra K L]
[LieAlgebra.IsKilling K L]
[FiniteDimensional K L]
{H : LieSubalgebra K L}
[H.IsCartanSubalgebra]
[LieModule.IsTriangularizable K (↥H) L]
(i : ↥LieSubalgebra.root)
(χ : Module.Dual K ↥H)
:
⇑(((LieAlgebra.IsKilling.rootSystem H).reflection i) χ) = ⇑χ - χ (LieAlgebra.IsKilling.coroot ↑i) • ⇑↑i
The reflection of the root system of H in a root i, read as a function on the Cartan
subalgebra, is χ ↦ χ - χ(αᵢ^∨) • αᵢ.