Jordan–Chevalley decomposition of Lie derivations

The Jordan–Chevalley decomposition D = N + S of a derivation D of a finite-dimensional Lie algebra, taken in the associative algebra of endomorphisms, has both parts again derivations. This is not formal: the parts are polynomials in D, and a polynomial expression in a derivation is in general not a derivation. The proof goes through generalized eigenspaces.

• A twisted Leibniz rule shows that the bracket of a generalized a-eigenvector and a generalized b-eigenvector of a derivation is a generalized (a + b)-eigenvector.
• The semisimple part S acts by the scalar a on the generalized a-eigenspace of D. Hence S satisfies the Leibniz rule on pairs of generalized eigenvectors, and so everywhere once the generalized eigenspaces of D span, for instance over an algebraically closed field. The nilpotent part N = D - S is then a derivation by subtraction.

The second step adapts the argument in Mathlib's proof of LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, which shows the same way that the semisimple part of ad x is a derivation, with root spaces of a Cartan subalgebra in place of the generalized eigenspaces of D.

This is the derivation-level input for the abstract Jordan decomposition of elements of a Lie algebra all of whose derivations are inner.

Main results

• LieDerivation.pow_sub_smul_one_apply_lie: the twisted Leibniz rule for powers of D - c.
• LieDerivation.lie_mem_maxGenEigenspace: brackets of generalized eigenvectors of a derivation add their eigenvalues.
• LieDerivation.apply_lie_eq_add_of_isNilpotent_sub: an endomorphism commuting with a split derivation D, finitely semisimple, and differing from D by a nilpotent map, satisfies the Leibniz rule.
• LieDerivation.exists_isNilpotent_isSemisimple_of_iSup_maxGenEigenspace_eq_top and LieDerivation.exists_isNilpotent_isSemisimple: the nilpotent and semisimple parts of a split derivation, respectively of any derivation over an algebraically closed field, are derivations.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §4.2, Lemma 4.2 (the semisimple and nilpotent parts of a derivation are derivations).

theorem LieDerivation.pow_sub_smul_one_apply_lie {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) (a b : R) (n : ℕ) (x y : L) : ((↑D - (a + b) • 1) ^ n) ⁅x, y⁆ = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • ⁅((↑D - a • 1) ^ ij.1) x, ((↑D - b • 1) ^ ij.2) y⁆

The twisted Leibniz rule: for a derivation D and scalars a, b, powers of D - (a + b) applied to a bracket expand binomially into powers of D - a and D - b applied to the two arguments. For a = b = 0 this is LieDerivation.iterate_apply_lie.

theorem LieDerivation.lie_mem_maxGenEigenspace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (D : LieDerivation R L L) {a b : R} {x y : L} (hx : x ∈ Module.End.maxGenEigenspace (↑D) a) (hy : y ∈ Module.End.maxGenEigenspace (↑D) b) : ⁅x, y⁆ ∈ Module.End.maxGenEigenspace (↑D) (a + b)

The bracket of a generalized a-eigenvector and a generalized b-eigenvector of a derivation is a generalized (a + b)-eigenvector.

theorem LieDerivation.apply_lie_eq_add_of_isNilpotent_sub {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (D : LieDerivation K L L) (hD : ⨆ (μ : K), Module.End.maxGenEigenspace (↑D) μ = ⊤) {S : Module.End K L} (hDS : Commute (↑D) S) (hS : S.IsFinitelySemisimple) (hN : IsNilpotent (↑D - S)) (x y : L) : S ⁅x, y⁆ = ⁅x, S y⁆ + ⁅S x, y⁆

Let D be a derivation whose generalized eigenspaces span. An endomorphism S commuting with D, finitely semisimple, and such that D - S is nilpotent, satisfies the Leibniz rule. Over a perfect field and in finite dimension, such an S is exactly the semisimple part of D, by uniqueness of the Jordan–Chevalley decomposition.

theorem LieDerivation.exists_isNilpotent_isSemisimple_of_iSup_maxGenEigenspace_eq_top {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] (D : LieDerivation K L L) (hD : ⨆ (μ : K), Module.End.maxGenEigenspace (↑D) μ = ⊤) : ∃ (N : LieDerivation K L L) (S : LieDerivation K L L), ↑N ∈ K[↑D] ∧ ↑S ∈ K[↑D] ∧ IsNilpotent ↑N ∧ Module.End.IsSemisimple ↑S ∧ D = N + S

Jordan–Chevalley decomposition of a split derivation. If the generalized eigenspaces of a derivation D of a finite-dimensional Lie algebra span, then the nilpotent and semisimple parts of D are derivations. They are polynomials in D. No perfectness of the field is needed: D is annihilated by a power of the separable polynomial whose simple roots are its eigenvalues.

theorem LieDerivation.exists_isNilpotent_isSemisimple {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [IsAlgClosed K] (D : LieDerivation K L L) : ∃ (N : LieDerivation K L L) (S : LieDerivation K L L), ↑N ∈ K[↑D] ∧ ↑S ∈ K[↑D] ∧ IsNilpotent ↑N ∧ Module.End.IsSemisimple ↑S ∧ D = N + S

Jordan–Chevalley decomposition of a derivation. Over an algebraically closed field, the nilpotent and semisimple parts of a derivation of a finite-dimensional Lie algebra are derivations. They are polynomials in the original derivation.