cfcₙHom_eq_cfcₙ_extend — Mathlib

English

If f and g agree on the spectrum of a, then their functional calculi at a agree.

Русский

Если f и g совпадают на спектре a, то их функциональные калькуляторы в a совпадают.

LaTeX

$$Set.EqOn f g (quasispectrum R a) → cfcₙ f a = cfcₙ g a$$

Lean4

theorem cfcₙHom_eq_cfcₙ_extend {a : A} (g : R → R) (ha : p a) (f : C(σₙ R a, R)₀) :
    cfcₙHom ha f = cfcₙ (Function.extend Subtype.val f g) a :=
  by
  have h : f = (σₙ R a).restrict (Function.extend Subtype.val f g) := by ext; simp
  have hg : ContinuousOn (Function.extend Subtype.val f g) (σₙ R a) :=
    continuousOn_iff_continuous_restrict.mpr <| h ▸ map_continuous f
  have hg0 : (Function.extend Subtype.val f g) 0 = 0 :=
    by
    rw [← quasispectrum.coe_zero (R := R) a, Subtype.val_injective.extend_apply]
    exact map_zero f
  rw [cfcₙ_apply ..]
  congr!

Похожие утверждения