English
There is a canonical isomorphism between the limit over J × K and the limit over the swapped shape, i.e., the limit of G with respect to both indices equals the limit of G with the swapped order, presented via curry and lim
Русский
Существует каноническое изоморфизм между пределом над J × K и пределом над переставленной формой, то есть предел G по двум индексам эквивалентен предел по переставленному порядку, выраженный через curry и lim
LaTeX
$$$\\lim (\\mathrm{curry.obj} (\\mathrm{Prod.swap}\\ K\\ J \\;\\gg\\; G) \\;\\gg\\; \\lim) \\cong \\lim (\\mathrm{curry.obj}\\ G \\;\\gg\\; \\lim)\\;$$
Lean4
/-- A variant of the Fubini theorem for a functor `G : J × K ⥤ C`,
showing that $\lim_k \lim_j G(j,k) ≅ \lim_j \lim_k G(j,k)$.
-/
noncomputable def limitCurrySwapCompLimIsoLimitCurryCompLim :
limit (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) ≅ limit (curry.obj G ⋙ lim) :=
calc
limit (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) ≅ limit (Prod.swap K J ⋙ G) := (limitIsoLimitCurryCompLim _).symm
_ ≅ limit G := (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl _))
_ ≅ limit (curry.obj G ⋙ lim) := limitIsoLimitCurryCompLim _
