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 ModuleCat in the main file about the preadditive Yoneda embedding.

instance CategoryTheory.preservesLimits_preadditiveYonedaObj {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) : Limits.PreservesLimits (preadditiveYonedaObj X)

instance CategoryTheory.preservesLimits_preadditiveCoyonedaObj {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) : Limits.PreservesLimits (preadditiveCoyonedaObj X)

instance CategoryTheory.preservesLimits_preadditiveYoneda_obj {C : Type u} [Category.{v, u} C] [Preadditive C] (X : C) : Limits.PreservesLimits (preadditiveYoneda.obj X)

instance CategoryTheory.preservesLimits_preadditiveCoyoneda_obj {C : Type u} [Category.{v, u} C] [Preadditive C] (X : Cᵒᵖ) : Limits.PreservesLimits (preadditiveCoyoneda.obj X)