# mathlibdocumentation

category_theory.limits.preserves.functor_category

# 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

noncomputable def category_theory.functor_category.prod_preserves_colimits {C : Type u} {D : Type u₂} (F : C D) :

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
@[protected, instance]
noncomputable def category_theory.whiskering_left_preserves_limits {C : Type u} {D : Type u₂} {E : Type u} (F : C E) :
Equations
noncomputable def category_theory.preserves_limit_of_Lan_presesrves_limit {C D : Type u} (F : C D) (J : Type u)  :

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

Equations