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} [CommSemiring 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

• resolventSet R a = {r : R | IsUnit ((algebraMap R A) r - a)}

def spectrum (R : Type u) {A : Type v} [CommSemiring 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 = (resolventSet R a)ᶜ

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

Equations

• resolvent a r = Ring.inverse ((algebraMap R A) r - a)

@[simp]

theorem IsUnit.val_subInvSMul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r • (algebraMap R A) s - a)) : ↑h.subInvSMul = (algebraMap R A) s - r⁻¹ • a

@[simp]

theorem IsUnit.val_inv_subInvSMul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r • (algebraMap R A) s - a)) : ↑h.subInvSMul⁻¹ = r • ↑h.unit⁻¹

noncomputable def IsUnit.subInvSMul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} (h : IsUnit (r • (algebraMap R A) s - a)) : Aˣ

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

Equations

• h.subInvSMul = { val := (algebraMap R A) s - r⁻¹ • a, inv := r • ↑h.unit⁻¹, val_inv := ⋯, inv_val := ⋯ }

theorem spectrum.mem_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} : r ∈ spectrum R a ↔ ¬IsUnit ((algebraMap R A) r - a)

theorem spectrum.not_mem_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} : r ∉ spectrum R a ↔ IsUnit ((algebraMap R A) r - a)

theorem spectrum.zero_mem_iff (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : 0 ∈ spectrum R a ↔ ¬IsUnit a

theorem spectrum.not_isUnit_of_zero_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : 0 ∈ spectrum R a → ¬IsUnit a

Alias of the forward direction of spectrum.zero_mem_iff.

theorem spectrum.zero_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : ¬IsUnit 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} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : 0 ∉ spectrum R a ↔ IsUnit a

theorem spectrum.zero_not_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : IsUnit a → 0 ∉ spectrum 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} [CommSemiring R] [Ring A] [Algebra R A] {a : A} : 0 ∉ spectrum R a → IsUnit a

Alias of the forward direction of spectrum.zero_not_mem_iff.

theorem spectrum.subset_singleton_zero_compl (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} (ha : IsUnit a) : spectrum R a ⊆ {0}ᶜ

theorem spectrum.mem_resolventSet_of_left_right_inverse {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} {b : A} {c : A} (h₁ : ((algebraMap R A) r - a) * b = 1) (h₂ : c * ((algebraMap R A) r - a) = 1) : r ∈ resolventSet R a

theorem spectrum.mem_resolventSet_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} : r ∈ resolventSet R a ↔ IsUnit ((algebraMap R A) r - a)

@[simp]

theorem spectrum.algebraMap_mem_iff (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} : (algebraMap R S) r ∈ spectrum S a ↔ r ∈ spectrum R a

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

Alias of the reverse direction of spectrum.algebraMap_mem_iff.

