English
With a unique-hom context, cfc_nHom ha equals cfc_nHom_of_cfcHom R ha.
Русский
При наличии уникального гомоморфа cfc_nHom ha = cfc_nHom_of_cfcHom R ha.
LaTeX
$$$$ cfc\\!_nHom ha = cfc\\!_nHom\\_of\\_cfcHom R ha $$$$
Lean4
/-- The non-unital continuous functional calculus obtained by restricting a unital calculus
to functions that map zero to zero. This is an auxiliary definition and is not
intended for use outside this file. The equality between the non-unital and unital
calculi in this case is encoded in the lemma `cfcₙ_eq_cfc`. -/
noncomputable def cfcₙHom_of_cfcHom {a : A} (ha : p a) : C(σₙ R a, R)₀ →⋆ₙₐ[R] A :=
let e := ContinuousMapZero.toContinuousMapHom (X := σₙ R a) (R := R)
let f : C(spectrum R a, quasispectrum R a) := ⟨_, continuous_inclusion <| spectrum_subset_quasispectrum R a⟩
let ψ := ContinuousMap.compStarAlgHom' R R f
(cfcHom ha (R := R) : C(spectrum R a, R) →⋆ₙₐ[R] A).comp <| (ψ : C(σₙ R a, R) →⋆ₙₐ[R] C(spectrum R a, R)).comp e
