Documentation

Mathlib.LinearAlgebra.JordanChevalley

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: #

TODO #

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) :
nAlgebra.adjoin K {f}, sAlgebra.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] :
nAlgebra.adjoin K {f}, sAlgebra.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.