English
For a functor G: J ⥤ K ⥤ C, the limit over J of G is naturally isomorphic to curry.obj (Prod.swap K J ⋙ uncurry.obj G) composed with lim. This expresses a canonical interchange of limits under currying.
Русский
Для функторa G: J ⥤ K ⥤ C предел над J от G естественным образом изоморфен curry.obj (Prod.swap K J ⋙ uncurry.obj G) ⋙ lim, выражая каноническую перестановку пределов при каррировании.
LaTeX
$$$\\text{limit } G \\cong \\mathrm{curry.obj}\\big(\\mathrm{Prod.swap}\\;K\\;J \\;\\circ\\; \\mathrm{uncurry.obj}\;G\\big) \\;\\circ\\; \\mathrm{lim}.$$$
Lean4
/-- For a functor `G : J ⥤ K ⥤ C`, its limit `K ⥤ C` is given by `(G' : K ⥤ J ⥤ C) ⋙ lim`.
Note that this does not require `K` to be small.
-/
@[simps!]
def limitIsoSwapCompLim [HasLimitsOfShape J C] (G : J ⥤ K ⥤ C) :
limit G ≅ curry.obj (Prod.swap K J ⋙ uncurry.obj G) ⋙ lim :=
limitIsoFlipCompLim G ≪≫ isoWhiskerRight (flipIsoCurrySwapUncurry _) _
