English
There is an isomorphism between colimit of G and colimit of curry.obj G ⋙ colim.
Русский
Существует изоморфизм между колимитом G и колимитом curry.obj G ⋙ colim.
LaTeX
$$$\text{colimitIsoColimitCurryCompColim } G : \colimit G \cong \colimit (\text{curry.obj } G \circ \mathrm{colim})$$$
Lean4
/-- The Fubini theorem for a functor `G : J × K ⥤ C`,
showing that the colimit of `G` can be computed as
the colimit of the colimits of the functors `G.obj (j, _)`.
-/
noncomputable def colimitIsoColimitCurryCompColim : colimit G ≅ colimit (curry.obj G ⋙ colim) :=
by
have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
haveI : Limits.HasColimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasColimit_of_iso i.symm
trans colimit (uncurry.obj ((@curry J _ K _ C _).obj G))
· apply HasColimit.isoOfNatIso i
· exact colimitUncurryIsoColimitCompColim ((@curry J _ K _ C _).obj G)
