English
There is a natural equivalence between F.CorepresentableBy X and coyoneda.obj (op X) ≅ F, given by a functorial correspondence between homEquiv data and isomorphisms.
Русский
Существуют естественные биекции между F.CorepresentableBy X и coyoneda.obj (op X) ≅ F, задаваемые соответствием гомэквивариантов и изоморфизмов.
LaTeX
$$corepresentableByEquiv {F : C ⥤ Type v} {X : C} : F.CorepresentableBy X ≃ (coyoneda.obj (op X) ≅ F)$$
Lean4
/-- The obvious bijection `F.CorepresentableBy X ≃ (yoneda.obj Y ≅ F)`
when `F : C ⥤ Type v₁` and `[Category.{v₁} C]`. -/
def corepresentableByEquiv {F : C ⥤ Type v₁} {X : C} : F.CorepresentableBy X ≃ (coyoneda.obj (op X) ≅ F)
where
toFun
r :=
NatIso.ofComponents (fun _ ↦ r.homEquiv.toIso)
(fun {X X'} f ↦ by
ext g
simp [r.homEquiv_comp])
invFun
e :=
{ homEquiv := (e.app _).toEquiv
homEquiv_comp := fun {X X'} f g ↦ congr_fun (e.hom.naturality f) g }
