Jordan-Chevalley-Dunford decomposition

Given a finite-dimensional linear endomorphism f, the Jordan-Chevalley-Dunford theorem provides a sufficient condition for there to exist a nilpotent endomorphism n and a semisimple endomorphism s, such that f = n + s and both n and s are polynomial expressions in f.

The condition is that there exists a separable polynomial P such that the endomorphism P(f) is nilpotent. This condition is always satisfied when the coefficients are a perfect field.

The proof given here uses Newton's method and is taken from Chambert-Loir's notes: Algebre

Main definitions / results:

• Module.End.exists_isNilpotent_isSemisimple: an endomorphism of a finite-dimensional vector space over a perfect field may be written as a sum of nilpotent and semisimple endomorphisms. Moreover these nilpotent and semisimple components are polynomial expressions in the original endomorphism.
• Module.End.isNilpotent_isSemisimple_unique: the Jordan-Chevalley-Dunford decomposition is unique: if f = n₁ + s₁ = n₂ + s₂ with nᵢ nilpotent, sᵢ semisimple, and nᵢ, sᵢ commuting, then n₁ = n₂ and s₁ = s₂.

theorem Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : End K V} {P : Polynomial K} {k : ℕ} (sep : P.Separable) (nil : minpoly K f ∣ P ^ k) : ∃ n ∈ Algebra.adjoin K {f}, ∃ s ∈ Algebra.adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

theorem Module.End.exists_isNilpotent_isSemisimple {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : End K V} [FiniteDimensional K V] [PerfectField K] : ∃ n ∈ Algebra.adjoin K {f}, ∃ s ∈ Algebra.adjoin K {f}, IsNilpotent n ∧ s.IsSemisimple ∧ f = n + s

Jordan-Chevalley-Dunford decomposition: an endomorphism of a finite-dimensional vector space over a perfect field may be written as a sum of nilpotent and semisimple endomorphisms. Moreover these nilpotent and semisimple components are polynomial expressions in the original endomorphism.

theorem Module.End.isNilpotent_isSemisimple_unique {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {f : End K V} [FiniteDimensional K V] [PerfectField K] {n₁ s₁ n₂ s₂ : End K V} (hn₁ : IsNilpotent n₁) (hs₁ : s₁.IsSemisimple) (hn₂ : IsNilpotent n₂) (hs₂ : s₂.IsSemisimple) (hc₁ : Commute n₁ s₁) (hc₂ : Commute n₂ s₂) (h₁ : f = n₁ + s₁) (h₂ : f = n₂ + s₂) : n₁ = n₂ ∧ s₁ = s₂

Uniqueness of Jordan-Chevalley-Dunford decomposition: if f = n₁ + s₁ = n₂ + s₂ with nᵢ nilpotent, sᵢ semisimple, and nᵢ, sᵢ commuting, then n₁ = n₂ and s₁ = s₂.