mathlib documentation

category_theory.preadditive.yoneda.limits

The Yoneda embedding for preadditive categories preserves limits #

The Yoneda embedding for preadditive categories preserves limits.

Implementation notes #

This is in a separate file to avoid having to import the development of the abelian structure on Module in the main file about the preadditive Yoneda embedding.