English
There exists aContinuousFunctionalCalculus ℂ A IsStarNormal, i.e., a continuous functional calculus for normal elements in A.
Русский
Существует непрерывный функциональный калькулятор для нормальных элементов в A.
LaTeX
$$ContinuousFunctionalCalculus ℂ A IsStarNormal$$
Lean4
instance instContinuousFunctionalCalculus {A : Type*} [CStarAlgebra A] : ContinuousFunctionalCalculus ℂ A IsStarNormal
where
predicate_zero := .zero
spectrum_nonempty a _ := spectrum.nonempty a
exists_cfc_of_predicate a
ha :=
by
refine
⟨(StarAlgebra.elemental ℂ a).subtype.comp <| continuousFunctionalCalculus a, ?hom_isClosedEmbedding, ?hom_id,
?hom_map_spectrum, ?predicate_hom⟩
case hom_isClosedEmbedding =>
exact
Isometry.isClosedEmbedding <|
isometry_subtype_coe.comp <| StarAlgEquiv.isometry (continuousFunctionalCalculus a)
case hom_id => exact congr_arg Subtype.val <| continuousFunctionalCalculus_map_id a
case hom_map_spectrum =>
intro f
simp only [StarAlgHom.comp_apply, StarAlgHom.coe_coe, StarSubalgebra.coe_subtype]
rw [← StarSubalgebra.spectrum_eq (hS := StarAlgebra.elemental.isClosed ℂ a),
AlgEquiv.spectrum_eq (continuousFunctionalCalculus a), ContinuousMap.spectrum_eq_range]
case predicate_hom => exact fun f ↦ ⟨by rw [← map_star]; exact Commute.all (star f) f |>.map _⟩
