starAlgHom_ext — Mathlib

English

Nonunital star maps lift uniquely to unital star maps; there is a star isomorphism between nonunital star homs and unitized star homs.

Русский

Неуниверсальные звездные отображения поднимаются уникально к единичным звездным отображениям; существует звёздное изоморфное соответствие.

LaTeX

$$$\text{starLift} : (A \to⋆ₙₐ[R] C) \simeq (Unitization(R,A) \to⋆ₐ[R] C)$$$

Lean4

/-- See note [partially-applied ext lemmas] -/
@[ext]
theorem starAlgHom_ext {φ ψ : Unitization R A →⋆ₐ[R] C}
    (h :
      (φ : Unitization R A →⋆ₙₐ[R] C).comp (Unitization.inrNonUnitalStarAlgHom R A) =
        (ψ : Unitization R A →⋆ₙₐ[R] C).comp (Unitization.inrNonUnitalStarAlgHom R A)) :
    φ = ψ :=
  Unitization.algHom_ext'' <| DFunLike.congr_fun h

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