The Killing property as nondegeneracy of the Killing form

LieAlgebra.IsKilling R L is stated as the vanishing of the Killing orthogonal complement of the whole algebra. Mathlib turns that into nondegeneracy of the Killing form in LieAlgebra.IsKilling.killingForm_nondegenerate; this file supplies the converse and packages the two as an equivalence, saying that LieAlgebra.IsKilling is exactly nondegeneracy of the Killing form. That is the form in which the property is recognised when it is produced by a computation with the form itself, as under base change.

Main declarations

• Ado.isKilling_of_ker_killingForm_eq_bot: a Lie algebra whose Killing form has trivial kernel is Killing.
• Ado.isKilling_of_killingForm_nondegenerate: a Lie algebra whose Killing form is nondegenerate is Killing.
• Ado.isKilling_iff_killingForm_nondegenerate: LieAlgebra.IsKilling is exactly nondegeneracy of the Killing form.

Roadmap

This supports TauCeti/Algebra/Lie/Killing/BaseChange.lean, a prerequisite for Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, the Chevalley--Demazure construction.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §5.1, for the Killing form and Cartan's criterion.

theorem Ado.isKilling_of_ker_killingForm_eq_bot (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (h : LinearMap.ker (killingForm R L) = ⊥) : LieAlgebra.IsKilling R L

A Lie algebra whose Killing form has trivial kernel is Killing.

theorem Ado.isKilling_of_killingForm_nondegenerate (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (h : (killingForm R L).Nondegenerate) : LieAlgebra.IsKilling R L

A Lie algebra whose Killing form is nondegenerate is Killing.

This is the converse of LieAlgebra.IsKilling.killingForm_nondegenerate, and the two together say that LieAlgebra.IsKilling is exactly nondegeneracy of the Killing form.

theorem Ado.isKilling_iff_killingForm_nondegenerate (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.IsKilling R L ↔ (killingForm R L).Nondegenerate

A Lie algebra is Killing exactly when its Killing form is nondegenerate.