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
@[simp]
theorem is_unit.coe_inv_sub_inv_smul {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {s : R} {a : A} (h : is_unit (r (algebra_map R A) s - a)) :
noncomputable def is_unit.sub_inv_smul {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {s : R} {a : A} (h : is_unit (r (algebra_map R A) s - a)) :

The unit 1 - r⁻¹ • a constructed from r • 1 - a when the latter is a unit.

Equations
@[simp]
theorem is_unit.coe_sub_inv_smul {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {s : R} {a : A} (h : is_unit (r (algebra_map R A) s - a)) :
theorem spectrum.mem_iff {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : R} {a : A} :
theorem spectrum.not_mem_iff {R : Type u} {A : Type v} [comm_semiring 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_semiring 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_semiring R] [ring A] [algebra R A] {r : R} {a : A} :
@[simp]
theorem spectrum.resolvent_set_of_subsingleton {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] [subsingleton A] (a : A) :
@[simp]
theorem spectrum.of_subsingleton {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] [subsingleton A] (a : A) :
theorem spectrum.resolvent_eq {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {a : A} {r : R} (h : r resolvent_set R a) :
theorem spectrum.units_smul_resolvent {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {s : R} {a : A} :
theorem spectrum.units_smul_resolvent_self {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {a : A} :
theorem spectrum.is_unit_resolvent {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : R} {a : A} :

The resolvent is a unit when the argument is in the resolvent set.

theorem spectrum.inv_mem_resolvent_set {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {a : Aˣ} (h : r resolvent_set R a) :
theorem spectrum.inv_mem_iff {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {a : Aˣ} :
theorem spectrum.zero_mem_resolvent_set_of_unit {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] (a : Aˣ) :
theorem spectrum.ne_zero_of_mem_of_unit {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {a : Aˣ} {r : R} (hr : r spectrum R a) :
r 0
theorem spectrum.add_mem_iff {R : Type u} {A : Type v} [comm_semiring 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_semiring 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_semiring R] [ring A] [algebra R A] (a : A) (r : Rˣ) :
spectrum R (r a) = r spectrum R a
theorem spectrum.unit_mem_mul_iff_mem_swap_mul {R : Type u} {A : Type v} [comm_semiring 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_semiring R] [ring A] [algebra R A] {a b : A} :
theorem spectrum.star_mem_resolvent_set_iff {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] [has_involutive_star R] [star_ring A] [star_module R A] {r : R} {a : A} :
@[protected]
theorem spectrum.map_star {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] [has_involutive_star R] [star_ring A] [star_module R A] (a : 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) :
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
@[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}
@[protected]
theorem spectrum.map_inv {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] (a : Aˣ) :
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.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.mem_resolvent_set_apply {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_ring R] [ring A] [algebra R A] [ring B] [algebra R B] [alg_hom_class F R A B] (φ : F) {a : A} {r : R} (h : r resolvent_set R a) :
theorem alg_hom.spectrum_apply_subset {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_ring R] [ring A] [algebra R A] [ring B] [algebra R B] [alg_hom_class F R A B] (φ : F) (a : A) :
spectrum R (φ a) spectrum R a
theorem alg_hom.apply_mem_spectrum {F : Type u_1} {R : Type u_2} {A : Type u_3} [comm_ring R] [ring A] [algebra R A] [alg_hom_class F R A R] [nontrivial R] (φ : F) (a : A) :
φ a spectrum R a