cfcₙHom_eq_of_continuous_of_map_id

English

If a continuous, star-preserving homomorphism φ agrees with the nonunital functional calculus on the relevant generators and sends the identity to a, then it equals the calculus map cfcₙHom ha.

Русский

Если непрерывный гомоморфизм, сохраняющий сопряжение, совпадает с неприводимым функциональным калькулятором на соответствующих образах и отображает тождественный элемент в a, то он равен cfcₙHom ha.

LaTeX

$$$\text{If } (h\varphi_1: Continuous φ\text{ and } h\varphi_2: φ(.id)=a)\Rightarrow cfc_nHom ha = φ.$$$

Lean4

theorem cfcₙHom_eq_of_continuous_of_map_id [UniqueHom R A] (φ : C(σₙ R a, R)₀ →⋆ₙₐ[R] A) (hφ₁ : Continuous φ)
    (hφ₂ : φ (.id _) = a) : cfcₙHom ha = φ :=
  (cfcₙHom ha).ext_continuousMap a φ (cfcₙHom_isClosedEmbedding ha).continuous hφ₁ <| by rw [cfcₙHom_id ha, hφ₂]

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