Documentation

Mathlib.Algebra.Lie.Derivation.Killing

Derivations of finite dimensional Killing Lie algebras #

This file establishes that all derivations of finite-dimensional Killing Lie algebras are inner.

Main statements #

theorem LieDerivation.IsKilling.killingForm_restrict_range_ad (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] :
(killingForm R (LieDerivation R L L)).restrict (LieDerivation.ad R L).range.toSubmodule = killingForm R (LieDerivation.ad R L).range
@[simp]
theorem LieDerivation.IsKilling.rangeAdOrthogonal_carrier (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] :
(LieDerivation.IsKilling.rangeAdOrthogonal R L) = {m : LieDerivation R L L | ∀ (a : L), (killingForm R (LieDerivation R L L)).IsOrtho ((LieDerivation.ad R L) a) m}
noncomputable def LieDerivation.IsKilling.rangeAdOrthogonal (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] :

The orthogonal complement of the inner derivations is a Lie submodule of all derivations.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem LieDerivation.IsKilling.ad_mem_orthogonal_of_mem_orthogonal {R : Type u_1} {L : Type u_2} [Field R] [LieRing L] [LieAlgebra R L] {D : LieDerivation R L L} (hD : D (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule) (x : L) :
    (LieDerivation.ad R L) (D x) (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule

    If a derivation D is in the Killing orthogonal of the range of the adjoint action, then, for any x : L, ad (D x) is also in this orthogonal.

    theorem LieDerivation.IsKilling.ad_mem_ker_killingForm_ad_range_of_mem_orthogonal {R : Type u_1} {L : Type u_2} [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] {D : LieDerivation R L L} (hD : D (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule) (x : L) :
    (LieDerivation.ad R L) (D x) Submodule.map (LieDerivation.ad R L).range.subtype (LinearMap.ker (killingForm R (LieDerivation.ad R L).range))
    @[simp]
    theorem LieDerivation.IsKilling.ad_apply_eq_zero_iff (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [LieAlgebra.IsKilling R L] (x : L) :
    (LieDerivation.ad R L) x = 0 x = 0
    theorem LieDerivation.IsKilling.killingForm_restrict_range_ad_nondegenerate (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [LieAlgebra.IsKilling R L] :
    ((killingForm R (LieDerivation R L L)).restrict (LieDerivation.ad R L).range.toSubmodule).Nondegenerate

    The restriction of the Killing form of a finite-dimensional Killing Lie algebra to the range of the adjoint action is nondegenerate.

    @[simp]

    The range of the adjoint action on a finite-dimensional Killing Lie algebra is full.

    theorem LieDerivation.IsKilling.exists_eq_ad {R : Type u_1} {L : Type u_2} [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [LieAlgebra.IsKilling R L] (D : LieDerivation R L L) :
    ∃ (x : L), (LieDerivation.ad R L) x = D

    Every derivation of a finite-dimensional Killing Lie algebra is an inner derivation.