instNonUnitalIsometricContinuousFunctionalCalculus

English

The nonunital isometric continuous functional calculus instance extends to IsSelfAdjoint in nonunital C*-algebras.

Русский

Непользовательное изометрическое непрерывное функциональное исчисление распространяется на IsSelfAdjoint в неединичных C*-алгебрах.

LaTeX

$$NonUnitalIsometricContinuousFunctionalCalculus ℂ A IsSelfAdjoint$$

Lean4

instance instNonUnitalIsometricContinuousFunctionalCalculus :
    NonUnitalIsometricContinuousFunctionalCalculus ℂ A IsStarNormal where
  isometric a
    ha := by
    refine AddMonoidHomClass.isometry_of_norm _ fun f ↦ ?_
    rw [← norm_inr (𝕜 := ℂ), ← inrNonUnitalStarAlgHom_apply, ← NonUnitalStarAlgHom.comp_apply,
      inr_comp_cfcₙHom_eq_cfcₙAux a, cfcₙAux]
    simp only [NonUnitalStarAlgHom.comp_assoc, NonUnitalStarAlgHom.comp_apply, toContinuousMapHom_apply,
      NonUnitalStarAlgHom.coe_coe]
    rw [norm_cfcHom (a : Unitization ℂ A), StarAlgEquiv.norm_map]
    rfl

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