# 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 #

• resolventSet 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 fun 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
def resolventSet (R : Type u) {A : Type v} [] [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
Instances For
def spectrum (R : Type u) {A : Type v} [] [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
Instances For
noncomputable def resolvent {R : Type u} {A : Type v} [] [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 (algebraMap R A r - a)⁻¹ when r ∈ resolvent R A and 0 when r ∈ spectrum R A.

Equations
Instances For
@[simp]
theorem IsUnit.val_subInvSMul {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r () s - a)) :
h.subInvSMul = () s - r⁻¹ a
@[simp]
theorem IsUnit.val_inv_subInvSMul {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r () s - a)) :
h.subInvSMul⁻¹ = r h.unit⁻¹
noncomputable def IsUnit.subInvSMul {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r () s - a)) :

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

Equations
• h.subInvSMul = { val := () s - r⁻¹ a, inv := r h.unit⁻¹, val_inv := , inv_val := }
Instances For
theorem spectrum.mem_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : R} {a : A} :
r spectrum R a ¬IsUnit (() r - a)
theorem spectrum.not_mem_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : R} {a : A} :
rspectrum R a IsUnit (() r - a)
theorem spectrum.zero_mem_iff (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] {a : A} :
theorem spectrum.not_isUnit_of_zero_mem (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] {a : A} :
0 spectrum R a¬

Alias of the forward direction of spectrum.zero_mem_iff.

theorem spectrum.zero_mem (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] {a : A} :
¬0 spectrum R a

Alias of the reverse direction of spectrum.zero_mem_iff.

theorem spectrum.zero_not_mem_iff (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] {a : A} :
0spectrum R a
theorem spectrum.zero_not_mem (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] {a : A} :
0spectrum R a

Alias of the reverse direction of spectrum.zero_not_mem_iff.

theorem spectrum.isUnit_of_zero_not_mem (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] {a : A} :
0spectrum R a

Alias of the forward direction of spectrum.zero_not_mem_iff.

theorem spectrum.subset_singleton_zero_compl (R : Type u) {A : Type v} [] [Ring A] [Algebra R A] {a : A} (ha : ) :
theorem spectrum.mem_resolventSet_of_left_right_inverse {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : R} {a : A} {b : A} {c : A} (h₁ : (() r - a) * b = 1) (h₂ : c * (() r - a) = 1) :
r
theorem spectrum.mem_resolventSet_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : R} {a : A} :
r IsUnit (() r - a)
@[simp]
theorem spectrum.algebraMap_mem_iff (S : Type u_1) {R : Type u_2} {A : Type u_3} [] [] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [] {a : A} {r : R} :
() r spectrum S a r spectrum R a
theorem spectrum.of_algebraMap_mem (S : Type u_1) {R : Type u_2} {A : Type u_3} [] [] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [] {a : A} {r : R} :
() r spectrum S ar spectrum R a

Alias of the forward direction of spectrum.algebraMap_mem_iff.

theorem spectrum.algebraMap_mem (S : Type u_1) {R : Type u_2} {A : Type u_3} [] [] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [] {a : A} {r : R} :
r spectrum R a() r spectrum S a

Alias of the reverse direction of spectrum.algebraMap_mem_iff.

