# 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} [] [] [Module K V] {f : } {P : } {k : } (sep : P.Separable) (nil : minpoly K f P ^ k) :
nAlgebra.adjoin K {f}, sAlgebra.adjoin K {f}, s.IsSemisimple f = n + s
theorem Module.End.exists_isNilpotent_isSemisimple {K : Type u_1} {V : Type u_2} [] [] [Module K V] [] {f : } [] :
nAlgebra.adjoin K {f}, sAlgebra.adjoin K {f}, 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.