Documentation

Mathlib.Algebra.Algebra.Spectrum.Basic

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

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

Equations
@[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)) :
@[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
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.notMem_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} :
rspectrum R a IsUnit ((algebraMap R A) r - a)
@[deprecated spectrum.notMem_iff (since := "2025-05-23")]
theorem spectrum.not_mem_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : A} :
rspectrum R a IsUnit ((algebraMap R A) r - a)

Alias of spectrum.notMem_iff.

theorem spectrum.zero_mem_iff (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : 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 a0 spectrum R a

Alias of the reverse direction of spectrum.zero_mem_iff.

theorem spectrum.zero_notMem_iff (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
0spectrum R a IsUnit a
@[deprecated spectrum.zero_notMem_iff (since := "2025-05-23")]
theorem spectrum.zero_not_mem_iff (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
0spectrum R a IsUnit a

Alias of spectrum.zero_notMem_iff.

theorem spectrum.zero_notMem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
IsUnit a0spectrum R a

Alias of the reverse direction of spectrum.zero_notMem_iff.


Alias of spectrum.zero_notMem_iff.

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

Alias of the forward direction of spectrum.zero_notMem_iff.


Alias of spectrum.zero_notMem_iff.

@[deprecated spectrum.isUnit_of_zero_notMem (since := "2025-05-23")]
theorem spectrum.isUnit_of_zero_not_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
0spectrum R aIsUnit a

Alias of the forward direction of spectrum.zero_notMem_iff.


Alias of the forward direction of spectrum.zero_notMem_iff.


Alias of spectrum.zero_notMem_iff.

@[deprecated spectrum.zero_notMem (since := "2025-05-23")]
theorem spectrum.zero_not_mem (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} :
IsUnit a0spectrum R a

Alias of the reverse direction of spectrum.zero_notMem_iff.


Alias of the reverse direction of spectrum.zero_notMem_iff.


Alias of spectrum.zero_notMem_iff.

@[simp]
theorem Units.zero_notMem_spectrum (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : Aˣ) :
0spectrum R a
@[deprecated Units.zero_notMem_spectrum (since := "2025-05-23")]
theorem Units.zero_not_mem_spectrum (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a : Aˣ) :
0spectrum R a

Alias of Units.zero_notMem_spectrum.

theorem spectrum.subset_singleton_zero_compl (R : Type u) {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a : A} (ha : IsUnit a) :
theorem spectrum.mem_resolventSet_of_left_right_inverse {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a b c : A} (h₁ : ((algebraMap R A) r - a) * b = 1) (h₂ : c * ((algebraMap R A) r - a) = 1) :
theorem spectrum.mem_resolventSet_iff {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : R} {a : 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} :
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 ar 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} :
@[simp]
@[simp]
theorem spectrum.of_subsingleton {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] [Subsingleton A] (a : 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) :
theorem spectrum.units_smul_resolvent {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {r : Rˣ} {s : R} {a : A} :
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} :

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) :
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 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 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_comm {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a b : A} {r : Rˣ} :
r spectrum R (a * b) r spectrum R (b * a)
@[deprecated spectrum.unit_mem_mul_comm (since := "2025-01-29")]
theorem spectrum.unit_mem_mul_iff_mem_swap_mul {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] {a b : A} {r : Rˣ} :
r spectrum R (a * b) r spectrum R (b * a)

Alias of spectrum.unit_mem_mul_comm.

theorem spectrum.preimage_units_mul_comm {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a b : A) :
@[deprecated spectrum.preimage_units_mul_comm (since := "2025-01-29")]

Alias of spectrum.preimage_units_mul_comm.

theorem spectrum.setOf_isUnit_inter_mul_comm {R : Type u} {A : Type v} [CommSemiring R] [Ring A] [Algebra R A] (a b : A) :
{r : R | IsUnit r} spectrum R (a * b) = {r : R | IsUnit r} 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} :
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) :
theorem spectrum.subset_subalgebra {S : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] [SetLike S A] [SubringClass S A] [SMulMemClass S R A] {s : S} (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) :
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.inv₀_mem_iff {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} :
theorem spectrum.inv₀_mem_inv_iff {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} :
theorem spectrum.inv₀_mem {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} :
r spectrum R a⁻¹r⁻¹ spectrum R a

Alias of the reverse direction of spectrum.inv₀_mem_iff.

theorem spectrum.of_inv₀_mem {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} :
r⁻¹ spectrum R ar spectrum R a⁻¹

Alias of the forward direction of spectrum.inv₀_mem_iff.

theorem spectrum.inv₀_mem_inv {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} :
r spectrum R ar⁻¹ spectrum R a⁻¹

Alias of the reverse direction of spectrum.inv₀_mem_inv_iff.

theorem spectrum.of_inv₀_mem_inv {R : Type u} {A : Type v} [Semifield R] [Ring A] [Algebra R A] {r : R} {a : Aˣ} :
r⁻¹ spectrum R a⁻¹r spectrum R a

Alias of the forward direction of spectrum.inv₀_mem_inv_iff.

@[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_comm {𝕜 : Type u} {A : Type v} [Field 𝕜] [Ring A] [Algebra 𝕜 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
@[simp]
theorem spectrum.units_conjugate {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {u : Aˣ} :
spectrum R (u * a * u⁻¹) = spectrum R a

Conjugation by a unit preserves the spectrum, inverse on right.

@[simp]
theorem spectrum.units_conjugate' {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] {a : A} {u : Aˣ} :
spectrum R (u⁻¹ * a * u) = spectrum R a

Conjugation by a unit preserves the spectrum, inverse on left.