English
If x is almost a root of P in the sense that aeval x P is nilpotent and aeval x (derivative P) is a unit, then there exists a unique r with x − r nilpotent and aeval r P = 0.
Русский
Если x почти является корнем P, то есть aeval x P нильпотентен и aeval x (derivative P) единица, существует единственный элемент r в S такой, что x−r нильпотентен и aeval r P = 0.
LaTeX
$$$$\exists! r\in S\quad (\operatorname{IsNilpotent}(x-r) \land aeval\,r\,P = 0).$$$$
Lean4
/-- If `x` is almost a root of `P` in the sense that `P(x)` is nilpotent (and `P'(x)` is a
unit) then we may write `x` as a sum `x = n + r` where `n` is nilpotent and `r` is a root of `P`.
Moreover, `n` and `r` are unique.
This can be used to prove the Jordan-Chevalley decomposition of linear endomorphims. -/
theorem existsUnique_nilpotent_sub_and_aeval_eq_zero (h : IsNilpotent (aeval x P))
(h' : IsUnit (aeval x <| derivative P)) : ∃! r, IsNilpotent (x - r) ∧ aeval r P = 0 :=
by
simp_rw [(neg_sub _ x).symm, isNilpotent_neg_iff]
refine existsUnique_of_exists_of_unique ?_ fun r₁ r₂ ⟨hr₁, hr₁'⟩ ⟨hr₂, hr₂'⟩ ↦ ?_
· -- Existence
obtain ⟨n, hn⟩ := id h
refine ⟨P.newtonMap^[n] x, isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n, ?_⟩
rw [← zero_dvd_iff, ← pow_eq_zero_of_le (n.lt_two_pow_self).le hn]
exact aeval_pow_two_pow_dvd_aeval_iterate_newtonMap h h' n
· -- Uniqueness
have ⟨u, hu⟩ := binomExpansion (P.map (algebraMap R S)) r₁ (r₂ - r₁)
suffices IsUnit (aeval r₁ (derivative P) + u * (r₂ - r₁)) by
rwa [derivative_map, eval_map_algebraMap, eval_map_algebraMap, eval_map_algebraMap, add_sub_cancel, hr₂', hr₁',
zero_add, pow_two, ← mul_assoc, ← add_mul, eq_comm, this.mul_right_eq_zero, sub_eq_zero, eq_comm] at hu
have : IsUnit (aeval r₁ (derivative P)) := isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' hr₁
rw [← sub_sub_sub_cancel_right r₂ r₁ x]
refine IsNilpotent.isUnit_add_left_of_commute ?_ this (Commute.all _ _)
exact (Commute.all _ _).isNilpotent_mul_left <| (Commute.all _ _).isNilpotent_sub hr₂ hr₁
