English
There exists a nonunital continuous functional calculus for A, obtained from the unitized calculus via a restriction along the inr map and a spectral embedding.
Русский
Существуeт ненулевой непрерывный функциональный калькулятор для A, получаемый из унитированного калькулятора через ограничение по отображению inr и спектральному вложению.
LaTeX
$$$$ \\text{nonUnitalCFC} : \\text{NonUnitalContinuousFunctionalCalculus } 𝕜 A \\;\\text{(p)} $$$$
Lean4
theorem nonUnitalContinuousFunctionalCalculus : NonUnitalContinuousFunctionalCalculus 𝕜 A p
where
predicate_zero := by
rw [← hp₁, Unitization.inr_zero 𝕜]
exact cfc_predicate_zero 𝕜
exists_cfc_of_predicate a
ha :=
by
let ψ : C(σₙ 𝕜 a, 𝕜)₀ →⋆ₙₐ[𝕜] A :=
comp (inrRangeEquiv 𝕜 A).symm <| codRestrict (cfcₙAux hp₁ a ha) _ (cfcₙAux_mem_range_inr hp₁ a ha)
have coe_ψ (f : C(σₙ 𝕜 a, 𝕜)₀) : ψ f = cfcₙAux hp₁ a ha f :=
congr_arg Subtype.val <|
(inrRangeEquiv 𝕜 A).apply_symm_apply ⟨cfcₙAux hp₁ a ha f, cfcₙAux_mem_range_inr hp₁ a ha f⟩
refine ⟨ψ, ?isClosedEmbedding, ?map_id, fun f ↦ ?map_spec, fun f ↦ ?isStarNormal⟩
case
isClosedEmbedding =>
apply isometry_inr (𝕜 := 𝕜) (A := A) |>.isClosedEmbedding |>.of_comp_iff.mp
have : inr ∘ ψ = cfcₙAux hp₁ a ha := by ext1; rw [Function.comp_apply, coe_ψ]
exact this ▸ isClosedEmbedding_cfcₙAux hp₁ a ha
case map_id => exact inr_injective (R := 𝕜) <| coe_ψ _ ▸ cfcₙAux_id hp₁ a ha
case map_spec => exact quasispectrum_eq_spectrum_inr' 𝕜 𝕜 (ψ f) ▸ coe_ψ _ ▸ spec_cfcₙAux hp₁ a ha f
case isStarNormal => exact hp₁.mp <| coe_ψ _ ▸ cfcHom_predicate (R := 𝕜) (hp₁.mpr ha) _
