Commit 2024-02-27 19:35 e10b4f54

feat: abstract continuous functional calculus for unital algebras (#5750) This PR introduces two classes ContinuousFunctionalCalculus and UniqueContinuousFunctionalCalculus. The former provides a collection of star algebra homomoprhisms from the continuous functions on the spectrum of an element a : A, into the algebra A itself, subject to the constraint that a satisfies a certain predicate p : A → Prop. These morphisms are continuous (even closed embeddings) and send the identity function to a itself, and moreover, the spectrum of the image of an element is its range. The latter class says that there is at most one such star algebra homomorphism which is continuous and maps the identity to a; in practice, this is a consequence of the Stone-Weierstrass theorem, but we create a separate class because we will also want a version for ℝ≥0-valued functions. This latter class is the key to establish the compositional property of the continuous functional calculus, cfc_comp : cfc a (g ∘ f) = cfc (cfc a f) g. This is one of the key properties of the continuous functional calculus that makes it useful.