English
For any g: R → R, under SpectrumRestricts, the CFC with g on a equals the CFC with algebraMap applied to g(f(x)).
Русский
Для любого $g:R\\to R$ при SpectrumRestricts выполняется: $\\mathrm{cfc}\\,g\\,a = \\mathrm{cfc}(\\lambda x. \\mathrm{algebraMap}_{R S}(g(f(x))))\\,a$.
LaTeX
$$$\\forall g:R\\to R,\\ cfc\\ g\\ a = cfc(\\lambda x. algebraMap(R, S)(g(f(x))))\\ a$$$
Lean4
theorem cfcₙ_eq_restrict (f : C(S, R)) (halg : IsUniformEmbedding (algebraMap R S)) {a : A} (hpa : p a) (hqa : q a)
(h : QuasispectrumRestricts a f) (g : R → R) : cfcₙ g a = cfcₙ (fun x ↦ algebraMap R S (g (f x))) a :=
by
by_cases hg : ContinuousOn g (σₙ R a) ∧ g 0 = 0
· obtain ⟨hg, hg0⟩ := hg
rw [cfcₙ_apply g a, cfcₙHom_eq_restrict f halg hpa hqa h, nonUnitalStarAlgHom_apply, cfcₙHom_eq_cfcₙ_extend 0]
apply cfcₙ_congr fun x hx ↦ ?_
lift x to σₙ S a using hx
simp
· simp only [not_and_or] at hg
obtain (hg | hg) := hg
· have : ¬ContinuousOn (fun x ↦ algebraMap R S (g (f x)) : S → S) (σₙ S a) :=
by
refine fun hg' ↦ hg ?_
rw [halg.isEmbedding.continuousOn_iff]
simpa [halg.isEmbedding.continuousOn_iff, Function.comp_def, h.left_inv _] using
hg'.comp halg.isEmbedding.continuous.continuousOn (fun _ : R ↦ quasispectrum.algebraMap_mem S)
rw [cfcₙ_apply_of_not_continuousOn a hg, cfcₙ_apply_of_not_continuousOn a this]
· rw [cfcₙ_apply_of_not_map_zero a hg, cfcₙ_apply_of_not_map_zero a (by simpa [h.map_zero])]
