mathlib3 documentation

category_theory.preadditive.yoneda.limits

The Yoneda embedding for preadditive categories preserves limits #

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

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.