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)
:
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ᵒᵖ)
:
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.toPrefunctor.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.toPrefunctor.obj X)
Equations
- CategoryTheory.PreservesLimitsPreadditiveCoyoneda.obj X = let_fun this := inferInstance; this