Spectrum mapping theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file develops proves the spectral mapping theorem for polynomials over algebraically closed fields. In particular, if a is an element of an 𝕜-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 (λ 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_is_alg_closed_of_finite_dimensional: the spectrum is nonempty for any element of a nontrivial finite dimensional algebra over an algebraically closed field.

Notations #

σ a : spectrum R a of a : A

source

theorem spectrum.exists_mem_of_not_is_unit_aeval_prod {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [is_domain R] {p : polynomial R} {a : A} (hp : p ≠ 0) (h : ¬is_unit (⇑(polynomial.aeval a) (multiset.map (λ (x : R), polynomial.X - ⇑polynomial.C x) p.roots).prod)) :

∃ (k : R), 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 𝕜) :

(λ (k : 𝕜), polynomial.eval k 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] [is_alg_closed 𝕜] (a : A) (p : polynomial 𝕜) (hdeg : 0 < p.degree) :

spectrum 𝕜 (⇑(polynomial.aeval a) p) = (λ (k : 𝕜), polynomial.eval k 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] [is_alg_closed 𝕜] (a : A) (p : polynomial 𝕜) (hnon : (spectrum 𝕜 a).nonempty) :

spectrum 𝕜 (⇑(polynomial.aeval a) p) = (λ (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 : ℕ) :

(λ (x : 𝕜), x ^ n) '' spectrum 𝕜 a ⊆ spectrum 𝕜 (a ^ n)

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

source

theorem spectrum.map_pow_of_pos {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [is_alg_closed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) :

spectrum 𝕜 (a ^ n) = (λ (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] [is_alg_closed 𝕜] {a : A} (ha : (spectrum 𝕜 a).nonempty) (n : ℕ) :

spectrum 𝕜 (a ^ n) = (λ (x : 𝕜), x ^ n) '' spectrum 𝕜 a

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

source

theorem spectrum.nonempty_of_is_alg_closed_of_finite_dimensional (𝕜 : Type u) {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [is_alg_closed 𝕜] [nontrivial A] [I : finite_dimensional 𝕜 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.