English
In a finite-dimensional setting over a perfect field, every endomorphism has a decomposition into a nilpotent and a semisimple part that are polynomials in the endomorphism.
Русский
В конечномерном случае над идеальным полем любое преобразование можно разложить на нильпотентную и полусемисимплитную части, каждая из которых выражается полиномами от самого преобразования.
LaTeX
$$$$\\exists n,s\\in \\operatorname{ad}_K\\{f\\},\\; \\mathrm{IsNilpotent}(n) \\wedge \\mathrm{IsSemisimple}(s) \\wedge f = n + s.$$$$
Lean4
/-- **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 exists_isNilpotent_isSemisimple [PerfectField K] :
∃ᵉ (n ∈ adjoin K { f }) (s ∈ adjoin K { f }), IsNilpotent n ∧ IsSemisimple s ∧ f = n + s :=
by
obtain ⟨g, k, sep, -, nil⟩ := exists_squarefree_dvd_pow_of_ne_zero (minpoly.ne_zero_of_finite K f)
rw [← PerfectField.separable_iff_squarefree] at sep
exact exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow sep nil
