Structures · Analysis

ContinuousMap.UniqueHom

A class guaranteeing that the continuous functional calculus is uniquely determined by the properties that it is a continuous star algebra homomorphism mapping the (restriction of) the identity to a. This is the necessary tool used to establish cfcHom_comp and the more common variant cfc_comp. This class has instances, which can be found in Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean, in each of the common cases ℂ, ℝ and ℝ≥0 as a consequence of the Stone-Weierstrass theorem. This class is separate from ContinuousFunctionalCalculus primarily because we will later use SpectrumRestricts to derive an instance of ContinuousFunctionalCalculus on a scalar subring from one on a larger ring (i.e., to go from a continuous functional calculus over ℂ for normal elements to one over ℝ for selfadjoint elements), and proving this additional property is preserved would be burdensome or impossible.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Shape

2 explicit arguments · adds eq_of_continuous_of_map_id