# Preservation of (co)limits in the functor category #

• Show that if X ⨯ - preserves colimits in D for any X : D, then the product functor F ⨯ - for F : C ⥤ D preserves colimits.

The idea of the proof is simply that products and colimits in the functor category are computed pointwise, so pointwise preservation implies general preservation.

• Show that F ⋙ - preserves limits if the target category has limits.
• Show that F : C ⥤ D preserves limits of a certain shape if Lan F.op : Cᵒᵖ ⥤ Type* preserves such limits.

# References #

https://ncatlab.org/nlab/show/commutativity+of+limits+and+colimits#preservation_by_functor_categories_and_localizations

def CategoryTheory.FunctorCategory.prodPreservesColimits {C : Type u} {D : Type u₂} [] [(X : D) → CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj X)] (F : ) :
CategoryTheory.Limits.PreservesColimits (CategoryTheory.Limits.prod.functor.obj F)

If X × - preserves colimits in D for any X : D, then the product functor F ⨯ - for F : C ⥤ D also preserves colimits.

Note this is (mathematically) a special case of the statement that "if limits commute with colimits in D, then they do as well in C ⥤ D" but the story in Lean is a bit more complex, and this statement isn't directly a special case. That is, even with a formalised proof of the general statement, there would still need to be some work to convert to this version: namely, the natural isomorphism (evaluation C D).obj k ⋙ prod.functor.obj (F.obj k) ≅ prod.functor.obj F ⋙ (evaluation C D).obj k

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.whiskeringLeftPreservesLimits {C : Type u} {D : Type u₂} [] {E : Type u} (F : ) :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.whiskeringRightPreservesLimitsOfShape {C : Type u_1} [] {D : Type u_2} [] {E : Type u_3} [] {J : Type u_4} [] (F : ) :
Equations
• One or more equations did not get rendered due to their size.
instance CategoryTheory.whiskeringRightPreservesLimits {C : Type u_1} [] {D : Type u_2} [] {E : Type u_3} [] (F : ) [] [] :
Equations
• = { preservesLimitsOfShape := fun {J : Type w'} [] => inferInstance }
noncomputable def CategoryTheory.preservesLimitOfLanPreservesLimit {C : Type u} {D : Type u} (F : ) (J : Type u) [] :

If Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*) preserves limits of shape J, so will F.

Equations
Instances For