# mathlibdocumentation

algebra.algebra.spectrum

# 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
def resolvent_set (R : Type u) {A : Type v} [ring A] [ 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} [ring A] [ 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} [ring A] [ 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 (algebra_map R A r - a)⁻¹ when r ∈ resolvent R A and 0 when r ∈ spectrum R A.

Equations
@[simp]
theorem is_unit.coe_inv_sub_inv_smul {R : Type u} {A : Type v} [ring A] [ A] {r : Rˣ} {s : R} {a : A} (h : is_unit (r A) s - a)) :
noncomputable def is_unit.sub_inv_smul {R : Type u} {A : Type v} [ring A] [ A] {r : Rˣ} {s : R} {a : A} (h : is_unit (r A) s - a)) :

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

Equations
@[simp]
theorem is_unit.coe_sub_inv_smul {R : Type u} {A : Type v} [ring A] [ A] {r : Rˣ} {s : R} {a : A} (h : is_unit (r A) s - a)) :
theorem spectrum.mem_iff {R : Type u} {A : Type v} [ring A] [ A] {r : R} {a : A} :
r a ¬is_unit ( A) r - a)
theorem spectrum.not_mem_iff {R : Type u} {A : Type v} [ring A] [ A] {r : R} {a : A} :
r a is_unit ( A) r - a)
theorem spectrum.mem_resolvent_set_of_left_right_inverse {R : Type u} {A : Type v} [ring A] [ A] {r : R} {a b c : A} (h₁ : ( A) r - a) * b = 1) (h₂ : c * ( A) r - a) = 1) :
r
theorem spectrum.mem_resolvent_set_iff {R : Type u} {A : Type v} [ring A] [ A] {r : R} {a : A} :
r is_unit ( A) r - a)
@[simp]
theorem spectrum.resolvent_set_of_subsingleton {R : Type u} {A : Type v} [ring A] [ A] [subsingleton A] (a : A) :
@[simp]
theorem spectrum.of_subsingleton {R : Type u} {A : Type v} [ring A] [ A] [subsingleton A] (a : A) :
a =
theorem spectrum.resolvent_eq {R : Type u} {A : Type v} [ring A] [ A] {a : A} {r : R} (h : r ) :
theorem spectrum.units_smul_resolvent {R : Type u} {A : Type v} [ring A] [ A] {r : Rˣ} {s : R} {a : A} :
r s = resolvent (r⁻¹ a) (r⁻¹ s)
theorem spectrum.units_smul_resolvent_self {R : Type u} {A : Type v} [ring A] [ A] {r : Rˣ} {a : A} :
theorem spectrum.is_unit_resolvent {R : Type u} {A : Type v} [ring A] [ A] {r : R} {a : A} :

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

theorem spectrum.inv_mem_resolvent_set {R : Type u} {A : Type v} [ring A] [ A] {r : Rˣ} {a : Aˣ} (h : r ) :
theorem spectrum.inv_mem_iff {R : Type u} {A : Type v} [ring A] [ A] {r : Rˣ} {a : Aˣ} :
theorem spectrum.zero_mem_resolvent_set_of_unit {R : Type u} {A : Type v} [ring A] [ A] (a : Aˣ) :
0
theorem spectrum.ne_zero_of_mem_of_unit {R : Type u} {A : Type v} [ring A] [ A] {a : Aˣ} {r : R} (hr : r a) :
r 0
theorem spectrum.add_mem_iff {R : Type u} {A : Type v} [ring A] [ A] {a : A} {r s : R} :
r a r + s ( A) s + a)
theorem spectrum.smul_mem_smul_iff {R : Type u} {A : Type v} [ring A] [ A] {a : A} {s : R} {r : Rˣ} :
r s (r a) s a
theorem spectrum.unit_smul_eq_smul {R : Type u} {A : Type v} [ring A] [ A] (a : A) (r : Rˣ) :
(r a) = r a
theorem spectrum.unit_mem_mul_iff_mem_swap_mul {R : Type u} {A : Type v} [ring A] [ A] {a b : A} {r : Rˣ} :
r (a * b) r (b * a)
theorem spectrum.preimage_units_mul_eq_swap_mul {R : Type u} {A : Type v} [ring A] [ A] {a b : A} :
coe ⁻¹' (a * b) = coe ⁻¹' (b * a)
theorem spectrum.star_mem_resolvent_set_iff {R : Type u} {A : Type v} [ring A] [ A] [star_ring A] [ A] {r : R} {a : A} :
r
@[protected]
theorem spectrum.map_star {R : Type u} {A : Type v} [ring A] [ A] [star_ring A] [ A] (a : A) :
theorem spectrum.left_add_coset_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (a : A) (r : R) :
(spectrum R a) = ( A) r + a)
theorem spectrum.exists_mem_of_not_is_unit_aeval_prod {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] [is_domain R] {p : polynomial R} {a : A} (hp : p 0) (h : ¬is_unit ( (multiset.map (λ (x : R), p.roots).prod)) :
∃ (k : R), k a = 0
@[simp]
theorem spectrum.zero_eq {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [ A] [nontrivial A] :
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] [ A] [nontrivial A] (k : 𝕜) :
( A) k) = {k}
@[simp]
theorem spectrum.one_eq {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [ A] [nontrivial A] :
1 = {1}
theorem spectrum.smul_eq_smul {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [ A] [nontrivial A] (k : 𝕜) (a : A) (ha : (spectrum 𝕜 a).nonempty) :
(k a) = k 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] [ A] (a b : A) :
(a * b) \ {0} = (b * a) \ {0}
@[protected]
theorem spectrum.map_inv {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [ A] (a : Aˣ) :
theorem spectrum.subset_polynomial_aeval {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [ A] (a : A) (p : polynomial 𝕜) :
(λ (k : 𝕜), p) '' 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.

theorem spectrum.map_polynomial_aeval_of_degree_pos {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [ A] (a : A) (p : polynomial 𝕜) (hdeg : 0 < p.degree) :
( p) = (λ (k : 𝕜), p) '' 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.

theorem spectrum.map_polynomial_aeval_of_nonempty {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [ A] [nontrivial A] (a : A) (p : polynomial 𝕜) (hnon : (spectrum 𝕜 a).nonempty) :
( p) = (λ (k : 𝕜), p) '' 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. Note: the assumption [nontrivial A] is necessary for the same reason as in spectrum.zero_eq.

theorem spectrum.nonempty_of_is_alg_closed_of_finite_dimensional (𝕜 : Type u) {A : Type v} [field 𝕜] [ring A] [ A] [nontrivial A] [I : A] (a : A) :
∃ (k : 𝕜), k a

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

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] [ A] [ring B] [ B] [ A B] (φ : F) {a : A} {r : R} (h : r ) :
r (φ a)
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] [ A] [ring B] [ B] [ A B] (φ : F) (a : A) :
(φ a) a
theorem alg_hom.apply_mem_spectrum {F : Type u_1} {R : Type u_2} {A : Type u_3} [comm_ring R] [ring A] [ A] [ A R] [nontrivial R] (φ : F) (a : A) :
φ a a