compPreadditiveYonedaIso_inv_app_app_apply

English

Alternative representation of the inverse Yoneda application in additive context.

Русский

Альтернативное представление применения обратной Йонады в аддитивном контексте.

LaTeX

$$Alt form of Yoneda inverse apply$$

Lean4

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

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