English
Let A be a nonunital star algebra over a field 𝕜 with suitable topology. If φ and ψ are continuous nonunital ℝ-algebra homomorphisms from the nonunital algebra of continuous functions C(X, ℝ)₀ into A that agree on the identity function, then φ = ψ. In other words, the extension provided by the continuous functional calculus is unique once it is fixed on the identity function.
Русский
Пусть A — неполной единицы звёздно-алгебра над полем 𝕜 с подходящей топологией. Если φ и ψ — непрерывные гомоморфизмы без единицы из $\mathcal{C}(X, \mathbb{R})_{0}$ в A и они совпадают на тождественной функции, то φ = ψ. То есть непрерывное функциональное исчисление задаёт единственный такой гомоморфизм, фиксируемый на идентичности.
LaTeX
$$$\\phi = \\psi$ если $\\phi(\\mathrm{id}) = \\psi(\\mathrm{id})$ и оба являются непрерывными гомоморфизмами;\\, \\phi, \\psi : \\mathcal{C}(X, \\mathbb{R})_{0} \\to A$.$$
Lean4
instance uniqueNonUnitalContinuousFunctionalCalculus [TopologicalSpace A] [T2Space A] [NonUnitalRing A] [StarRing A]
[Module 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] : ContinuousMapZero.UniqueHom 𝕜 A where
eq_of_continuous_of_map_id s hs h0 φ ψ hφ hψ
h := by
rw [DFunLike.ext'_iff, ← Set.eqOn_univ, ← (ContinuousMapZero.adjoin_id_dense _).closure_eq]
refine Set.EqOn.closure (fun f hf ↦ ?_) hφ hψ
rw [← NonUnitalStarAlgHom.mem_equalizer]
apply adjoin_le ?_ hf
rw [Set.singleton_subset_iff]
exact h
