English
Let C be a category, F a functor C ⥤ Type. For any morphism f : coyoneda.obj (op X) ⟶ F and any g : X ⟶ Y, the image of f under the coyoneda equivalence, after applying F along g, equals the component of f at Y applied to g. In symbols: F.map g (coyonedaEquiv f) = f.app Y g.
Русский
Пусть C — категория, F — функтор C ⥤ Type. Для произвольного отображения f : coyoneda.obj (op X) ⟶ F и любой стрелки g : X ⟶ Y выполняется равенство, связывающее отображение F вдоль g и компоненту f на Y: F.map g (coyonedaEquiv f) = f.app Y g.
LaTeX
$$$$ F.map(g)(\\mathrm{coyonedaEquiv}(f)) = f.app\\,Y\\,g $$$$
Lean4
theorem map_coyonedaEquiv {X Y : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F) (g : X ⟶ Y) :
F.map g (coyonedaEquiv f) = f.app Y g := by
rw [coyonedaEquiv_naturality, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map]
