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.

TODO

• Uniqueness of decomposition (once we prove that the sum of commuting semisimple endomorphims is semisimple, this will follow from Module.End.eq_zero_of_isNilpotent_isSemisimple).

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 : Module.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 : Module.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.