# 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) [] [] [] :

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 :

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

Instances
@[simp]
theorem LieAlgebra.IsKilling.killingCompl_top_eq_bot {R : Type u_1} {L : Type u_3} [] [] [] [self : ] :

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) [] [] [] [] :
theorem LieAlgebra.IsKilling.killingForm_nondegenerate (R : Type u_1) (L : Type u_3) [] [] [] [] :
().Nondegenerate
theorem LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian {R : Type u_1} {L : Type u_3} [] [] [] [] [] [] [] (I : LieIdeal R L) [IsLieAbelian I] :
I =
instance LieAlgebra.IsKilling.instSemisimple (K : Type u_2) (L : Type u_3) [] [] [] [] [] :
Equations
• =
instance LieAlgebra.IsKilling.instHasTrivialRadical (R : Type u_1) (L : Type u_3) [] [] [] [] [] [] [] :

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.

Equations
• =
@[simp]
theorem LieAlgebra.killingForm_of_equiv_apply {R : Type u_1} {L : Type u_3} [] [] [] {L' : Type u_5} [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R L') (x : L) (y : L) :
((killingForm R L') (e x)) (e y) = (() 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} [] [] [] {L' : Type u_5} [LieRing L'] [LieAlgebra R L'] [] (e : L ≃ₗ⁅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} [] [] [] {L' : Type u_5} [LieRing L'] [LieAlgebra R L'] [] (e : L ≃ₗ⁅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.