A Lie algebra with nondegenerate Killing form is perfect

A finite-dimensional Lie algebra L whose Killing form κ is nondegenerate satisfies ⁅L, L⁆ = L. The proof is a two-line use of the invariance κ ⁅x, y⁆ z = κ x ⁅y, z⁆: a linear form vanishing on the derived ideal is κ x for a unique x, and then κ ⁅x, y⁆ z = κ x ⁅y, z⁆ vanishes for all z, so x is central; a central element of a Killing algebra is zero, so the form is zero and the derived ideal was already everything.

The statement is recorded here in the form its consumers use: an action of L that composes to zero is itself zero (TauCeti.isTrivial_of_derivedSeries_one_eq_top_of_lie_lie_eq_zero), which is what turns a two-step filtration of a module into a trivial action. This is the step that rules out the degenerate case in the Casimir proof of Weyl's complete reducibility theorem, where a module M with ⁅L, M⁆ ⊆ N and N acted on trivially would otherwise escape the argument.

Main results

• TauCeti.derivedSeries_one_eq_top_of_isKilling: a Lie algebra with nondegenerate Killing form is perfect.
• TauCeti.isTrivial_of_derivedSeries_one_eq_top_of_lie_lie_eq_zero: over a perfect Lie algebra, a module on which the action composes to zero is a trivial module.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §5.2, where perfectness is deduced from the decomposition of a semisimple Lie algebra into simple ideals; the argument here uses only the nondegeneracy and the invariance of the Killing form.

theorem TauCeti.derivedSeries_one_eq_top_of_isKilling (K : Type u_1) (L : Type u_2) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] : LieAlgebra.derivedSeries K L 1 = ⊤

A Lie algebra with nondegenerate Killing form is perfect: ⁅L, L⁆ = L.

A linear form killing the derived ideal is κ x for some x, by nondegeneracy of the Killing form on a finite-dimensional space. Invariance turns κ x ⁅y, z⁆ = 0 into κ ⁅x, y⁆ z = 0 for all z, so ⁅x, y⁆ = 0 for every y; then ad x = 0, so κ x vanishes identically and x = 0. The linear form was therefore zero, which contradicts the properness of the derived ideal.

theorem TauCeti.isTrivial_of_derivedSeries_one_eq_top_of_lie_lie_eq_zero {K : Type u_1} {L : Type u_2} [CommRing K] [LieRing L] [LieAlgebra K L] {M : Type u_3} [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] (hL : LieAlgebra.derivedSeries K L 1 = ⊤) (h : ∀ (x y : L) (m : M), ⁅x, ⁅y, m⁆⁆ = 0) : LieModule.IsTrivial L M

Over a perfect Lie algebra an action that composes to zero is zero. Each bracket ⁅y, z⁆ acts as a composite of two actions by the Leibniz rule, hence by zero, and the brackets span a perfect Lie algebra.