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.preservesLimitsPreadditiveYonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) : CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveYonedaObj X)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• CategoryTheory.PreservesLimitsPreadditiveYoneda.obj X = let_fun this := inferInstance; this

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

Equations

• CategoryTheory.PreservesLimitsPreadditiveCoyoneda.obj X = let_fun this := inferInstance; this