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.preservesLimits_preadditiveYonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : C) :
CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveYonedaObj X)
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.preservesLimits_preadditiveCoyonedaObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) :
CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveCoyonedaObj X)
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.preservesLimits_preadditiveYoneda_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.preservesLimits_preadditiveCoyoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (X : Cᵒᵖ) :
CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveCoyoneda.obj X)
Equations
  • ⋯ = ⋯