mathlib documentation

algebra.algebra.spectrum

Spectrum of an element in an algebra #

This file develops the basic theory of the spectrum of an element of an algebra. This theory will serve as the foundation for spectral theory in Banach algebras.

Main definitions #

Main statements #

Notations #

def resolvent_set (R : Type u) {A : Type v} [comm_semiring R] [ring A] [algebra R A] (a : A) :
set R

Given a commutative ring R and an R-algebra A, the resolvent set of a : A is the set R consisting of those r : R for which r•1 - a is a unit of the algebra A.

Equations
def spectrum (R : Type u) {A : Type v} [comm_semiring R] [ring A] [algebra R A] (a : A) :
set R

Given a commutative ring R and an R-algebra A, the spectrum of a : A is the set R consisting of those r : R for which r•1 - a is not a unit of the algebra A.

The spectrum is simply the complement of the resolvent set.

Equations
noncomputable def resolvent {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] (a : A) (r : R) :
A

Given an a : A where A is an R-algebra, the resolvent is a map R → A which sends r : R to (algebra_map R A r - a)⁻¹ when r ∈ resolvent R A and 0 when r ∈ spectrum R A.

Equations
theorem is_unit.smul_sub_iff_sub_inv_smul {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : Rˣ} {a : A} :
is_unit (r 1 - a) is_unit (1 - r⁻¹ a)
theorem spectrum.mem_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : R} {a : A} :
theorem spectrum.not_mem_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : R} {a : A} :
theorem spectrum.mem_resolvent_set_of_left_right_inverse {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : R} {a b c : A} (h₁ : ((algebra_map R A) r - a) * b = 1) (h₂ : c * ((algebra_map R A) r - a) = 1) :
theorem spectrum.mem_resolvent_set_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {r : R} {a : A} :
theorem spectrum.resolvent_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {a : A} {r : R} (h : r resolvent_set R a) :
theorem spectrum.add_mem_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {a : A} {r s : R} :
r spectrum R a r + s spectrum R ((algebra_map R A) s + a)
theorem spectrum.smul_mem_smul_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {a : A} {s : R} {r : Rˣ} :
r s spectrum R (r a) s spectrum R a
theorem spectrum.unit_smul_eq_smul {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (a : A) (r : Rˣ) :
spectrum R (r a) = r spectrum R a
theorem spectrum.left_add_coset_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (a : A) (r : R) :
r +l spectrum R a = spectrum R ((algebra_map R A) r + a)
theorem spectrum.unit_mem_mul_iff_mem_swap_mul {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {a b : A} {r : Rˣ} :
r spectrum R (a * b) r spectrum R (b * a)
theorem spectrum.preimage_units_mul_eq_swap_mul {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {a b : A} :
@[simp]
theorem spectrum.zero_eq {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [nontrivial A] :
spectrum 𝕜 0 = {0}

Without the assumption nontrivial A, then 0 : A would be invertible.

@[simp]
theorem spectrum.scalar_eq {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [nontrivial A] (k : 𝕜) :
spectrum 𝕜 ((algebra_map 𝕜 A) k) = {k}
@[simp]
theorem spectrum.one_eq {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [nontrivial A] :
spectrum 𝕜 1 = {1}
theorem spectrum.smul_eq_smul {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [nontrivial A] (k : 𝕜) (a : A) (ha : (spectrum 𝕜 a).nonempty) :
spectrum 𝕜 (k a) = k spectrum 𝕜 a

the assumption (σ a).nonempty is necessary and cannot be removed without further conditions on the algebra A and scalar field 𝕜.

theorem spectrum.nonzero_mul_eq_swap_mul {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] (a b : A) :
spectrum 𝕜 (a * b) \ {0} = spectrum 𝕜 (b * a) \ {0}
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.

theorem spectrum.exists_mem_of_not_is_unit_aeval_prod {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] {p : polynomial 𝕜} {a : A} (hp : p 0) (h : ¬is_unit ((polynomial.aeval a) (multiset.map (λ (x : 𝕜), polynomial.X - polynomial.C x) p.roots).prod)) :
∃ (k : 𝕜), k spectrum 𝕜 a polynomial.eval k p = 0
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.

theorem spectrum.map_polynomial_aeval_of_nonempty {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [is_alg_closed 𝕜] [nontrivial A] (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. Note: the assumption [nontrivial A] is necessary for the same reason as in spectrum.zero_eq.

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

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

theorem alg_hom.apply_mem_spectrum {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] [nontrivial R] (φ : A →ₐ[R] R) (a : A) :
φ a spectrum R a