Continuous functional calculus #
In this file we construct the
continuousFunctionalCalculus for a normal element
a of a
(unital) C⋆-algebra over
ℂ. This is a star algebra equivalence
C(spectrum ℂ a, ℂ) ≃⋆ₐ[ℂ] elementalStarAlgebra ℂ a which sends the (restriction of) the
ContinuousMap.id ℂ to the (unique) preimage of
a under the coercion of
elementalStarAlgebra ℂ a to
Being a star algebra equivalence between C⋆-algebras, this map is continuous (even an isometry),
and by the Stone-Weierstrass theorem it is the unique star algebra equivalence which extends the
polynomial functional calculus (i.e.,
For any continuous function
f : spectrum ℂ a → ℂ, this makes it possible to define an element
f a (not valid notation) in the original algebra, which heuristically has the same eigenspaces as
a and acts on eigenvector of
a for an eigenvalue
λ as multiplication by
f λ. This
description is perfectly accurate in finite dimension, but only heuristic in infinite dimension as
there might be no genuine eigenvector. In particular, when
f is a polynomial
∑ cᵢ Xⁱ, then
f a is
∑ cᵢ aⁱ. Also,
id a = a.
This file also includes a proof of the spectral permanence theorem for (unital) C⋆-algebras
Main definitions #
continuousFunctionalCalculus : C(spectrum ℂ a, ℂ) ≃⋆ₐ[ℂ] elementalStarAlgebra ℂ a: this is the composition of the inverse of the
gelfandStarTransformwith the natural isomorphism induced by the homeomorphism
characterSpace ℂ (elementalStarAlgebra ℂ a) ≃ₜ spectrum ℂ a: this homeomorphism is defined by evaluating a character
a, and noting that
φ a ∈ spectrum ℂ asince
φis an algebra homomorphism. Moreover, this map is continuous and bijective and since the spaces involved are compact Hausdorff, it is a homeomorphism.
Main statements #
x : Sin a C⋆-Subalgebra
↑x : Ais a Unit if and only if
xis a unit.
StarSubalgebra.spectrum_eq: spectral_permanence for
x : S, where
Sis a C⋆-Subalgebra of
spectrum ℂ x = spectrum ℂ (x : A).
The result we have established here is the strongest possible, but it is likely not the version which will be most useful in practice. Future work will include developing an appropriate API for the continuous functional calculus (including one for real-valued functions with real argument that applies to self-adjoint elements of the algebra).
This lemma is used in the proof of
which in turn is the key to spectral permanence
StarSubalgebra.spectrum_eq, which is itself
necessary for the continuous functional calculus. Using the continuous functional calculus, this
lemma can be superseded by one that omits the
This is the key lemma on the way to establishing spectral permanence for C⋆-algebras, which is
StarSubalgebra.spectrum_eq. This lemma is superseded by
StarSubalgebra.coe_isUnit, which does not require an
IsStarNormal hypothesis and holds for
any closed star subalgebra.
x : A which is invertible in
A, the inverse lies in any unital C⋆-subalgebra
For a unital C⋆-subalgebra
x : S, if
↑x : A is invertible in
x is invertible in
Spectral permanence. The spectrum of an element is invariant of the (closed)
StarSubalgebra in which it is contained.
The natural map from
characterSpace ℂ (elementalStarAlgebra ℂ x) to
spectrum ℂ x given
x. This is essentially just evaluation of the
but because we want something in
spectrum ℂ x, as opposed to
spectrum ℂ ⟨x, elementalStarAlgebra.self_mem ℂ x⟩ there is slightly more work to do.
The homeomorphism between the character space of the unital C⋆-subalgebra generated by a
single normal element
a : A and
spectrum ℂ a.
Continuous functional calculus. Given a normal element
a : A of a unital C⋆-algebra,
the continuous functional calculus is a
StarAlgEquiv from the complex-valued continuous
functions on the spectrum of
a to the unital C⋆-subalgebra generated by
a. Moreover, this
(ContinuousMap.id ℂ).restrict (spectrum ℂ a)) with
continuousFunctionalCalculus_map_id. As such it extends the polynomial functional calculus.