theorem spectrum.of_algebraMap_mem (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {r : R} : (algebraMap R S) r ∈ spectrum S a → r ∈ spectrum R a

Alias of the forward direction of spectrum.algebraMap_mem_iff.

@[simp]

theorem spectrum.preimage_algebraMap (S : Type u_1) {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} : ⇑(algebraMap R S) ⁻¹' spectrum S a = spectrum R a

@[simp]

theorem spectrum.resolventSet_of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [Subsingleton A] (a : A) : resolventSet R a = Set.univ

@[simp]

theorem spectrum.of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [Subsingleton A] (a : A) : spectrum R a = ∅

theorem spectrum.resolvent_eq {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {r : R} (h : r ∈ resolventSet R a) : resolvent a r = ↑(IsUnit.unit h)⁻¹

theorem spectrum.units_smul_resolvent {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} : r • resolvent a s = resolvent (r⁻¹ • a) (r⁻¹ • s)

theorem spectrum.units_smul_resolvent_self {R : Type u} {A : Type v} [CommSemiring R] [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} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} : r ∈ resolventSet R a ↔ IsUnit (resolvent a r)

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

theorem spectrum.inv_mem_resolventSet {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {a : Aˣ} (h : ↑r ∈ resolventSet R ↑a) : ↑r⁻¹ ∈ resolventSet R ↑a⁻¹

theorem spectrum.inv_mem_iff {R : Type u} {A : Type v} [CommSemiring R] [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} [CommSemiring R] [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} [CommSemiring 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} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {r : R} {s : R} : r + s ∈ spectrum R a ↔ r ∈ spectrum R (-(algebraMap R A) s + a)

theorem spectrum.add_mem_add_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {r : R} {s : R} : r + s ∈ spectrum R ((algebraMap R A) s + a) ↔ r ∈ spectrum R a

theorem spectrum.smul_mem_smul_iff {R : Type u} {A : Type v} [CommSemiring 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} [CommSemiring 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} [CommSemiring R] [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} [CommSemiring R] [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} [CommSemiring R] [Ring A] [Algebra R A] [InvolutiveStar R] [StarRing A] [StarModule R A] {r : R} {a : A} : star r ∈ resolventSet R a ↔ r ∈ resolventSet R (star a)

theorem spectrum.map_star {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [InvolutiveStar R] [StarRing A] [StarModule R A] (a : A) : spectrum R (star a) = star (spectrum R a)

theorem spectrum.subset_subalgebra {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {S : Subalgebra R A} (a : ↥S) : spectrum R ↑a ⊆ spectrum R a

theorem spectrum.subset_starSubalgebra {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] [StarRing R] [StarRing A] [StarModule R A] {S : StarSubalgebra R A} (a : ↥S) : spectrum R ↑a ⊆ spectrum R a

theorem spectrum.singleton_add_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : {r} + spectrum R a = spectrum R ((algebraMap R A) r + a)

theorem spectrum.add_singleton_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : spectrum R a + {r} = spectrum R (a + (algebraMap R A) r)

theorem spectrum.vadd_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : r +ᵥ spectrum R a = spectrum R ((algebraMap R A) r + a)

theorem spectrum.neg_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) : -spectrum R a = spectrum R (-a)

theorem spectrum.singleton_sub_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : {r} - spectrum R a = spectrum R ((algebraMap R A) r - a)

theorem spectrum.sub_singleton_eq {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (a : A) (r : R) : spectrum R a - {r} = spectrum R (a - (algebraMap R A) r)

@[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 𝕜 ((algebraMap 𝕜 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 : A) (b : A) : spectrum 𝕜 (a * b) \ {0} = spectrum 𝕜 (b * a) \ {0}

theorem spectrum.map_inv {𝕜 : Type u} {A : Type v} [Field 𝕜] [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} [CommSemiring R] [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 ∈ resolventSet R a) : 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} [CommSemiring R] [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} [CommRing R] [Ring A] [Algebra R A] [FunLike F A R] [AlgHomClass F R A R] [Nontrivial 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} [CommSemiring R] [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

Restriction of the spectrum

structure SpectrumRestricts {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] (a : A) (f : S → R) : Prop

Given an element a : A of an S-algebra, where S is itself an R-algebra, we say that the spectrum of a restricts via a function f : S → R if f is a left inverse of algebraMap R S, and f is a right inverse of algebraMap R S on spectrum S a.

For example, when f = Complex.re (so S := ℂ and R := ℝ), SpectrumRestricts a f means that the ℂ-spectrum of a is contained within ℝ. This arises naturally when a is selfadjoint and A is a C⋆-algebra.

This is the property allows us to restrict a continuous functional calculus over S to a continuous functional calculus over R.

• rightInvOn : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)

  f is a right inverse of algebraMap R S when restricted to spectrum S a.

• left_inv : Function.LeftInverse f ⇑(algebraMap R S)

  f is a left inverse of algebraMap R S.

theorem SpectrumRestricts.rightInvOn {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} (self : SpectrumRestricts a f) : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)

f is a right inverse of algebraMap R S when restricted to spectrum S a.

theorem SpectrumRestricts.left_inv {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} (self : SpectrumRestricts a f) : Function.LeftInverse f ⇑(algebraMap R S)

f is a left inverse of algebraMap R S.

theorem SpectrumRestricts.of_subset_range_algebraMap {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] (a : A) (f : S → R) (hf : Function.LeftInverse f ⇑(algebraMap R S)) (h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)) : SpectrumRestricts a f

theorem SpectrumRestricts.algebraMap_image {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {f : S → R} (h : SpectrumRestricts a f) : ⇑(algebraMap R S) '' spectrum R a = spectrum S a

theorem SpectrumRestricts.image {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {f : S → R} (h : SpectrumRestricts a f) : f '' spectrum S a = spectrum R a

theorem SpectrumRestricts.apply_mem {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {f : S → R} (h : SpectrumRestricts a f) {s : S} (hs : s ∈ spectrum S a) : f s ∈ spectrum R a

theorem SpectrumRestricts.subset_preimage {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {a : A} {f : S → R} (h : SpectrumRestricts a f) : spectrum S a ⊆ f ⁻¹' spectrum R a

theorem SpectrumRestricts.of_spectrum_eq {R : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {b : A} {f : S → R} (ha : SpectrumRestricts a f) (h : spectrum S a = spectrum S b) : SpectrumRestricts b f

theorem SpectrumRestricts.comp {R₁ : Type u_4} {R₂ : Type u_5} {R₃ : Type u_6} {A : Type u_7} [CommSemiring R₁] [CommSemiring R₂] [CommSemiring R₃] [Ring A] [Algebra R₁ A] [Algebra R₂ A] [Algebra R₃ A] [Algebra R₁ R₂] [Algebra R₂ R₃] [Algebra R₁ R₃] [IsScalarTower R₁ R₂ R₃] [IsScalarTower R₂ R₃ A] {a : A} {f : R₃ → R₂} {g : R₂ → R₁} {e : R₃ → R₁} (hfge : g ∘ f = e) (hf : SpectrumRestricts a f) (hg : SpectrumRestricts a g) : SpectrumRestricts a e