Documentation

Mathlib.CategoryTheory.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: linearYoneda R C is R-linear. TODO: In fact, linearYoneda 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
  • One or more equations did not get rendered due to their size.
Instances For

    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
    • One or more equations did not get rendered due to their size.
    Instances For