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 derivationD
is in the Killing orthogonal of the range of the adjoint action, then, for anyx : 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.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]
:
LieSubmodule R L (LieDerivation R L L)
The orthogonal complement of the inner derivations is a Lie submodule of all derivations.
Equations
- LieDerivation.IsKilling.rangeAdOrthogonal R L = { toSubmodule := (killingForm R (LieDerivation R L L)).orthogonal (LieDerivation.ad R L).range.toSubmodule, lie_mem := ⋯ }
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
instance
LieDerivation.IsKilling.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.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]
theorem
LieDerivation.IsKilling.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.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.