English
There is an isometric continuous functional calculus under spectrum restriction: given a function f on a spectrum S and a restriction map that preserves isometry, one obtains an isometric continuous functional calculus on A. The result ensures compatibility via a spectrum-restriction map and provides the corresponding calculus p on A.
Русский
Существуют изометрический непрерывный функциональный калькулятор на A при ограничении спектра: задана функция на спектре S и изометрическое отображение ограничений, сохраняющее изометричность; образуется изометрический непрерывный функциональный калькулятор на A, совместимый с ограничением спектра.
LaTeX
$$$\text{IsometricCFC}(R,A,p)\;\text{exists under spectrum restriction}$$$
Lean4
protected theorem isometric_cfc (f : C(S, R)) (halg : Isometry (algebraMap R S)) (h0 : p 0)
(h : ∀ a, p a ↔ q a ∧ SpectrumRestricts a f) : IsometricContinuousFunctionalCalculus R A p
where
toContinuousFunctionalCalculus := SpectrumRestricts.cfc f halg.isUniformEmbedding h0 h
isometric a
ha := by
obtain ⟨ha', haf⟩ := h a |>.mp ha
have := SpectrumRestricts.cfc f halg.isUniformEmbedding h0 h
rw [cfcHom_eq_restrict f halg.isUniformEmbedding ha ha' haf]
refine .of_dist_eq fun g₁ g₂ ↦ ?_
simp only [starAlgHom_apply, isometry_cfcHom a ha' |>.dist_eq]
refine le_antisymm ?_ ?_
all_goals refine ContinuousMap.dist_le dist_nonneg |>.mpr fun x ↦ ?_
· simpa [halg.dist_eq] using ContinuousMap.dist_apply_le_dist _
· let x' : σ S a := Subtype.map (algebraMap R S) (fun _ ↦ spectrum.algebraMap_mem S) x
apply le_of_eq_of_le ?_ <| ContinuousMap.dist_apply_le_dist x'
simp only [ContinuousMap.comp_apply, ContinuousMap.coe_mk, StarAlgHom.ofId_apply, halg.dist_eq, x']
congr!
all_goals ext; exact haf.left_inv _ |>.symm
