English
Let a be an element of a star-algebra A with a predicate p, and b an element that commutes with a and with the adjoint of a. For any continuous functional calculus f on the spectrum of a, the element cfcHom ha f commutes with b.
Русский
Пусть a принадлежит элементу A с заданным свойством p и элемент b удовлетворяет [a,b]=0 и [a*,b]=0. Для любого непрерывного функционального калькулятора f определенного на спектре a, элемент cfcHom ha f коммутирует с b.
LaTeX
$$$\forall a,b \in A,\ ha : p(a),\ Commute \!a\! b \\land \\ Commute \! (a^*) \! b \\Rightarrow \\forall f \in C(\mathrm{spectrum}(\mathbb{K},a), \mathbb{K}),\ Commute( cfcHom(ha,f), b).$$
Lean4
protected theorem cfcHom {a b : A} (ha : p a) (hb₁ : Commute a b) (hb₂ : Commute (star a) b) (f : C(spectrum 𝕜 a, 𝕜)) :
Commute (cfcHom ha f) b := by
open scoped ContinuousFunctionalCalculus in
induction f using ContinuousMap.induction_on_of_compact with
| const
r =>
conv =>
enter [1, 2]
equals algebraMap 𝕜 _ r => rfl
rw [AlgHomClass.commutes]
exact Algebra.commute_algebraMap_left r b
| id => rwa [cfcHom_id ha]
| star_id => rwa [map_star, cfcHom_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 cfcHom_continuous ha |>.tendsto _
