English
There is a dual construction to Yoneda, the Coyoneda embedding, which assigns to each Y ∈ Cᵒᵖ a functor Yᵒᵖ ⥤ (C ⥤ ModuleCat R) that is compatible with the R-linear structure.
Русский
Существует двойственная конструкция к Yoneda — Coyoneda embedding, которая каждому Y ∈ Cᵒᵖ сопоставляет функтор Yᵒᵖ ⥤ (C ⥤ ModuleCat R), совместимый с R-линейной структурой.
LaTeX
$$$\\text{linearCoyoneda}_R(C): C^{op} \\to C \\to \\text{ModuleCat}(R)$, с \n$$ (\\text{linearCoyoneda}_R(C))(Y) (X) = \\mathrm{ModuleCat.of}_R(\\mathrm{Hom}_C(\\mathrm{unop}\\,Y, X)).$$$$
Lean4
/-- The Yoneda embedding for `R`-linear categories `C`,
sending an object `Y : Cᵒᵖ` to the `ModuleCat R`-valued copresheaf on `C`,
with value on `X : C` given by `ModuleCat.of R (unop Y ⟶ X)`. -/
@[simps]
def linearCoyoneda : Cᵒᵖ ⥤ C ⥤ ModuleCat R
where
obj
Y :=
{ obj := fun X => ModuleCat.of R (unop Y ⟶ X)
map := fun f => ModuleCat.ofHom (Linear.rightComp R _ f) }
map {Y₁ Y₂}
f := { app := fun X => @ModuleCat.ofHom R _ (unop Y₁ ⟶ X) (unop Y₂ ⟶ X) _ _ _ _ (Linear.leftComp _ _ f.unop) }
