English
Consider the inverse bijection of the free Yoneda equivalence. For x in M.obj (Opposite.op X), the inverse applied to x, when evaluated at X on the distinguished free generator, yields x itself. This confirms that the inverse bijection correctly recovers x from its image under the forward bijection.
Русский
Рассматривая обратную биекцию эквиваленции свободной Yoneda, для x в M.obj (Opposite.op X) обратное отображение возвращает x, когда его применяют к X на выделенном свободном генераторе. Это подтверждает корректность восстановления x из образа по прямой биекции.
LaTeX
$$$\\big(\\mathrm{freeYonedaEquiv}^{-1} x\\big)_X(\\mathrm{id}_X) = x\\quad\\text{for } x \\in M(X^{op}).$$$
Lean4
theorem freeYonedaEquiv_symm_app (M : PresheafOfModules.{v} R) (X : C) (x : M.obj (Opposite.op X)) :
(freeYonedaEquiv.symm x).app (Opposite.op X) (ModuleCat.freeMk (𝟙 _)) = x :=
by
dsimp [freeYonedaEquiv, freeHomEquiv, yonedaEquiv]
rw [ModuleCat.freeDesc_apply, op_id, M.presheaf.map_id]
rfl
