compPreadditiveYonedaIso_hom_app_app_apply

English

Inverse Yoneda-like morphisms preserve additive structure under adjunctions.

Русский

Обратные Йонадовы-подобные морфизмы сохраняют аддитивную структуру при сопряжении.

LaTeX

$$Isomorphism related statements for inverse Yoneda iso$$

Lean4

theorem compPreadditiveYonedaIso_hom_app_app_apply (X : Cᵒᵖ) (Y : D)
    (a : ULift.{max v₁ v₂, v₁} (Opposite.unop X ⟶ G.obj Y)) :
    ((adj.compPreadditiveYonedaIso.hom.app Y).app X) a =
      ULift.up ((adj.homEquiv (Opposite.unop X) Y).symm (AddEquiv.ulift a)) :=
  rfl

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