English
In the nonunital setting, if a and b commute and star a commutes with b, then cfcₙHom ha f commutes with b for all f in C(quasispectrum 𝕜 a, 𝕜)₀.
Русский
В непользовательной среде, если a и b коммутируют, и star a коммутирует с b, то cfcₙHom ha f коммутирует с b для всех f ∈ C(quasispectrum 𝕜 a, 𝕜)₀.
LaTeX
$$$\forall a,b:\ Commute a b \land Commute (star a) b \\Rightarrow \forall f:\, C(quasispectrum 𝕜 a, 𝕜)_0,\ Commute( cfc\ₙHom ha f, b).$$
Lean4
protected theorem cfcₙHom {a b : A} (ha : p a) (hb₁ : Commute a b) (hb₂ : Commute (star a) b)
(f : C(quasispectrum 𝕜 a, 𝕜)₀) : Commute (cfcₙHom ha f) b := by
open scoped NonUnitalContinuousFunctionalCalculus in
induction f using ContinuousMapZero.induction_on_of_compact with
| zero => simp
| smul r f hf => rw [map_smul]; exact hf.smul_left r
| id => rwa [cfcₙHom_id ha]
| star_id => rwa [map_star, cfcₙHom_id]
| add f g hf hg => rw [map_add]; exact hf.add_left hg
| mul f g hf hg => rw [map_mul]; exact mul_left hf hg
| frequently f
hf =>
rw [commute_iff_eq, ← Set.mem_setOf (p := fun x => x * b = b * x), ←
(isClosed_eq (by fun_prop) (by fun_prop)).closure_eq]
apply mem_closure_of_frequently_of_tendsto hf
exact cfcₙHom_continuous ha |>.tendsto _
