English
Let R be a presheaf of rings on C, and M a presheaf of R-modules. For every object X in C, there exists a natural bijection between the morphisms from the free presheaf (free R) on the Yoneda presheaf at X to M, and the value M at X interpreted in the opposite direction, i.e., M.obj (Opposite.op X). This expresses a universal property of the free Yoneda construction.
Русский
Пусть R – расправная (презешаф) кольца над C и M – презешаф модулей над R. Для каждого объекта X в C существует естественная биекция между отображениями из свободного презешафта (free R) на Yoneda-презешафе X в M и значением M в X, преображенным в противоположное направление, то есть M.obj (Opposite.op X). Это выражает универсальное свойство свободной Yoneda-конструкции.
LaTeX
$$$\\text{Hom}_{\\mathrm{PMod}_R}((\\mathrm{free}\\;R)(\\mathrm{yoneda}(X)), M) \\cong M(X^{op})$$$
Lean4
/-- When `R : Cᵒᵖ ⥤ RingCat`, `M : PresheafOfModules R`, and `X : C`, this is the
bijection `((free R).obj (yoneda.obj X) ⟶ M) ≃ M.obj (Opposite.op X)`. -/
noncomputable def freeYonedaEquiv {M : PresheafOfModules.{v} R} {X : C} :
((free R).obj (yoneda.obj X) ⟶ M) ≃ M.obj (Opposite.op X) :=
freeHomEquiv.trans yonedaEquiv
