English
The Yoneda embedding for R-linear categories is a functor sending X ∈ C to the presheaf Y ↦ ModuleCat.of_R(Hom_C(unop Y, X)), with compatible action on morphisms.
Русский
Юнова эмбеддинг для R-линейных категорий — это функтор, отправляющий X в преспешаф Y ↦ ModuleCat.of_R(Hom_C(unop Y, X)) и действующий на морфизмы по правилу композиции.
LaTeX
$$$\\text{linearYoneda}_R(C): C \\to C^{op} \\to \\text{ModuleCat}(R),\\quad X \\mapsto\\big(Y \\mapsto \\mathrm{ModuleCat.of}_R(\\mathrm{Hom}_C(\\mathrm{unop}\\,Y, X))\\big)$$$
Lean4
/-- The Yoneda embedding for `R`-linear categories `C`,
sending an object `X : C` to the `ModuleCat R`-valued presheaf on `C`,
with value on `Y : Cᵒᵖ` given by `ModuleCat.of R (unop Y ⟶ X)`. -/
@[simps]
def linearYoneda : C ⥤ Cᵒᵖ ⥤ ModuleCat R
where
obj
X :=
{ obj := fun Y => ModuleCat.of R (unop Y ⟶ X)
map := fun f => ModuleCat.ofHom (Linear.leftComp R _ f.unop) }
map {X₁ X₂} f := { app := fun Y => @ModuleCat.ofHom R _ (Y.unop ⟶ X₁) (Y.unop ⟶ X₂) _ _ _ _ (Linear.rightComp R _ f) }
