isClosedEmbedding_starAlgHom — Mathlib

English

For ha, the range of the nonunital star calculus homomorphism cfcₙHom ha is exactly the elemental a-subalgebra.

Русский

Для ha диапазон неглавного звездо-калькулятора cfcₙHom ha равен элементарной подалгебре, порождённой a.

LaTeX

$$$\\mathrm{range}(\\mathrm{cfc\\,ₙHom}\\; ha) = \\mathrm{elemental}\\; a$$$

Lean4

theorem isClosedEmbedding_starAlgHom {a : A} {φ : C(spectrum S a, S) →⋆ₐ[S] A} (hφ : IsClosedEmbedding φ) {f : C(S, R)}
    (h : SpectrumRestricts a f) (halg : IsUniformEmbedding (algebraMap R S)) : IsClosedEmbedding (h.starAlgHom φ) :=
  hφ.comp <|
    IsUniformEmbedding.isClosedEmbedding <|
      .comp (ContinuousMap.isUniformEmbedding_comp _ halg)
        (UniformEquiv.arrowCongr h.homeomorph.symm (.refl _) |>.isUniformEmbedding)

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