English
Let C be a category, F a presheaf on C (a functor C^op → Type), X,Y objects of C, f an arrow yoneda.obj X → F, and g: Y → X. Then applying F along g^op to the Yoneda equivalence of f yields the component of f at (op Y) evaluated on g; i.e. F.map g.op (yonedaEquiv f) = f.app (op Y) g.
Русский
Пусть C — категория, F — картина (прешпхеаф) на C, то есть функтор C^op → Type; X, Y — объекты C; f : yoneda.obj X → F; g: Y → X. Тогда применение F вдоль g^op к эквивалентности yoneda(f) даёт элемент в F.obj (op Y), равный значению f на (op Y) и на g; то есть F.map g.op (yonedaEquiv f) = f.app (op Y) g.
LaTeX
$$$F.map g^{op} (\ yonedaEquiv f) = f.app (op Y) g$$$
Lean4
/-- See also `map_yonedaEquiv'` for a more general version. -/
theorem map_yonedaEquiv {X Y : C} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj X ⟶ F) (g : Y ⟶ X) :
F.map g.op (yonedaEquiv f) = f.app (op Y) g := by
rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
