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 #

resolvent_set a : set R: the resolvent set of an element a : A where A is an R-algebra.
spectrum a : set R: the spectrum of an element a : A where A is an R-algebra.
resolvent : R → A: the resolvent function is λ r, ring.inverse (↑ₐr - a), and hence when r ∈ resolvent R A, it is actually the inverse of the unit (↑ₐr - a).

Main statements #

spectrum.unit_smul_eq_smul and spectrum.smul_eq_smul: units in the scalar ring commute (multiplication) with the spectrum, and over a field even 0 commutes with the spectrum.
spectrum.left_add_coset_eq: elements of the scalar ring commute (addition) with the spectrum.
spectrum.unit_mem_mul_iff_mem_swap_mul and spectrum.preimage_units_mul_eq_swap_mul: the units (of R) in σ (a*b) coincide with those in σ (b*a).
spectrum.scalar_eq: in a nontrivial algebra over a field, the spectrum of a scalar is a singleton.
spectrum.subset_polynomial_aeval, spectrum.map_polynomial_aeval_of_degree_pos, spectrum.map_polynomial_aeval_of_nonempty: variations on the spectral mapping theorem.

Notations #

σ a : spectrum R a of a : A

source

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

resolvent_set R a = {r : R | is_unit (⇑(algebra_map R A) r - a)}

source

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

spectrum R a = (resolvent_set R a)ᶜ

source

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

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

resolvent a r = ring.inverse (⇑(algebra_map R A) r - a)

source

@[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)) :

↑(h.sub_inv_smul)⁻¹ = r • ↑(h.unit)⁻¹

source

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)) :

Aˣ

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

Equations

h.sub_inv_smul = {val := ⇑(algebra_map R A) s - r⁻¹ • a, inv := r • ↑(h.unit)⁻¹, val_inv := _, inv_val := _}

source

@[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)) :

↑(h.sub_inv_smul) = ⇑(algebra_map R A) s - r⁻¹ • a

source

theorem spectrum.mem_iff {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : R} {a : A} :

r ∈ spectrum R a ↔ ¬is_unit (⇑(algebra_map R A) r - a)

source

theorem spectrum.not_mem_iff {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : R} {a : A} :

r ∉ spectrum R a ↔ is_unit (⇑(algebra_map R A) r - a)

source

theorem spectrum.zero_mem_iff (R : Type u) {A : Type v} [comm_semiring R] [ring A] [algebra R A] {a : A} :

0 ∈ spectrum R a ↔ ¬is_unit a

source

theorem spectrum.zero_not_mem_iff (R : Type u) {A : Type v} [comm_semiring R] [ring A] [algebra R A] {a : A} :

0 ∉ spectrum R a ↔ is_unit a

source

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) :

r ∈ resolvent_set R a

source

theorem spectrum.mem_resolvent_set_iff {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : R} {a : A} :

r ∈ resolvent_set R a ↔ is_unit (⇑(algebra_map R A) r - a)

source

@[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) :

resolvent_set R a = set.univ

source

@[simp]

theorem spectrum.of_subsingleton {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] [subsingleton A] (a : A) :

spectrum R a = ∅

source

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) :

resolvent a r = ↑(is_unit.unit h)⁻¹

source

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} :

r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

source

theorem spectrum.units_smul_resolvent_self {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {a : A} :

r • resolvent a ↑r = resolvent (r⁻¹ • a) 1

source

theorem spectrum.is_unit_resolvent {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : R} {a : A} :

r ∈ resolvent_set R a ↔ is_unit (resolvent a r)

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

source

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) :

↑r⁻¹ ∈ resolvent_set R ↑a⁻¹

source

theorem spectrum.inv_mem_iff {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {r : Rˣ} {a : Aˣ} :

↑r ∈ spectrum R ↑a ↔ ↑r⁻¹ ∈ spectrum R ↑a⁻¹

source

theorem spectrum.zero_mem_resolvent_set_of_unit {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] (a : Aˣ) :

0 ∈ resolvent_set R ↑a

source

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

source

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 + s ∈ spectrum R a ↔ r ∈ spectrum R (-⇑(algebra_map R A) s + a)

source

theorem spectrum.add_mem_add_iff {R : Type u} {A : Type v} [comm_semiring R] [ring A] [algebra R A] {a : A} {r s : R} :

r + s ∈ spectrum R (⇑(algebra_map R A) s + a) ↔ r ∈ spectrum R a

source

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

source

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

source

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)

source

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} :

coe ⁻¹' spectrum R (a * b) = coe ⁻¹' spectrum R (b * a)

source

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} :

has_star.star r ∈ resolvent_set R a ↔ r ∈ resolvent_set R (has_star.star a)

source

@[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) :

spectrum R (has_star.star a) = has_star.star (spectrum R a)

source

theorem spectrum.subset_subalgebra {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] {S : subalgebra R A} (a : ↥S) :

spectrum R ↑a ⊆ spectrum R a

source

theorem spectrum.subset_star_subalgebra {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] [star_ring R] [star_ring A] [star_module R A] {S : star_subalgebra R A} (a : ↥S) :

spectrum R ↑a ⊆ spectrum R a

source

theorem spectrum.singleton_add_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (a : A) (r : R) :

{r} + spectrum R a = spectrum R (⇑(algebra_map R A) r + a)

source

theorem spectrum.add_singleton_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (a : A) (r : R) :

spectrum R a + {r} = spectrum R (a + ⇑(algebra_map R A) r)

source

theorem spectrum.vadd_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (a : A) (r : R) :

r +ᵥ spectrum R a = spectrum R (⇑(algebra_map R A) r + a)

source

theorem spectrum.neg_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (a : A) :

-spectrum R a = spectrum R (-a)

source

theorem spectrum.singleton_sub_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (a : A) (r : R) :

{r} - spectrum R a = spectrum R (⇑(algebra_map R A) r - a)

source

theorem spectrum.sub_singleton_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (a : A) (r : R) :

spectrum R a - {r} = spectrum R (a - ⇑(algebra_map R A) r)

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

@[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.

source

@[simp]

theorem spectrum.scalar_eq {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [nontrivial A] (k : 𝕜) :

spectrum 𝕜 (⇑(algebra_map 𝕜 A) k) = {k}

source

@[simp]

theorem spectrum.one_eq {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] [nontrivial A] :

spectrum 𝕜 1 = {1}

source

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

source

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}

source

@[protected]

theorem spectrum.map_inv {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [algebra 𝕜 A] (a : Aˣ) :

(spectrum 𝕜 ↑a)⁻¹ = spectrum 𝕜 ↑a⁻¹

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) :

∃ (k : 𝕜), k ∈ spectrum 𝕜 a

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

source

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) :

r ∈ resolvent_set R (⇑φ a)

source

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

source

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