mathlib3 documentation

category_theory.preadditive.yoneda.basic

The Yoneda embedding for preadditive categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The Yoneda embedding for preadditive categories sends an object Y to the presheaf sending an object X to the group of morphisms X ⟶ Y. At each point, we get an additional End Y-module structure.

We also show that this presheaf is additive and that it is compatible with the normal Yoneda embedding in the expected way and deduce that the preadditive Yoneda embedding is fully faithful.

TODO #

The Yoneda embedding for preadditive categories sends an object Y to the presheaf sending an object X to the End Y-module of morphisms X ⟶ Y.

Equations
Instances for category_theory.preadditive_yoneda_obj

The Yoneda embedding for preadditive categories sends an object Y to the presheaf sending an object X to the group of morphisms X ⟶ Y. At each point, we get an additional End Y-module structure, see preadditive_yoneda_obj.

Equations
Instances for category_theory.preadditive_yoneda

The Yoneda embedding for preadditive categories sends an object X to the copresheaf sending an object Y to the End X-module of morphisms X ⟶ Y.

Equations
Instances for category_theory.preadditive_coyoneda_obj

The Yoneda embedding for preadditive categories sends an object X to the copresheaf sending an object Y to the group of morphisms X ⟶ Y. At each point, we get an additional End X-module structure, see preadditive_coyoneda_obj.

Equations
Instances for category_theory.preadditive_coyoneda