colimitIsoSwapCompColim — Mathlib

English

For a functor G: J ⥤ K ⥤ C, the colimit over J of G is naturally isomorphic to curry.obj (Prod.swap K J ⋙ uncurry.obj G) composed with colim.

Русский

Для функторa G: J ⥤ K ⥤ C колимит над J от G естественным образом изоморфен curry.obj (Prod.swap K J ⋙ uncurry.obj G) ⋙ colim.

LaTeX

$$$\\text{colimit } G \\cong \\mathrm{curry.obj}\\big(\\mathrm{Prod.swap}\\;K\\;J ⋙ \\mathrm{uncurry.obj}\\;G\\big) ⋙ \\mathrm{colim}.$$$

Lean4

/-- For a functor `G : J ⥤ K ⥤ C`, its colimit `K ⥤ C` is given by `(G' : K ⥤ J ⥤ C) ⋙ colim`.
Note that this does not require `K` to be small.
-/
@[simps!]
def colimitIsoSwapCompColim [HasColimitsOfShape J C] (G : J ⥤ K ⥤ C) :
    colimit G ≅ curry.obj (Prod.swap K J ⋙ uncurry.obj G) ⋙ colim :=
  colimitIsoFlipCompColim G ≪≫ isoWhiskerRight (flipIsoCurrySwapUncurry _) _

Похожие утверждения