Documentation

Mathlib.Algebra.Lie.Killing

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 #

TODO #

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

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).

Instances
    @[simp]

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

    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} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_5} [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R L') (x : L) (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_5} [LieRing L'] [LieAlgebra R L'] [LieAlgebra.IsKilling 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} [CommRing R] [LieRing L] [LieAlgebra R L] {L' : Type u_5} [LieRing L'] [LieAlgebra R L'] [LieAlgebra.IsKilling 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.