Cartan's criteria

The two Cartan criteria characterise solvability and semisimplicity of finite-dimensional Lie algebras over fields of characteristic zero in terms of the Killing form: solvability via its vanishing on L × ⁅L, L⁆, semisimplicity via its non-degeneracy.

Main results

• LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero: over a field of characteristic zero, if a finite-dimensional representation M of L has trivial trace form, then M is nilpotent as a ⁅L, L⁆-module.
• LieAlgebra.isSolvable_of_killingForm_apply_lie_eq_zero: Cartan's criterion for solvability: if the Killing form of a Lie algebra L vanishes on L × ⁅L, L⁆, then L is solvable.
• LieAlgebra.killingCompl_top_le_radical: the Killing radical of a finite-dimensional Lie algebra is contained in the solvable radical.
• LieAlgebra.HasTrivialRadical.instIsKilling: Cartan's criterion for semisimplicity: if a finite-dimensional Lie algebra has trivial solvable radical, then its Killing form is non-degenerate.

TODO

• Add the converse direction of LieAlgebra.isSolvable_of_killingForm_apply_lie_eq_zero by proving radical R L = (derivedSeries R L 1).killingCompl R L.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3 Chapter I. §5.4
• J. Humphreys, Introduction to Lie Algebras and ... Chapter II 4.3

theorem LieModule.isNilpotent_derivedSeries_of_traceForm_eq_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [CharZero R] [IsDomain R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [LieRingModule L M] [Module R M] [LieModule R L M] [IsNoetherian R M] [Module.Free R M] (h : traceForm R L M = 0) : IsNilpotent (↥(LieAlgebra.derivedSeries R L 1)) M

If the trace form of M is zero, then the ⁅L, L⁆-module M is nilpotent.

theorem LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zero {R : Type u_1} {L : Type u_2} [CommRing R] [CharZero R] [IsDomain R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] [Module.Free R L] (I : LieIdeal R L) (h : ∀ x ∈ I, ∀ y ∈ ⁅I, I⁆, ((killingForm R L) x) y = 0) : LieAlgebra.IsSolvable ↥I

A convenience variation of LieAlgebra.isSolvable_of_forall_derived_killingForm_eq_zero for working with ideals.

Over a principal ideal domain by LieIdeal.killingForm_eq this is just a specialisation of LieAlgebra.isSolvable_of_killingForm_apply_lie_eq_zero but since it does not require the PID assumption, it is a slightly stronger result.

theorem LieAlgebra.killingCompl_top_le_radical (R : Type u_1) (L : Type u_2) [CommRing R] [CharZero R] [IsDomain R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] [Module.Free R L] : LieIdeal.killingCompl R L ⊤ ≤ radical R L

The Killing radical of a finite-dimensional Lie algebra is contained in the solvable radical.

instance LieAlgebra.HasTrivialRadical.instIsKilling (R : Type u_1) (L : Type u_2) [CommRing R] [CharZero R] [IsDomain R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] [Module.Free R L] [HasTrivialRadical R L] : IsKilling R L

Cartan's criterion for semisimplicity: if a finite-dimensional Lie algebra has trivial solvable radical, then its Killing form is non-degenerate.

See also LieAlgebra.hasTrivialRadical_iff_isKilling.