Spectral properties in C⋆-algebras #
In this file, we establish various properties related to the spectrum of elements in C⋆-algebras.
In particular, we show that the spectrum of a unitary element is contained in the unit circle in
ℂ
, the spectrum of a selfadjoint element is real, the spectral radius of a selfadjoint element
or normal element is its norm, among others.
An essential feature of C⋆-algebras is spectral permanence. This is the property that the spectrum of an element in a closed subalgebra is the same as the spectrum of the element in the whole algebra. For Banach algebras more generally, and even for Banach ⋆-algebras, this fails.
A consequence of spectral permanence is that one may always enlarge the C⋆-algebra (via a unital
embedding) while preserving the spectrum of any element. In addition, it allows us to make sense of
the spectrum of elements in non-unital C⋆-algebras by considering them as elements in the
Unitization
of the C⋆-algebra, or indeed any unital C⋆-algebra. Of course, one may do this
(that is, consider the spectrum of an element in a non-unital by embedding it in a unital algebra)
for any Banach algebra, but the downside in that setting is that embedding in different unital
algebras results in varying spectra.
In Mathlib, we don't define the spectrum of an element in a non-unital C⋆-algebra, and instead
simply consider the quasispectrum
so as to avoid depending on a choice of unital algebra. However,
we can still establish a form of spectral permanence.
Main statements #
unitary.spectrum_subset_circle
: The spectrum of a unitary element is contained in the unit sphere inℂ
.IsSelfAdjoint.spectralRadius_eq_nnnorm
: The spectral radius of a selfadjoint element is equal to its norm.IsStarNormal.spectralRadius_eq_nnnorm
: The spectral radius of a normal element is equal to its norm.IsSelfAdjoint.mem_spectrum_eq_re
: Any element of the spectrum of a selfadjoint element is real.
StarSubalgebra.coe_isUnit
: forx : S
in a C⋆-SubalgebraS
ofA
, then↑x : A
is a Unit if and only ifx
is a unit.StarSubalgebra.spectrum_eq
: spectral_permanence forx : S
, whereS
is a C⋆-Subalgebra ofA
,spectrum ℂ x = spectrum ℂ (x : A)
.
TODO #
- prove a variation of spectral permanence using
StarAlgHom
instead ofStarSubalgebra
. - prove a variation of spectral permanence for
quasispectrum
.
In a C⋆-algebra, the spectral radius of a self-adjoint element is equal to its norm.
See IsSelfAdjoint.toReal_spectralRadius_eq_norm
for a version involving
spectralRadius ℝ a
.
Any element of the spectrum of a selfadjoint is real.
Any element of the spectrum of a selfadjoint is real.
Any element of the spectrum of a selfadjoint is real.
The spectrum of a selfadjoint is real
The spectrum of a selfadjoint is real
The complement of the spectrum of a selfadjoint element in a C⋆-algebra is connected.
For a unital C⋆-subalgebra S
of A
and x : S
, if ↑x : A
is invertible in A
, then
x
is invertible in S
.
Spectral permanence. The spectrum of an element is invariant of the (closed)
StarSubalgebra
in which it is contained.
A non-unital star algebra homomorphism of complex C⋆-algebras is norm contractive.
A non-unital star algebra homomorphism of complex C⋆-algebras is norm contractive.
Non-unital star algebra homomorphisms between C⋆-algebras are continuous linear maps. See note [lower instance priority]
This instance is provided instead of StarHomClass
to avoid type class inference loops.
See note [lower instance priority]
Equations
- ⋯ = ⋯
This is not an instance to avoid type class inference loops. See
WeakDual.Complex.instStarHomClass
.
Equations
- ⋯ = ⋯