mathlib documentation

category_theory.linear.yoneda

The Yoneda embedding for R-linear categories #

The Yoneda embedding for R-linear categories C, sends an object X : C to the Module R-valued presheaf on C, with value on Y : Cᵒᵖ given by Module.of R (unop Y ⟶ X).

TODO: linear_yoneda R C is R-linear. TODO: In fact, linear_yoneda itself is additive and R-linear.

The Yoneda embedding for R-linear categories C, sending an object X : C to the Module R-valued presheaf on C, with value on Y : Cᵒᵖ given by Module.of R (unop Y ⟶ X).

Equations