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) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : L →ₗ[R] L →ₗ[R] R

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

@[simp]

theorem LieModule.traceForm_apply_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) : ↑(↑(LieModule.traceForm R L M) x) y = ↑(LinearMap.trace R M) (LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (↑(LieModule.toEndomorphism R L M) y))

theorem LieModule.traceForm_comm (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) : ↑(↑(LieModule.traceForm R L M) x) y = ↑(↑(LieModule.traceForm R L M) y) x

@[simp]

theorem LieModule.traceForm_flip (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LinearMap.flip (LieModule.traceForm R L M) = LieModule.traceForm R L M

theorem LieModule.traceForm_apply_lie_apply (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (z : L) : ↑(↑(LieModule.traceForm R L M) ⁅x, y⁆) z = ↑(↑(LieModule.traceForm R L M) x) ⁅y, z⁆

@[simp]

theorem LieModule.traceForm_eq_zero_of_isNilpotent (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsReduced R] [LieModule.IsNilpotent R L M] : LieModule.traceForm R L M = 0

@[simp]

theorem LieModule.traceForm_eq_zero_of_isTrivial (R : Type u_1) (L : Type u_2) (M : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsTrivial L M] : LieModule.traceForm 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} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I ≤ LieSubmodule.idealizer N) (x : L) {y : L} (hy : y ∈ I) (hy' : optParam (∀ (m : M), m ∈ N → ↑(LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (↑(LieModule.toEndomorphism R L M) y)) m ∈ N) (_ : ∀ (m : M), m ∈ N → ⁅x, ↑(↑(LieModule.toEndomorphism R L M) y) m⁆ ∈ N.carrier)) : ↑(LinearMap.trace R M) (LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (↑(LieModule.toEndomorphism R L M) y)) = ↑(LinearMap.trace R { x // x ∈ ↑N }) (LinearMap.restrict (LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (↑(LieModule.toEndomorphism R L M) y)) hy')

theorem LieSubmodule.traceForm_eq_of_le_idealizer {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I ≤ LieSubmodule.idealizer N) : LieModule.traceForm R { x // x ∈ ↑I } { x // x ∈ ↑N } = LinearMap.compl₁₂ (LieModule.traceForm R L M) (Submodule.subtype ↑I) (Submodule.subtype ↑I)

theorem LieSubmodule.traceForm_eq_zero_of_isTrivial {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M) (I : LieIdeal R L) (h : I ≤ LieSubmodule.idealizer N) (x : L) {y : L} (hy : y ∈ I) [LieModule.IsTrivial { x // x ∈ ↑I } { x // x ∈ ↑N }] : ↑(LinearMap.trace R M) (LinearMap.comp (↑(LieModule.toEndomorphism R L M) x) (↑(LieModule.toEndomorphism R L M) 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) [CommRing R] [LieRing L] [LieAlgebra R L] : L →ₗ[R] L →ₗ[R] R

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.

noncomputable def LieIdeal.killingCompl (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieIdeal R L

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

@[simp]

theorem LieIdeal.mem_killingCompl (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {x : L} : x ∈ LieIdeal.killingCompl R L I ↔ ∀ (y : L), y ∈ I → ↑(↑(killingForm R L) x) y = 0

theorem LieIdeal.killingForm_eq (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] (I : LieIdeal R L) : killingForm R { x // x ∈ ↑I } = LinearMap.compl₁₂ (killingForm R L) (Submodule.subtype ↑I) (Submodule.subtype ↑I)

@[simp]

theorem LieIdeal.le_killingCompl_top_of_isLieAbelian (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] (I : LieIdeal R L) [IsLieAbelian { x // x ∈ ↑I }] : I ≤ LieIdeal.killingCompl R L ⊤

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

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

instance LieAlgebra.IsKilling.isSemisimple (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] [LieAlgebra.IsKilling R L] : LieAlgebra.IsSemisimple R L

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