toIso — Mathlib

English

If a functor F is corepresentable by an object X via an isomorphism e, then coyoneda.obj(op X) is canonically isomorphic to F.

Русский

Если F является корпредставляющим по объекта X через изоморфизм e, то coyoneda.obj(op X) канонически изоморфен F.

LaTeX

$$$ coyoneda.obj(\\operatorname{op} X) \\cong F $$$

Lean4

/-- The isomorphism `coyoneda.obj (op X) ≅ F` induced by `e : F.CorepresentableBy X`. -/
def toIso {F : C ⥤ Type v₁} {X : C} (e : F.CorepresentableBy X) : coyoneda.obj (op X) ≅ F :=
  corepresentableByEquiv e

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