Spectrum of an element in an algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.

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

@[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 alg_hom.mem_resolvent_set_apply {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [comm_semiring 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_semiring 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