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 identity map ContinuousMap.id ℂ to the (unique) preimage of a under the coercion of elementalStarAlgebra ℂ 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, ℂ) ≃⋆ₐ[ℂ] elementalStarAlgebra ℂ a: this is the composition of the inverse of the gelfandStarTransform with the natural isomorphism induced by the homeomorphism elementalStarAlgebra.characterSpaceHomeo.
• elementalStarAlgebra.characterSpaceHomeo : characterSpace ℂ (elementalStarAlgebra ℂ a) ≃ₜ spectrum ℂ a: this homeomorphism is defined by evaluating a character φ at a, and noting that φ a ∈ spectrum ℂ a since φ is an algebra homomorphism. Moreover, this map is continuous and bijective and since the spaces involved are compact Hausdorff, it is a homeomorphism.

instance instNormedCommRingSubtypeMemStarSubalgebraElementalStarAlgebraOfIsStarNormal {R : Type u_2} {A : Type u_3} [CommRing R] [StarRing R] [NormedRing A] [Algebra R A] [StarRing A] [ContinuousStar A] [StarModule R A] (a : A) [IsStarNormal a] : NormedCommRing { x : A // x ∈ elementalStarAlgebra R a }

Equations

• instNormedCommRingSubtypeMemStarSubalgebraElementalStarAlgebraOfIsStarNormal a = NormedCommRing.mk ⋯

@[simp]

theorem elementalStarAlgebra.characterSpaceToSpectrum_coe {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [CStarRing A] [StarModule ℂ A] [CompleteSpace A] (x : A) (φ : ↑(WeakDual.characterSpace ℂ { x_1 : A // x_1 ∈ elementalStarAlgebra ℂ x })) : ↑(elementalStarAlgebra.characterSpaceToSpectrum x φ) = φ ⟨x, ⋯⟩

noncomputable def elementalStarAlgebra.characterSpaceToSpectrum {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [CStarRing A] [StarModule ℂ A] [CompleteSpace A] (x : A) (φ : ↑(WeakDual.characterSpace ℂ { x_1 : A // x_1 ∈ elementalStarAlgebra ℂ x })) : ↑(spectrum ℂ x)

The natural map from characterSpace ℂ (elementalStarAlgebra ℂ 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, elementalStarAlgebra.self_mem ℂ x⟩ there is slightly more work to do.

Equations

• elementalStarAlgebra.characterSpaceToSpectrum x φ = ⟨φ ⟨x, ⋯⟩, ⋯⟩

theorem elementalStarAlgebra.continuous_characterSpaceToSpectrum {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [CStarRing A] [StarModule ℂ A] [CompleteSpace A] (x : A) : Continuous (elementalStarAlgebra.characterSpaceToSpectrum x)

theorem elementalStarAlgebra.bijective_characterSpaceToSpectrum {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [CStarRing A] [StarModule ℂ A] [CompleteSpace A] (a : A) [IsStarNormal a] : Function.Bijective (elementalStarAlgebra.characterSpaceToSpectrum a)

noncomputable def elementalStarAlgebra.characterSpaceHomeo {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [CStarRing A] [StarModule ℂ A] [CompleteSpace A] (a : A) [IsStarNormal a] : ↑(WeakDual.characterSpace ℂ { x : A // x ∈ elementalStarAlgebra ℂ a }) ≃ₜ ↑(spectrum ℂ a)

The homeomorphism between the character space of the unital C⋆-subalgebra generated by a single normal element a : A and spectrum ℂ a.

Equations

• elementalStarAlgebra.characterSpaceHomeo a = ⋯.homeoOfEquivCompactToT2

noncomputable def continuousFunctionalCalculus {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [CStarRing A] [StarModule ℂ A] [CompleteSpace A] (a : A) [IsStarNormal a] : C(↑(spectrum ℂ a), ℂ) ≃⋆ₐ[ℂ] { x : A // x ∈ elementalStarAlgebra ℂ 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 equivalence identifies (ContinuousMap.id ℂ).restrict (spectrum ℂ a)) with a; see continuousFunctionalCalculus_map_id. As such it extends the polynomial functional calculus.

Equations

• continuousFunctionalCalculus a = (Homeomorph.compStarAlgEquiv' ℂ ℂ (elementalStarAlgebra.characterSpaceHomeo a)).trans (gelfandStarTransform { x : A // x ∈ elementalStarAlgebra ℂ a }).symm

theorem continuousFunctionalCalculus_map_id {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [CStarRing A] [StarModule ℂ A] [CompleteSpace A] (a : A) [IsStarNormal a] : (continuousFunctionalCalculus a) (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ)) = ⟨a, ⋯⟩