Derivations of finite dimensional Killing Lie algebras

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

Main statements

• LieDerivation.Killing.ad_mem_orthogonal_of_mem_orthogonal: 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.
• LieDerivation.Killing.range_ad_eq_top: in a finite-dimensional Lie algebra with non-degenerate Killing form, the range of the adjoint action is full,
• LieDerivation.Killing.exists_eq_ad: in a finite-dimensional Lie algebra with non-degenerate Killing form, any derivation is an inner derivation.

theorem LieDerivation.Killing.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.Killing.rangeAdOrthogonal_carrier (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] : ↑(LieDerivation.Killing.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.Killing.rangeAdOrthogonal (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] : LieSubmodule R L (LieDerivation R L 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.

theorem LieDerivation.Killing.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.Killing.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.Killing.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

instance LieDerivation.Killing.instIsKilling_range_ad (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [LieAlgebra.IsKilling R L] : LieAlgebra.IsKilling R ↥(LieDerivation.ad R L).range

Equations

• ⋯ = ⋯

theorem LieDerivation.Killing.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]

theorem LieDerivation.Killing.range_ad_eq_top (R : Type u_1) (L : Type u_2) [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] [LieAlgebra.IsKilling R L] : (LieDerivation.ad R L).range = ⊤

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

theorem LieDerivation.Killing.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.