# Documentation

Mathlib.Algebra.Lie.Killing

# The trace and Killing forms of a Lie algebra. #

Let L be a Lie algebra with coefficients in a commutative ring R. Suppose M is a finite, free R-module and we have a representation φ : L → End M. This data induces a natural bilinear form B on L, called the trace form associated to M; it is defined as B(x, y) = Tr (φ x) (φ y).

In the special case that M is L itself and φ is the adjoint representation, the trace form is known as the Killing form.

We define the trace / Killing form in this file and prove some basic properties.

## Main definitions #

• LieModule.traceForm
• LieModule.traceForm_eq_zero_of_isNilpotent
• killingForm
• LieAlgebra.IsKilling
• LieAlgebra.IsKilling.isSemisimple

## TODO #

• Prove that in characteristic zero, a semisimple Lie algebra has non-singular Killing form.
• If the Killing form is non-degenerate, then so is its restriction to a Cartan subalgebra.
noncomputable def LieModule.traceForm (R : Type u_1) (L : Type u_2) (M : Type u_3) [] [] [] [] [Module R M] [] [LieModule R L M] :

A finite, free representation of a Lie algebra L induces a bilinear form on L called the trace Form. See also killingForm.

Instances For
@[simp]
theorem LieModule.traceForm_apply_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (y : L) :
↑(↑() x) y = ↑() (LinearMap.comp (↑() x) (↑() y))
theorem LieModule.traceForm_comm (R : Type u_1) (L : Type u_2) (M : Type u_3) [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (y : L) :
↑(↑() x) y = ↑(↑() y) x
@[simp]
theorem LieModule.traceForm_flip (R : Type u_1) (L : Type u_2) (M : Type u_3) [] [] [] [] [Module R M] [] [LieModule R L M] :
=
theorem LieModule.traceForm_apply_lie_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [] [] [] [] [Module R M] [] [LieModule R L M] (x : L) (y : L) (z : L) :
↑(↑() x, y) z = ↑(↑() x) y, z
@[simp]
theorem LieModule.traceForm_eq_zero_of_isNilpotent (R : Type u_1) (L : Type u_2) (M : Type u_3) [] [] [] [] [Module R M] [] [LieModule R L M] [] [] [] [] :
= 0
@[simp]
theorem LieModule.traceForm_eq_zero_of_isTrivial (R : Type u_1) (L : Type u_2) (M : Type u_3) [] [] [] [] [Module R M] [] [LieModule R L M] [] :
= 0
theorem LieSubmodule.trace_eq_trace_restrict_of_le_idealizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] [] [] [] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : ) (x : L) {y : L} (hy : y I) (hy' : optParam (∀ (m : M), m N↑(LinearMap.comp (↑() x) (↑() y)) m N) (_ : ∀ (m : M), m Nx, ↑(↑() y) m N.carrier)) :
↑() (LinearMap.comp (↑() x) (↑() y)) = ↑(LinearMap.trace R { x // x N }) (LinearMap.restrict (LinearMap.comp (↑() x) (↑() y)) hy')
theorem LieSubmodule.traceForm_eq_of_le_idealizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] [] [] [] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : ) :
LieModule.traceForm R { x // x I } { x // x N } = LinearMap.compl₁₂ () () ()
theorem LieSubmodule.traceForm_eq_zero_of_isTrivial {R : Type u_1} {L : Type u_2} {M : Type u_3} [] [] [] [] [Module R M] [] [LieModule R L M] [] [] [] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : ) (x : L) {y : L} (hy : y I) [LieModule.IsTrivial { x // x I } { x // x N }] :
↑() (LinearMap.comp (↑() x) (↑() y)) = 0

Note that this result is slightly stronger than it might look at first glance: we only assume that N is trivial over I rather than all of L. This means that it applies in the important case of an Abelian ideal (which has M = L and N = I).

@[inline, reducible]
noncomputable abbrev killingForm (R : Type u_1) (L : Type u_2) [] [] [] :

A finite, free (as an R-module) Lie algebra L carries a bilinear form on L.

This is a specialisation of LieModule.traceForm to the adjoint representation of L.

Instances For
noncomputable def LieIdeal.killingCompl (R : Type u_1) (L : Type u_2) [] [] [] (I : LieIdeal R L) :

The orthogonal complement of an ideal with respect to the killing form is an ideal.

Instances For
@[simp]
theorem LieIdeal.mem_killingCompl (R : Type u_1) (L : Type u_2) [] [] [] (I : LieIdeal R L) {x : L} :
x ∀ (y : L), y I↑(↑() x) y = 0
theorem LieIdeal.killingForm_eq (R : Type u_1) (L : Type u_2) [] [] [] [] [] [] (I : LieIdeal R L) :
killingForm R { x // x I } = LinearMap.compl₁₂ () () ()
@[simp]
theorem LieIdeal.le_killingCompl_top_of_isLieAbelian (R : Type u_1) (L : Type u_2) [] [] [] [] [] [] (I : LieIdeal R L) [IsLieAbelian { x // x I }] :
I
class LieAlgebra.IsKilling (R : Type u_1) (L : Type u_2) [] [] [] :
• killingCompl_top_eq_bot :

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

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

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

Instances
instance LieAlgebra.IsKilling.isSemisimple (R : Type u_1) (L : Type u_2) [] [] [] [] [] [] [] :

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