English
An auxiliary nonunital star-homomorphism cfcₙAux is constructed from the unital calculus on the unitization, using a chain of isomorphisms, whose range lies inside the image of the canonical inclusion into the unitization.
Русский
Формируется вспомогательное отображение cfcₙAux – ненулевой звездовый однородник, получаемый из унитального функционального калькуляуса на единичной расширении через последовательность отображений, чья область значения лежит в образе включения в единичное расширение.
LaTeX
$$$$ cfc\\,\\!\\_nAux : C(\\sigma_n 𝕜 a, 𝕜)_0 \\to_*^{𝕜} A^+ $$ является непрерывным_STAR-гомоморфизмом в контексте непрерывного функционального калькулятора на единичном заполнении.$$
Lean4
/-- This is an auxiliary definition used for constructing an instance of the non-unital continuous
functional calculus given a instance of the unital one on the unitization.
This is the natural non-unital star homomorphism obtained from the chain
```lean
calc
C(σₙ 𝕜 a, 𝕜)₀ →⋆ₙₐ[𝕜] C(σₙ 𝕜 a, 𝕜) := ContinuousMapZero.toContinuousMapHom
_ ≃⋆[𝕜] C(σ 𝕜 (↑a : A⁺¹), 𝕜) := Homeomorph.compStarAlgEquiv'
_ →⋆ₐ[𝕜] A⁺¹ := cfcHom
```
This range of this map is contained in the range of `(↑) : A → A⁺¹` (see `cfcₙAux_mem_range_inr`),
and so we may restrict it to `A` to get the necessary homomorphism for the non-unital continuous
functional calculus.
-/
noncomputable def cfcₙAux : C(σₙ 𝕜 a, 𝕜)₀ →⋆ₙₐ[𝕜] A⁺¹ :=
(cfcHom (R := 𝕜) (hp₁.mpr ha) : C(σ 𝕜 (a : A⁺¹), 𝕜) →⋆ₙₐ[𝕜] A⁺¹) |>.comp
(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 <| .setCongr <| (quasispectrum_eq_spectrum_inr' 𝕜 𝕜 a).symm) |>.comp
ContinuousMapZero.toContinuousMapHom
