nonUnitalStarAlgHom_id — Mathlib

English

If φ is a closed embedding, then the restricted nonunital star algebra homomorphism h.nonUnitalStarAlgHom φ is also a closed embedding (under the given spectrum-restriction hypotheses).

Русский

Если φ — замкнутое вложение, то полученный ограниченный не-единичный звёздный гомоморфизм h.nonUnitalStarAlgHom φ тоже является замкнутым вложением (при заданных условиях ограничения спектра).

LaTeX

$$IsClosedEmbedding φ → IsClosedEmbedding (h.nonUnitalStarAlgHom φ)$$

Lean4

theorem nonUnitalStarAlgHom_id {a : A} {φ : C(σₙ S a, S)₀ →⋆ₙₐ[S] A} {f : C(S, R)} (h : QuasispectrumRestricts a f)
    (h_id : φ (.id _) = a) : h.nonUnitalStarAlgHom φ (.id _) = a :=
  by
  simp only [QuasispectrumRestricts.nonUnitalStarAlgHom_apply]
  convert h_id
  ext x
  exact h.rightInvOn x.2

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