@[simp]
theorem spectrum.preimage_algebraMap (S : Type u_1) {R : Type u_2} {A : Type u_3} [] [] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [] {a : A} :
() ⁻¹' spectrum S a = spectrum R a
@[simp]
theorem spectrum.resolventSet_of_subsingleton {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] (a : A) :
= Set.univ
@[simp]
theorem spectrum.of_subsingleton {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] (a : A) :
theorem spectrum.resolvent_eq {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {a : A} {r : R} (h : r ) :
= ()⁻¹
theorem spectrum.units_smul_resolvent {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} :
theorem spectrum.units_smul_resolvent_self {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : Rˣ} {a : A} :
r resolvent a r = resolvent (r⁻¹ a) 1
theorem spectrum.isUnit_resolvent {R : Type u} {A : Type v} [] [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_resolventSet {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : Rˣ} {a : Aˣ} (h : r resolventSet R a) :
r⁻¹
theorem spectrum.inv_mem_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {r : Rˣ} {a : Aˣ} :
r spectrum R a r⁻¹ spectrum R a⁻¹
theorem spectrum.zero_mem_resolventSet_of_unit {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (a : Aˣ) :
0 resolventSet R a
theorem spectrum.ne_zero_of_mem_of_unit {R : Type u} {A : Type v} [] [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} [] [Ring A] [Algebra R A] {a : A} {r : R} {s : R} :
r + s spectrum R a r spectrum R (-() s + a)
theorem spectrum.add_mem_add_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {a : A} {r : R} {s : R} :
r + s spectrum R (() s + a) r spectrum R a
theorem spectrum.smul_mem_smul_iff {R : Type u} {A : Type v} [] [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} [] [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} [] [Ring A] [Algebra R A] {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} [] [Ring A] [Algebra R A] {a : A} {b : A} :
Units.val ⁻¹' spectrum R (a * b) = Units.val ⁻¹' spectrum R (b * a)
theorem spectrum.star_mem_resolventSet_iff {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] [] [] {r : R} {a : A} :
theorem spectrum.map_star {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] [] [] (a : A) :
theorem spectrum.subset_subalgebra {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] {S : } (a : S) :
spectrum R a spectrum R a
theorem spectrum.subset_starSubalgebra {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] [] [] [] {S : } (a : S) :
spectrum R a spectrum R a
theorem spectrum.singleton_add_eq {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (a : A) (r : R) :
{r} + spectrum R a = spectrum R (() r + a)
theorem spectrum.add_singleton_eq {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (a : A) (r : R) :
spectrum R a + {r} = spectrum R (a + () r)
theorem spectrum.vadd_eq {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (a : A) (r : R) :
r +ᵥ spectrum R a = spectrum R (() r + a)
theorem spectrum.neg_eq {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (a : A) :
theorem spectrum.singleton_sub_eq {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (a : A) (r : R) :
{r} - spectrum R a = spectrum R (() r - a)
theorem spectrum.sub_singleton_eq {R : Type u} {A : Type v} [] [Ring A] [Algebra R A] (a : A) (r : R) :
spectrum R a - {r} = spectrum R (a - () r)
@[simp]
theorem spectrum.zero_eq {𝕜 : Type u} {A : Type v} [] [Ring A] [Algebra 𝕜 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} [] [Ring A] [Algebra 𝕜 A] [] (k : 𝕜) :
spectrum 𝕜 (() k) = {k}
@[simp]
theorem spectrum.one_eq {𝕜 : Type u} {A : Type v} [] [Ring A] [Algebra 𝕜 A] [] :
spectrum 𝕜 1 = {1}
theorem spectrum.smul_eq_smul {𝕜 : Type u} {A : Type v} [] [Ring A] [Algebra 𝕜 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} [] [Ring A] [Algebra 𝕜 A] (a : A) (b : A) :
spectrum 𝕜 (a * b) \ {0} = spectrum 𝕜 (b * a) \ {0}
theorem spectrum.map_inv {𝕜 : Type u} {A : Type v} [] [Ring A] [Algebra 𝕜 A] (a : Aˣ) :
(spectrum 𝕜 a)⁻¹ = spectrum 𝕜 a⁻¹
theorem AlgHom.mem_resolventSet_apply {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] (φ : F) {a : A} {r : R} (h : r ) :
r resolventSet R (φ a)
theorem AlgHom.spectrum_apply_subset {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [] [Ring A] [Algebra R A] [Ring B] [Algebra R B] [FunLike F A B] [AlgHomClass F R A B] (φ : F) (a : A) :
spectrum R (φ a) spectrum R a
theorem AlgHom.apply_mem_spectrum {F : Type u_1} {R : Type u_2} {A : Type u_3} [] [Ring A] [Algebra R A] [FunLike F A R] [AlgHomClass F R A R] [] (φ : F) (a : A) :
φ a spectrum R a
@[simp]
theorem AlgEquiv.spectrum_eq {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [] [Ring A] [Ring B] [Algebra R A] [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) (a : A) :
spectrum R (f a) = spectrum R a