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.

References #

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

source

def category_theory.functor_category.prod_preserves_colimits {C : Type v₂} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.limits.has_binary_products D] [category_theory.limits.has_colimits D] [Π (X : D), category_theory.limits.preserves_colimits (category_theory.limits.prod.functor.obj X)] (F : C ⥤ D) :

category_theory.limits.preserves_colimits (category_theory.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

category_theory.functor_category.prod_preserves_colimits F = {preserves_colimits_of_shape := λ (J : Type v₂) (𝒥 : category_theory.small_category J), {preserves_colimit := λ (K : J ⥤ C ⥤ D), {preserves := λ (c : category_theory.limits.cocone K) (t : category_theory.limits.is_colimit c), category_theory.limits.evaluation_jointly_reflects_colimits ((category_theory.limits.prod.functor.obj F).map_cocone c) (λ (k : C), id (let this : category_theory.limits.is_colimit (((category_theory.evaluation C D).obj k ⋙ category_theory.limits.prod.functor.obj (F.obj k)).map_cocone c) := category_theory.limits.is_colimit_of_preserves ((category_theory.evaluation C D).obj k ⋙ category_theory.limits.prod.functor.obj (F.obj k)) t in category_theory.limits.is_colimit.map_cocone_equiv (category_theory.nat_iso.of_components (λ (G : C ⥤ D), category_theory.as_iso (category_theory.limits.prod_comparison ((category_theory.evaluation C D).obj k) F G)) _).symm this))}}}