English
Variant of the previous statement with a general g: X → Y in C^op. If f: yoneda.obj (unop X) ⟶ F and g: X ⟶ Y, then F.map g (yonedaEquiv f) = f.app Y g.unop.
Русский
Вариант предыдущего утверждения с обобщённым г: X → Y в C^op. Пусть f : yoneda.obj (unop X) ⟶ F и g: X ⟶ Y. Тогда F.map g (yonedaEquiv f) = f.app Y g.unop.
LaTeX
$$$F.map g (\ yonedaEquiv f) = f.app Y g.unop$$$
Lean4
/-- Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
can avoid the "motive is not type correct" error. -/
theorem map_yonedaEquiv' {X Y : Cᵒᵖ} {F : Cᵒᵖ ⥤ Type v₁} (f : yoneda.obj (unop X) ⟶ F) (g : X ⟶ Y) :
F.map g (yonedaEquiv f) = f.app Y g.unop := by
rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]
