Lie algebras with non-degenerate Killing forms.

In characteristic zero, the following three conditions are equivalent:

1. The solvable radical of a Lie algebra is trivial
2. A Lie algebra is a direct sum of its simple ideals
3. A Lie algebra has non-degenerate Killing form

In positive characteristic, it is still true that 3 implies 2, and that 2 implies 1, but there are counterexamples to the remaining implications. Thus condition 3 is the strongest assumption. Furthermore, much of the Cartan-Killing classification of semisimple Lie algebras in characteristic zero, continues to hold in positive characteristic (over a perfect field) if the Lie algebra has a non-degenerate Killing form.

This file contains basic definitions and results for such Lie algebras.

Main declarations

• LieAlgebra.IsKilling: a typeclass encoding the fact that a Lie algebra has a non-singular Killing form.
• LieAlgebra.IsKilling.instSemisimple: if a finite-dimensional Lie algebra over a field has non-singular Killing form then it is semisimple.
• LieAlgebra.IsKilling.instHasTrivialRadical: if a Lie algebra over a PID has non-singular Killing form then it has trivial radical.

TODO

• Prove that in characteristic zero, a semisimple Lie algebra has non-singular Killing form.

class LieAlgebra.IsKilling (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] : Prop

We say a Lie algebra is Killing if its Killing form is non-singular.

NB: This is not standard terminology (the literature does not seem to name Lie algebras with this property).

• killingCompl_top_eq_bot : LieIdeal.killingCompl R L ⊤ = ⊥

  We say a Lie algebra is Killing if its Killing form is non-singular.

@[simp]

theorem LieAlgebra.IsKilling.ker_killingForm_eq_bot (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [IsKilling R L] : LinearMap.ker (killingForm R L) = ⊥

theorem LieAlgebra.IsKilling.killingForm_nondegenerate (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [IsKilling R L] : (killingForm R L).Nondegenerate

theorem LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [IsKilling R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] (I : LieIdeal R L) [IsLieAbelian ↥I] : I = ⊥

instance LieAlgebra.IsKilling.instSemisimple (K : Type u_2) (L : Type u_3) [Field K] [LieRing L] [LieAlgebra K L] [IsKilling K L] [Module.Finite K L] : IsSemisimple K L

instance LieAlgebra.IsKilling.instHasTrivialRadical (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [IsKilling R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] : HasTrivialRadical R L

The converse of this is true over a field of characteristic zero. There are counterexamples over fields with positive characteristic.

Note that when the coefficients are a field this instance is redundant since we have LieAlgebra.IsKilling.instSemisimple and LieAlgebra.IsSemisimple.instHasTrivialRadical.

@[simp]

theorem LieAlgebra.killingForm_of_equiv_apply {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_4} [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') (x y : L) : ((killingForm R L') (e x)) (e y) = ((killingForm R L) x) y

Given an equivalence e of Lie algebras from L to L', and elements x y : L, the respective Killing forms of L and L' satisfy κ'(e x, e y) = κ(x, y).

theorem LieAlgebra.isKilling_of_equiv {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_4} [LieRing L'] [LieAlgebra R L'] [IsKilling R L] (e : L ≃ₗ⁅R⁆ L') : IsKilling R L'

Given a Killing Lie algebra L, if L' is isomorphic to L, then L' is Killing too.

theorem LieEquiv.isKilling {R : Type u_1} {L : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_4} [LieRing L'] [LieAlgebra R L'] [LieAlgebra.IsKilling R L] (e : L ≃ₗ⁅R⁆ L') : LieAlgebra.IsKilling R L'

Alias of LieAlgebra.isKilling_of_equiv.

---

Given a Killing Lie algebra L, if L' is isomorphic to L, then L' is Killing too.