The derived algebra of a solvable Lie algebra

In characteristic zero, the derived algebra of a solvable Lie algebra acts nilpotently on any finite-dimensional module. In particular the derived algebra of a finite-dimensional solvable Lie algebra is nilpotent and lies in its nilradical. This is the structural input for controlling images of derivations by adjoining a derivation as a new Lie algebra element.

Lie's theorem supplies a nonzero common weight space after extending scalars to an algebraic closure. The derived algebra acts trivially on that space, and induction on the dimension of the quotient proves nilpotence. Nilpotence then descends along the injective scalar-extension map on endomorphisms, as in Mathlib's LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero.

References

• N. Jacobson, Lie Algebras, Interscience (1962), Chapter II, Lie's theorem and its corollaries.

theorem Ado.isNilpotent_derivedSeries_of_isSolvable {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsSolvable L] (M : Type u_3) [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] : LieModule.IsNilpotent (↥(LieAlgebra.derivedSeries K L 1)) M

In characteristic zero, the derived algebra of a solvable Lie algebra acts nilpotently on any finite-dimensional module, over the original field.

theorem Ado.derivedSeries_le_nilradical_of_isSolvable {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsSolvable L] [FiniteDimensional K L] : LieAlgebra.derivedSeries K L 1 ≤ LieAlgebra.nilradical K L

The derived algebra of a finite-dimensional solvable Lie algebra in characteristic zero is contained in its nilradical.