isClosedEmbedding_nonUnitalStarAlgHom

English

Under the same hypotheses, the restricted nonunital star algebra homomorphism is a closed embedding.

Русский

При тех же предположениях ограниченный неединичный звездный гомоморфизм является замкнутым вложением.

LaTeX

$$IsClosedEmbedding (h.nonUnitalStarAlgHom φ)$$

Lean4

theorem isClosedEmbedding_nonUnitalStarAlgHom {a : A} {φ : C(σₙ S a, S)₀ →⋆ₙₐ[S] A} (hφ : IsClosedEmbedding φ)
    {f : C(S, R)} (h : QuasispectrumRestricts a f) (halg : IsUniformEmbedding (algebraMap R S)) :
    IsClosedEmbedding (h.nonUnitalStarAlgHom φ) :=
  by
  have : h.homeomorph.symm 0 = 0 := Subtype.ext (map_zero <| algebraMap _ _)
  refine
    hφ.comp <|
      IsUniformEmbedding.isClosedEmbedding <|
        .comp (ContinuousMapZero.isUniformEmbedding_comp _ halg)
          (UniformEquiv.arrowCongrLeft₀ h.homeomorph.symm this |>.isUniformEmbedding)

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