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
Instances for category_theory.linear_yoneda

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

Equations
Instances for category_theory.linear_coyoneda