Simplicity of the split even orthogonal Lie algebra #
The split orthogonal Lie algebra on Fin n ⊕ Fin n is simple for 4 ≤ n over a field of
characteristic zero. Consequently its Killing form is nondegenerate.
The Killing certificate makes the generic Borel and highest-weight APIs available for the concrete
type-D basis TypeDStd.lieBasis. In particular,
LieAlgebra.Basis.borelSubalgebra_eq_sup_lieSpan_e describes its compatible Borel using the
diagonal Cartan and raising generators, while
LieAlgebra.Basis.isHighestWeightVector_iff_forall_e reduces highest-weight conditions to the
action of those generators.
Main results #
TauCeti.TypeDStd.isSimple_typeD: the split type-DLie algebra is simple.TauCeti.TypeDStd.isKilling_typeD: its Killing form is nondegenerate.
References #
- N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§8, 14.
theorem
TauCeti.TypeDStd.isSimple_typeD
{K : Type u_1}
[Field K]
[CharZero K]
(n : ℕ)
(hn : 4 ≤ n)
:
LieAlgebra.IsSimple K ↥(LieAlgebra.Orthogonal.typeD (Fin n) K)
The split even orthogonal Lie algebra of type Dₙ is simple in characteristic zero.
theorem
TauCeti.TypeDStd.isKilling_typeD
{K : Type u_1}
[Field K]
[CharZero K]
(n : ℕ)
(hn : 4 ≤ n)
:
LieAlgebra.IsKilling K ↥(LieAlgebra.Orthogonal.typeD (Fin n) K)
The Killing form of the split even orthogonal Lie algebra of type Dₙ is nondegenerate in
characteristic zero.