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 #

TODO #

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] :

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) [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] :
    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]
    @[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] :
    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 Nx, ↑(↑(LieModule.toEndomorphism R L M) y) m N.carrier)) :
    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 }] :

    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] :

    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) [CommRing R] [LieRing L] [LieAlgebra R L] (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) [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
        class LieAlgebra.IsKilling (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] :

        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.