# Spectrum mapping theorem #

This file develops proves the spectral mapping theorem for polynomials over algebraically closed fields. In particular, if `a` is an element of a `𝕜`-algebra `A` where `𝕜` is a field, and `p : 𝕜[X]` is a polynomial, then the spectrum of `Polynomial.aeval a p` contains the image of the spectrum of `a` under `(fun k ↦ Polynomial.eval k p)`. When `𝕜` is algebraically closed, these are in fact equal (assuming either that the spectrum of `a` is nonempty or the polynomial has positive degree), which is the spectral mapping theorem.

In addition, this file contains the fact that every element of a finite-dimensional nontrivial algebra over an algebraically closed field has nonempty spectrum. In particular, this is used in `Module.End.exists_eigenvalue` to show that every linear map from a vector space to itself has an eigenvalue.

## Main statements #

- `spectrum.subset_polynomial_aeval`, `spectrum.map_polynomial_aeval_of_degree_pos`, `spectrum.map_polynomial_aeval_of_nonempty`: variations on the spectral mapping theorem.
- `spectrum.nonempty_of_isAlgClosed_of_finiteDimensional`: the spectrum is nonempty for any element of a nontrivial finite-dimensional algebra over an algebraically closed field.

## Notation #

- `σ a` : `spectrum R a` of `a : A`

source
theorem spectrum.exists_mem_of_not_isUnit_aeval_prod {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [IsDomain R] {p : Polynomial R} {a : A} (h : ¬IsUnit ((Polynomial.aeval a) (Multiset.map (fun (x : R) => Polynomial.X - Polynomial.C x) p.roots).prod)) :
∃ k ∈ spectrum R a, Polynomial.eval k p = 0
source
theorem spectrum.subset_polynomial_aeval {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) (p : Polynomial 𝕜) :
(fun (x : 𝕜) => Polynomial.eval x p) '' spectrum 𝕜 a ⊆ spectrum 𝕜 ((Polynomial.aeval a) p)

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.

source
theorem spectrum.map_polynomial_aeval_of_degree_pos {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) (p : Polynomial 𝕜) (hdeg : 0 < p.degree) :
spectrum 𝕜 ((Polynomial.aeval a) p) = (fun (x : 𝕜) => Polynomial.eval x p) '' spectrum 𝕜 a

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`.

source
theorem spectrum.map_polynomial_aeval_of_nonempty {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) (p : Polynomial 𝕜) (hnon : (spectrum 𝕜 a).Nonempty) :
spectrum 𝕜 ((Polynomial.aeval a) p) = (fun (k : 𝕜) => Polynomial.eval k p) '' spectrum 𝕜 a

In this version of the spectral mapping theorem, we assume the spectrum is nonempty instead of assuming the degree of the polynomial is positive.

source
theorem spectrum.pow_image_subset {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) (n : ℕ) :
(fun (x : 𝕜) => x ^ n) '' spectrum 𝕜 a ⊆ spectrum 𝕜 (a ^ n)

A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience.

source
theorem spectrum.pow_mem_pow {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] (a : A) (n : ℕ) {k : 𝕜} (hk : k ∈ spectrum 𝕜 a) :
k ^ n ∈ spectrum 𝕜 (a ^ n)
source
theorem spectrum.map_pow_of_pos {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) :
spectrum 𝕜 (a ^ n) = (fun (x : 𝕜) => x ^ n) '' spectrum 𝕜 a

A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for convenience.

source
theorem spectrum.map_pow_of_nonempty {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] {a : A} (ha : (spectrum 𝕜 a).Nonempty) (n : ℕ) :
spectrum 𝕜 (a ^ n) = (fun (x : 𝕜) => x ^ n) '' spectrum 𝕜 a

A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for convenience.

source
theorem spectrum.nonempty_of_isAlgClosed_of_finiteDimensional (𝕜 : Type u) {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 A] [IsAlgClosed 𝕜] [Nontrivial A] [I : FiniteDimensional 𝕜 A] (a : A) :
(spectrum 𝕜 a).Nonempty

Every element `a` in a nontrivial finite-dimensional algebra `A` over an algebraically closed field `𝕜` has non-empty spectrum.

source
theorem IsIdempotentElem.spectrum_subset (𝕜 : Type u_1) {A : Type u_2} [Field 𝕜] [Ring A] [Algebra 𝕜 A] {p : A} (hp : IsIdempotentElem p) :
spectrum 𝕜 p ⊆ {0, 1}
source
theorem IsIdempotentElem.quasispectrum_subset {𝕜 : Type u_1} {A : Type u_2} [Field 𝕜] [NonUnitalRing A] [Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {p : A} (hp : IsIdempotentElem p) :
quasispectrum 𝕜 p ⊆ {0, 1}