English
Let f: C(S,R) be as above with h : SpectrumRestricts a f. Then the restricted functional calculus homomorphism on p is equal to the star-conjugate of the functional calculus on q composed with h: cfc p = h.starAlgHom (cfc q).
Русский
Пусть f: C(S,R) удовлетворяет условиям с h: SpectrumRestricts(a,f). Тогда ограниченный функциональный расчётный гомоморфизм для p равен звёздному гомоморфизму, полученному из cfc q и композиции с h: cfc(p) = h.starAlgHom(cfc(q)).
LaTeX
$$$cfc(hpa) = h.starAlgHom\\big(cfc(hqa)\\big),$ где $hpa$ и $hqa$ соответствуют предикатам $p$ и $q$ на $a$.$$
Lean4
theorem cfcHom_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a)
(h : SpectrumRestricts a f) : cfcHom hpa = h.starAlgHom (cfcHom hqa) :=
by
apply cfcHom_eq_of_continuous_of_map_id
· exact h.isClosedEmbedding_starAlgHom (cfcHom_isClosedEmbedding hqa) halg |>.continuous
· exact h.starAlgHom_id (cfcHom_id hqa)
