Structures · Analysis

NonUnitalContinuousFunctionalCalculus

A non-unital star R-algebra A has a continuous functional calculus for elements satisfying the property p : A → Prop if + for every such element a : A there is a non-unital star algebra homomorphism cfcₙHom : C(quasispectrum R a, R)₀ →⋆ₙₐ[R] A sending the (restriction of) the identity map to a. + cfcHom is continuous and injective and the quasispectrum of the image of function f is its range. + cfcₙHom preserves the property p. The property p is marked as an outParam so that the user need not specify it. In practice, + for R := ℂ, we choose p := IsStarNormal, + for R := ℝ, we choose p := IsSelfAdjoint, + for R := ℝ≥0, we choose p := (0 ≤ ·). Instead of directly providing the data we opt instead for a Prop class. In all relevant cases, the continuous functional calculus is uniquely determined, and utilizing this approach prevents diamonds or problems arising from multiple instances.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

Shape

3 explicit arguments · adds predicate_zero, compactSpace_quasispectrum, exists_cfc_of_predicate