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, ℂ) ≃⋆ₐ[ℂ] elemental ℂ a which sends the (restriction of) the
identity map ContinuousMap.id ℂ to the (unique) preimage of a under the coercion of
elemental ℂ a to A.
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., Polynomial.aeval).
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.
The result we have established here is the strongest possible, but it is not the version which is
most useful in practice. The generic API for the continuous functional calculus can be found in
Analysis.CStarAlgebra.ContinuousFunctionalCalculus in the Unital and NonUnital files. The
relevant instances on C⋆-algebra can be found in the Instances file.
Main definitions #
continuousFunctionalCalculus : C(spectrum ℂ a, ℂ) ≃⋆ₐ[ℂ] elemental ℂ a: this is the composition of the inverse of thegelfandStarTransformwith the natural isomorphism induced by the homeomorphismelemental.characterSpaceHomeo.elemental.characterSpaceHomeo:characterSpace ℂ (elemental ℂ a) ≃ₜ spectrum ℂ a: this homeomorphism is defined by evaluating a characterφata, 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.IsStarNormal.instContinuousFunctionalCalculus: the continuous functional calculus for normal elements in a unital C⋆-algebra overℂ.CStarAlgebra.instNonnegSpectrumClass: In a unital C⋆-algebra overℂwhich is also aStarOrderedRing, the spectrum of a nonnegative element is nonnegative.
The natural map from characterSpace ℂ (elemental ℂ x) to spectrum ℂ x given
by evaluating φ at x. This is essentially just evaluation of the gelfandTransform of x,
but because we want something in spectrum ℂ x, as opposed to
spectrum ℂ ⟨x, elemental.self_mem ℂ x⟩ there is slightly more work to do.
Equations
- StarAlgebra.elemental.characterSpaceToSpectrum x φ = ⟨φ ⟨x, ⋯⟩, ⋯⟩
Instances For
Alias of StarAlgebra.elemental.characterSpaceToSpectrum.
The natural map from characterSpace ℂ (elemental ℂ x) to spectrum ℂ x given
by evaluating φ at x. This is essentially just evaluation of the gelfandTransform of x,
but because we want something in spectrum ℂ x, as opposed to
spectrum ℂ ⟨x, elemental.self_mem ℂ x⟩ there is slightly more work to do.
Equations
Instances For
Alias of StarAlgebra.elemental.continuous_characterSpaceToSpectrum.
Alias of StarAlgebra.elemental.bijective_characterSpaceToSpectrum.
The homeomorphism between the character space of the unital C⋆-subalgebra generated by a
single normal element a : A and spectrum ℂ a.
Equations
- StarAlgebra.elemental.characterSpaceHomeo a = ⋯.homeoOfEquivCompactToT2
Instances For
Alias of StarAlgebra.elemental.characterSpaceHomeo.
The homeomorphism between the character space of the unital C⋆-subalgebra generated by a
single normal element a : A and spectrum ℂ a.
Instances For
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
equivalence identifies (ContinuousMap.id ℂ).restrict (spectrum ℂ a)) with a; see
continuousFunctionalCalculus_map_id. As such it extends the polynomial functional calculus.
Equations
Instances For
Continuous functional calculus for normal elements #
The spectrum of a nonnegative element is nonnegative #
The partial order on a C⋆-algebra defined by x ≤ y if and only if y - x is
selfadjoint and has nonnegative spectrum.
This is not declared as an instance because one may already have a partial order with better definitional properties. However, it can be useful to invoke this as an instance in proofs.
Equations
Instances For
The CStarAlgebra.spectralOrder on a C⋆-algebra is a StarOrderedRing.
This lemma requires a lot from type class synthesis, and so one should instead favor the bespoke
versions for ℝ≥0, ℝ, and ℂ.
note: the version for ℝ≥0, Unization.nnreal_cfcₙ_eq_cfc_inr, can be found in
Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order