Borels from a Lie algebra basis

This file connects a LieAlgebra.Basis to the positive nilradical and Borel subalgebra determined by its root-system base. The positive nilradical is generated as a Lie algebra by the raising operators eᵢ, so the corresponding Borel is the Cartan subalgebra together with their Lie span.

The construction follows the simple-root presentation in Meinolf Geck, On the construction of semisimple Lie algebras and Chevalley groups, and the positive-root generation argument of Humphreys, Introduction to Lie Algebras and Representation Theory, §10.

Main results

• LieAlgebra.Basis.positiveNilradical_eq_lieSpan_e identifies the positive nilradical with the Lie span of the raising operators.
• LieAlgebra.Basis.borelSubalgebra_eq_sup_lieSpan_e gives the corresponding Borel.

theorem LieAlgebra.Basis.positiveNilradical_eq_lieSpan_e {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_1} [Fintype ι] (b : Basis ι H) : TauCeti.positiveNilradical H b.base = LieSubalgebra.lieSpan K L (Set.range b.e)

The positive nilradical associated to a Lie algebra basis is the Lie span of its raising operators.

theorem LieAlgebra.Basis.borelSubalgebra_eq_sup_lieSpan_e {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} {ι : Type u_1} [Fintype ι] (b : Basis ι H) : TauCeti.borelSubalgebra H b.base = H ⊔ LieSubalgebra.lieSpan K L (Set.range b.e)

The Borel associated to a Lie algebra basis is its Cartan subalgebra together with the Lie span of its raising operators.