English
Let 𝕜 be algebraically closed, a ∈ A, p ∈ 𝕜[X], and assume the spectrum σ(a) is nonempty. Then σ(aeval a p) equals the image of σ(a) under x ↦ eval_x(p): σ(aeval a p) = { eval_x(p) : x ∈ σ(a) }. (The same spectral mapping holds under the nonempty spectrum hypothesis.)
Русский
Пусть 𝕜 — алгебраически замкнутое поле, A — кольцо с алгеброй над 𝕜, a ∈ A, p ∈ 𝕜[X], и предположим, что спектр σ(a) не пуст. Тогда σ(aeval(a, p)) = { eval_x(p) : x ∈ σ(a) }. Повторяется та же самая карта спектра при непустом спектре.
LaTeX
$$$$ (\\sigma a).Nonempty \\Rightarrow \\sigma\\big(\\mathrm{aeval}_a p\\big) \;=\; \\{ \\operatorname{eval}(x,p) \\;|\\; x \\in \\sigma(a) \\}. $$$$
Lean4
/-- In this version of the spectral mapping theorem, we assume the spectrum
is nonempty instead of assuming the degree of the polynomial is positive. -/
theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X]) (hnon : (σ a).Nonempty) :
σ (aeval a p) = (fun k => eval k p) '' σ a := by
nontriviality A
refine Or.elim (le_or_gt (degree p) 0) (fun h => ?_) (map_polynomial_aeval_of_degree_pos a p)
rw [eq_C_of_degree_le_zero h]
simp only [eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]
