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 elementa : A
whereA
is anR
-algebra.spectrum a : set R
: the spectrum of an elementa : A
whereA
is anR
-algebra.resolvent : R → A
: the resolvent function isλ r, ring.inverse (↑ₐr - a)
, and hence whenr ∈ resolvent R A
, it is actually the inverse of the unit(↑ₐr - a)
.
Main statements #
spectrum.unit_smul_eq_smul
andspectrum.smul_eq_smul
: units in the scalar ring commute (multiplication) with the spectrum, and over a field even0
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
andspectrum.preimage_units_mul_eq_swap_mul
: the units (ofR
) 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
ofa : A
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
- resolvent_set R a = {r : R | is_unit (⇑(algebra_map R A) r - a)}
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 = (resolvent_set 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
- resolvent a r = ring.inverse (⇑(algebra_map R A) r - a)
The unit 1 - r⁻¹ • a
constructed from r • 1 - a
when the latter is a unit.
The resolvent is a unit when the argument is in the resolvent set.
Without the assumption nontrivial A
, then 0 : A
would be invertible.
the assumption (σ a).nonempty
is necessary and cannot be removed without
further conditions on the algebra A
and scalar field 𝕜
.
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.
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
.
In this version of the spectral mapping theorem, we assume the spectrum is nonempty instead of assuming the degree of the polynomial is positive.
A specialization of spectrum.map_polynomial_aeval_of_nonempty
to monic monomials for
convenience.
A specialization of spectrum.map_polynomial_aeval_of_nonempty
to monic monomials for
convenience.
Every element a
in a nontrivial finite-dimensional algebra A
over an algebraically closed field 𝕜
has non-empty spectrum.