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.
A finite, free representation of a Lie algebra L
induces a bilinear form on L
called
the trace Form. See also killingForm
.
Instances For
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
).
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
The orthogonal complement of an ideal with respect to the killing form is an ideal.
Instances For
- killingCompl_top_eq_bot : LieIdeal.killingCompl R L ⊤ = ⊥
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
The converse of this is true over a field of characteristic zero. There are counterexamples over fields with positive characteristic.