Levi complements of abelian ideals

Let L be a finite-dimensional Lie algebra over a field of characteristic zero and I an ideal of L whose quotient L ⧸ I has nondegenerate Killing form. This file proves that I has a complementary Lie subalgebra whenever I is abelian (LieIdeal.exists_lieSubalgebra_isCompl_of_isLieAbelian), and a complementary ideal whenever I is central (LieIdeal.exists_isCompl_of_le_center).

These are the base cases of Levi's theorem. Its proof by induction on the dimension reduces to the case where the solvable radical R contains no nonzero proper ideal of L. Such an R is abelian, since its derived algebra is a proper ideal of L contained in R, and it is either central or meets the centre trivially.

The argument

A central ideal I is a Lie submodule of the adjoint module, on which I acts trivially, so Weyl's theorem for the action of L ⧸ I (LieSubmodule.exists_isCompl_of_le_ker) complements it by a submodule, that is, by an ideal.

For an abelian ideal I, let L act on its endomorphisms by commutators with the adjoint action, and consider the submodules

• C, the endomorphisms with range in I that act on I as a scalar;
• B ≤ C, those that vanish on I;
• A ≤ B, the inner derivations ad a by elements a ∈ I.

The algebra L carries C into B, and I carries C into A: for r ∈ I and φ ∈ C acting on I as c, the bracket ⁅r, φ⁆ is ad (-(c • r)). So L ⧸ I acts on C / A, and Weyl's theorem complements B / A in C / A; when I ≠ 0, the complement is nonzero, and as L carries it into B / A it consists of invariants. Rescaling a nonzero invariant gives a projection ψ of L onto I with ⁅x, ψ⁆ ∈ A for every x : L. Its stabilizer S = {x | ⁅x, ψ⁆ = 0} is a Lie subalgebra with I + S = L, and S ∩ I consists of central elements.

If I meets the centre trivially, S is already the complement; this is the classical argument. In general S ∩ I is a central ideal of S with quotient L ⧸ I, so the central case complements it inside S, and that complement is a complement of I in L.

The last step holds for any Lie subalgebra P with I + P = L: the quotient P ⧸ (I ∩ P) is isomorphic to L ⧸ I, and a complement of I ∩ P in P is a complement of I in L. These statements are supplied by TauCeti/Algebra/Lie/Quotient.lean and TauCeti/Algebra/Lie/Killing/Quotient.lean, since the induction for solvable ideals uses them again.

Main results

• LieIdeal.exists_isCompl_of_le_center: a central ideal with Killing quotient has a complementary ideal.
• LieIdeal.exists_lieSubalgebra_isCompl_of_isLieAbelian: an abelian ideal with Killing quotient has a complementary Lie subalgebra.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Springer GTM 129, Appendix E, for the proof of Levi's theorem by reduction to a minimal abelian ideal, and the submodules A ≤ B ≤ C used for an ideal meeting the centre trivially.

theorem LieIdeal.exists_isCompl_of_le_center {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [CharZero K] [FiniteDimensional K L] (I : LieIdeal K L) [LieAlgebra.IsKilling K (L ⧸ I)] (hI : I ≤ LieAlgebra.center K L) : ∃ (J : LieIdeal K L), IsCompl I J

A central ideal is a direct summand when the quotient by it has nondegenerate Killing form: it has a complementary ideal.

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

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