English
If every X ∈ D yields X × - preserves colimits in D, then the product functor (prod.functor.obj F) preserves colimits in the functor category C ⥤ D.
Русский
Если для каждого X из D операция X × - сохраняет колимиты в D, то проиводящая F ⋯ сохраняет колимиты в категориальной категории функций.
LaTeX
$$$\forall X\in D\, \mathrm{PreservesColimits}(\mathrm{prod.functor.obj}\; X) \Rightarrow \mathrm{PreservesColimits}(\mathrm{prod.functor.obj}\; F)$$$
Lean4
/-- 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`
-/
theorem prod_preservesColimits [HasBinaryProducts D] [HasColimits D] [∀ X : D, PreservesColimits (prod.functor.obj X)]
(F : C ⥤ D) : PreservesColimits (prod.functor.obj F) where
preservesColimitsOfShape {J : Type u}
[Category.{u, u}
J] :=
{
preservesColimit := fun {K : J ⥤ C ⥤ D} =>
({
preserves := fun {c : Cocone K} (t : IsColimit c) =>
⟨by
apply evaluationJointlyReflectsColimits _ fun {k} => ?_
change IsColimit ((prod.functor.obj F ⋙ (evaluation _ _).obj k).mapCocone c)
let this := isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
apply IsColimit.mapCoconeEquiv _ this
apply (NatIso.ofComponents _ _).symm
· intro G
apply asIso (prodComparison ((evaluation C D).obj k) F G)
· intro G G'
apply prodComparison_natural ((evaluation C D).obj k) (𝟙 F)⟩ }) }
