English
Final articulation of the limit iso equivalence with curry/lim interplay.
Русский
Финальная формулировка соотношения предельного изоморфизма через карри/лим.
LaTeX
$$$\text{eq1}_{final}: \text{limitIsoLimitCurryCompLim } G = \text{trans}(\text{HasLimit isoOfNatIso}, \text{limitUncurryIsoLimitCompLim})$$$
Lean4
/-- The Fubini theorem for a functor `G : J × K ⥤ C`,
showing that the limit of `G` can be computed as
the limit of the limits of the functors `G.obj (j, _)`.
-/
noncomputable def limitIsoLimitCurryCompLim : limit G ≅ limit (curry.obj G ⋙ lim) :=
by
have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
haveI : Limits.HasLimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasLimit_of_iso i
trans limit (uncurry.obj ((@curry J _ K _ C _).obj G))
· apply HasLimit.isoOfNatIso i
· exact limitUncurryIsoLimitCompLim ((@curry J _ K _ C _).obj G)
