Levi's theorem

Let L be a finite-dimensional Lie algebra over a field of characteristic zero. Levi's theorem says that the solvable radical R of L has a complementary Lie subalgebra S, a Levi complement. Such an S is isomorphic to L ⧸ R, so it is semisimple, and L is the semidirect sum R ⋊ S for the adjoint action of S on R.

The theorem is proved more generally for a solvable ideal I whose quotient L ⧸ I has nondegenerate Killing form (LieIdeal.exists_lieSubalgebra_isCompl_of_isSolvable); the radical is such an ideal by Cartan's criterion. The general form is the one that admits an induction.

The argument

Induct on the dimension of L. Let A be the last nonzero term of the derived series of I: an abelian ideal of L contained in I. If I = 0 there is nothing to prove. Otherwise A ≠ 0, so L ⧸ A has smaller dimension, and its solvable ideal I ⧸ A has quotient L ⧸ I; by induction it has a complement S₁. The preimage P of S₁ in L is a Lie subalgebra with I + P = L and I ∩ P = A. The abelian ideal A of P has quotient P ⧸ A ≃ L ⧸ I, so the abelian case (LieIdeal.exists_lieSubalgebra_isCompl_of_isLieAbelian) complements it inside P, and that complement is a complement of I in L (LieIdeal.isCompl_map_incl).

Main results

• LieIdeal.exists_lieSubalgebra_isCompl_of_isSolvable: a solvable ideal with Killing quotient has a complementary Lie subalgebra.
• Ado.exists_leviComplement: Levi's theorem, the radical has a complementary Lie subalgebra.
• Ado.exists_leviDecomposition: the Levi decomposition, L ≃ R ⋊ S with S semisimple.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Springer GTM 129, Appendix E, for the proof of Levi's theorem by induction on the dimension.
• N. Jacobson, Lie Algebras, Chapter III, §9.

theorem LieIdeal.exists_lieSubalgebra_isCompl_of_isSolvable {K : Type u} [Field K] {L : Type v} [LieRing L] [LieAlgebra K L] [CharZero K] [FiniteDimensional K L] (I : LieIdeal K L) [LieAlgebra.IsSolvable ↥I] [LieAlgebra.IsKilling K (L ⧸ I)] : ∃ (S : LieSubalgebra K L), IsCompl (↑I) S.toSubmodule

A Levi complement of a solvable ideal. Over a field of characteristic zero, a solvable ideal I of a finite-dimensional Lie algebra L whose quotient L ⧸ I has nondegenerate Killing form has a complementary Lie subalgebra.

theorem Ado.exists_leviComplement (K : Type u) [Field K] (L : Type v) [LieRing L] [LieAlgebra K L] [CharZero K] [FiniteDimensional K L] : ∃ (S : LieSubalgebra K L), IsCompl (↑(LieAlgebra.radical K L)) S.toSubmodule

Levi's theorem. Over a field of characteristic zero, the solvable radical of a finite-dimensional Lie algebra has a complementary Lie subalgebra, a Levi complement.

theorem Ado.exists_leviDecomposition (K : Type u) [Field K] (L : Type v) [LieRing L] [LieAlgebra K L] [CharZero K] [FiniteDimensional K L] : ∃ (S : LieSubalgebra K L) (ψ : ↥S →ₗ⁅K⁆ LieDerivation K ↥(LieAlgebra.radical K L) ↥(LieAlgebra.radical K L)), LieAlgebra.IsSemisimple K ↥S ∧ Nonempty (L ≃ₗ⁅K⁆ ↥(LieAlgebra.radical K L) ⋊⁅ψ⁆ ↥S)

The Levi decomposition. Over a field of characteristic zero, a finite-dimensional Lie algebra is the semidirect sum of its solvable radical and a semisimple Lie subalgebra acting on the radical by the adjoint action.