English
Let 𝕜 be algebraically closed, a an element of a 𝕜-algebra A, and p ∈ 𝕜[X] with deg p > 0. Then the spectrum of the evaluation of p at a, σ(aeval a p), equals the image of the spectrum of a under the polynomial evaluation map: σ(aeval a p) = { eval_x(p) : x ∈ σ(a) }. In particular, the eigenvalues of p(a) are obtained by applying p to the eigenvalues of a.
Русский
Пусть 𝕜 — алгебраически замкнутое поле, A — кольцо с алгеброй над 𝕜, a ∈ A и p ∈ 𝕜[X] с deg p > 0. Тогда спектр элемента aeval(a, p) равен образу спектра a при отображении x ↦ eval_x(p): σ(aeval(a, p)) = { eval_x(p) | x ∈ σ(a) }. Другими словами, собственные значения p(a) получаются путём применения p к собственным значениям a.
LaTeX
$$$$\\sigma\\big(\\mathrm{aeval}_a p\\big) \;=\; \\{ \\operatorname{eval}(x,p) \\;|\\; x \\in \\sigma(a) \\}. $$$$
Lean4
/-- The *spectral mapping theorem* for polynomials. Note: the assumption `degree p > 0`
is necessary in case `σ a = ∅`, for then the left-hand side is `∅` and the right-hand side,
assuming `[Nontrivial A]`, is `{k}` where `p = Polynomial.C k`. -/
theorem map_polynomial_aeval_of_degree_pos [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X]) (hdeg : 0 < degree p) :
σ (aeval a p) = (eval · p) '' σ a := by
-- handle the easy direction via `spectrum.subset_polynomial_aeval`
refine
Set.eq_of_subset_of_subset (fun k hk => ?_)
(subset_polynomial_aeval a p)
-- write `C k - p` product of linear factors and a constant; show `C k - p ≠ 0`.
have hprod := eq_prod_roots_of_splits_id (IsAlgClosed.splits (C k - p))
have h_ne : C k - p ≠ 0 :=
ne_zero_of_degree_gt <| by rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)]
have lead_ne := leadingCoeff_ne_zero.mpr h_ne
have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).isUnit
have p_a_eq : aeval a (C k - p) = ↑ₐ k - aeval a p := by simp only [aeval_C, map_sub]
rw [mem_iff, ← p_a_eq, hprod, aeval_mul, ((Commute.all _ _).map (aeval a : 𝕜[X] →ₐ[𝕜] A)).isUnit_mul_iff,
aeval_C] at hk
replace hk := exists_mem_of_not_isUnit_aeval_prod (not_and.mp hk lead_unit)
rcases hk with ⟨r, r_mem, r_ev⟩
exact ⟨r, r_mem, symm (by simpa [eval_sub, eval_C, sub_eq_zero] using r_ev)⟩
