Killing pairings of root spaces #
This file records consequences of the non-degeneracy of the Killing form for the root spaces of a splitting Cartan subalgebra, and the vanishing of brackets inside the Cartan subalgebra itself.
Main results #
Ado.killingForm_ne_zero_of_mem_rootSpace: nonzero vectors in opposite root spaces have nonzero Killing pairing.Ado.rootSpace_neg_eq_bot_iff: the roots are closed under negation, so a functional on the Cartan subalgebra is a root exactly when its negative is.Ado.lie_cartan_cartan_eq_zero: the Cartan subalgebra is abelian, so two of its elements have zero bracket in the ambient Lie algebra.
theorem
Ado.killingForm_ne_zero_of_mem_rootSpace
{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]
{α : LieModule.Weight K (↥H) L}
(hα : α.IsNonZero)
{e f : L}
(he : e ∈ LieAlgebra.rootSpace H ⇑α)
(he₀ : e ≠ 0)
(hf : f ∈ LieAlgebra.rootSpace H (-⇑α))
(hf₀ : f ≠ 0)
:
Nonzero vectors in opposite root spaces have nonzero Killing pairing.
@[simp]
theorem
Ado.rootSpace_neg_eq_bot_iff
{K : Type u_1}
{L : Type u_2}
[Field K]
[LieRing L]
[LieAlgebra K L]
[LieAlgebra.IsKilling K L]
[FiniteDimensional K L]
{H : LieSubalgebra K L}
[H.IsCartanSubalgebra]
[LieModule.IsTriangularizable K (↥H) L]
(χ : ↥H → K)
:
The roots of a Lie algebra with non-degenerate Killing form are closed under negation, so a functional on the Cartan subalgebra is a root exactly when its negative is.
theorem
Ado.lie_cartan_cartan_eq_zero
{K : Type u_1}
{L : Type u_2}
[Field K]
[LieRing L]
[LieAlgebra K L]
[LieAlgebra.IsKilling K L]
[FiniteDimensional K L]
{H : LieSubalgebra K L}
[H.IsCartanSubalgebra]
(y z : ↥H)
:
A splitting Cartan subalgebra is abelian, so any two of its elements have zero bracket in the ambient Lie algebra.