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

Notations #

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
theorem is_unit.smul_sub_iff_sub_inv_smul {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {r : Rˣ} {a : A} :
is_unit (r 1 - a) is_unit (1 - r⁻¹ a)
theorem spectrum.mem_iff {R : Type u} {A : Type v} [comm_ring R] [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} [comm_ring R] [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} [comm_ring R] [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} [comm_ring R] [ring A] [ A] {r : R} {a : A} :
r is_unit ( A) r - a)
theorem spectrum.resolvent_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {a : A} {r : R} (h : r ) :
theorem spectrum.add_mem_iff {R : Type u} {A : Type v} [comm_ring R] [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} [comm_ring R] [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} [comm_ring R] [ring A] [ A] (a : A) (r : Rˣ) :
(r a) = r a
theorem spectrum.left_add_coset_eq {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (a : A) (r : R) :
r +l a = ( A) r + a)
theorem spectrum.unit_mem_mul_iff_mem_swap_mul {R : Type u} {A : Type v} [comm_ring R] [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} [comm_ring R] [ring A] [ A] {a b : A} :
coe ⁻¹' (a * b) = coe ⁻¹' (b * a)
@[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}
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.exists_mem_of_not_is_unit_aeval_prod {𝕜 : Type u} {A : Type v} [field 𝕜] [ring A] [ A] {p : polynomial 𝕜} {a : A} (hp : p 0) (h : ¬is_unit ( (multiset.map (λ (x : 𝕜), p.roots).prod)) :
∃ (k : 𝕜), k a = 0
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.apply_mem_spectrum {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [ A] [nontrivial R] (φ : A →ₐ[R] R) (a : A) :
φ a a