Spectrum of an element in an algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.
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 𝕜
.