English
Half of the spectral mapping theorem for polynomials: the image under evaluation is contained in the spectrum of the aeval polynomial.
Русский
Половина спектральной отображения: образ под
определения аeval содержит спектр полинома.
LaTeX
$$$(eval \cdot p)'' \sigma a \subseteq \sigma (aeval a p)$$$
Lean4
/-- Half of the spectral mapping theorem for polynomials. We prove it separately
because it holds over any field, whereas `spectrum.map_polynomial_aeval_of_degree_pos` and
`spectrum.map_polynomial_aeval_of_nonempty` need the field to be algebraically closed. -/
theorem subset_polynomial_aeval (a : A) (p : 𝕜[X]) : (eval · p) '' σ a ⊆ σ (aeval a p) :=
by
rintro _ ⟨k, hk, rfl⟩
let q := C (eval k p) - p
have hroot : IsRoot q k := by simp only [q, eval_C, eval_sub, sub_self, IsRoot.def]
rw [← mul_div_eq_iff_isRoot, ← neg_mul_neg, neg_sub] at hroot
have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by simp only [q, aeval_C, map_sub]
rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a : 𝕜[X] →ₐ[𝕜] A)
apply mt fun h => (hcomm.isUnit_mul_iff.mp h).1
simpa only [aeval_X, aeval_C, map_sub] using hk
