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 #
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))}}}