Documentation

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

source
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.
source
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.
source
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
source
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