Abstract Jordan decomposition in Killing Lie algebras

Let L be a finite-dimensional Lie algebra with nondegenerate Killing form over a field K. Every element x : L whose adjoint action ad x is split (its generalized eigenspaces span L, which is automatic when K is algebraically closed) decomposes as x = n + s with ⁅n, s⁆ = 0, ad n nilpotent and ad s semisimple. When K is perfect these parts are unique. This is the abstract (or internal) Jordan decomposition: the Jordan–Chevalley decomposition of the endomorphism ad x does not a priori have its parts in the image of ad, and the decomposition here reconstructs them inside L.

The proof applies the Jordan–Chevalley decomposition of derivations (LieDerivation.exists_isNilpotent_isSemisimple_of_iSup_maxGenEigenspace_eq_top) to the inner derivation ad x: both parts are derivations, hence inner because every derivation of a Killing Lie algebra is inner (LieDerivation.IsKilling.exists_eq_ad), and ad is injective because the center is trivial. Uniqueness is the uniqueness of the Jordan–Chevalley decomposition of ad x together with injectivity of ad; it only needs L to act faithfully on itself and K to be perfect.

Main results

• TauCeti.exists_isNilpotent_ad_isSemisimple_ad_of_iSup_maxGenEigenspace_eq_top: existence of the decomposition for an element whose adjoint action is split.
• TauCeti.exists_isNilpotent_ad_isSemisimple_ad: existence over an algebraically closed field.
• TauCeti.isNilpotent_ad_isSemisimple_ad_unique: uniqueness, for a finite-dimensional Lie algebra with trivial center over a perfect field.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §5.4 (abstract Jordan decomposition).

theorem TauCeti.exists_isNilpotent_ad_isSemisimple_ad_of_iSup_maxGenEigenspace_eq_top {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] (x : L) (hx : ⨆ (μ : K), ((LieAlgebra.ad K L) x).maxGenEigenspace μ = ⊤) : ∃ (n : L) (s : L), (LieAlgebra.ad K L) n ∈ K[(LieAlgebra.ad K L) x] ∧ (LieAlgebra.ad K L) s ∈ K[(LieAlgebra.ad K L) x] ∧ IsNilpotent ((LieAlgebra.ad K L) n) ∧ ((LieAlgebra.ad K L) s).IsSemisimple ∧ ⁅n, s⁆ = 0 ∧ x = n + s

Abstract Jordan decomposition, existence for split elements. In a finite-dimensional Lie algebra with nondegenerate Killing form, an element x whose adjoint action has spanning generalized eigenspaces is a sum n + s of commuting elements with ad n nilpotent and ad s semisimple. Both ad n and ad s are polynomials in ad x.

theorem TauCeti.exists_isNilpotent_ad_isSemisimple_ad {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] [IsAlgClosed K] (x : L) : ∃ (n : L) (s : L), (LieAlgebra.ad K L) n ∈ K[(LieAlgebra.ad K L) x] ∧ (LieAlgebra.ad K L) s ∈ K[(LieAlgebra.ad K L) x] ∧ IsNilpotent ((LieAlgebra.ad K L) n) ∧ ((LieAlgebra.ad K L) s).IsSemisimple ∧ ⁅n, s⁆ = 0 ∧ x = n + s

Abstract Jordan decomposition, existence. In a finite-dimensional Lie algebra with nondegenerate Killing form over an algebraically closed field, every element x is a sum n + s of commuting elements with ad n nilpotent and ad s semisimple. Both ad n and ad s are polynomials in ad x.

theorem TauCeti.isNilpotent_ad_isSemisimple_ad_unique {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieModule.IsFaithful K L L] [PerfectField K] {n₁ s₁ n₂ s₂ : L} (hn₁ : IsNilpotent ((LieAlgebra.ad K L) n₁)) (hs₁ : ((LieAlgebra.ad K L) s₁).IsSemisimple) (hn₂ : IsNilpotent ((LieAlgebra.ad K L) n₂)) (hs₂ : ((LieAlgebra.ad K L) s₂).IsSemisimple) (hc₁ : ⁅n₁, s₁⁆ = 0) (hc₂ : ⁅n₂, s₂⁆ = 0) (h : n₁ + s₁ = n₂ + s₂) : n₁ = n₂ ∧ s₁ = s₂

Abstract Jordan decomposition, uniqueness. In a finite-dimensional Lie algebra with trivial center over a perfect field, if n₁ + s₁ = n₂ + s₂ where ⁅nᵢ, sᵢ⁆ = 0, ad nᵢ is nilpotent and ad sᵢ is semisimple, then n₁ = n₂ and s₁ = s₂.