English
If unique homomorphisms align on composed functions, then the composed cfcHom agrees with the corresponding cfcHom of the composed map.
Русский
Если уникальные гомоморфизмы согласованы на композиции функций, то соответствующая композиция cfcHom согласуется с соответствующим cfcHom от композиции.
LaTeX
$$cfcHom_comp ha f f' (hff' : ∀x, f x = f' x) (g) : cfcHom ha (g ∘ f') = cfcHom (cfcHom_predicate ha f) g$$
Lean4
theorem cfcHom_comp [UniqueHom R A] (f : C(spectrum R a, R)) (f' : C(spectrum R a, spectrum R (cfcHom ha f)))
(hff' : ∀ x, f x = f' x) (g : C(spectrum R (cfcHom ha f), R)) :
cfcHom ha (g.comp f') = cfcHom (cfcHom_predicate ha f) g :=
by
let φ : C(spectrum R (cfcHom ha f), R) →⋆ₐ[R] A := (cfcHom ha).comp <| ContinuousMap.compStarAlgHom' R R f'
suffices cfcHom (cfcHom_predicate ha f) = φ from DFunLike.congr_fun this.symm g
refine cfcHom_eq_of_continuous_of_map_id (cfcHom_predicate ha f) φ ?_ ?_
· exact (cfcHom_isClosedEmbedding ha).continuous.comp f'.continuous_precomp
· simp only [φ, StarAlgHom.comp_apply, ContinuousMap.compStarAlgHom'_apply]
congr
ext x
simp [hff']
