English
The isColimit instance for the uncurry-cone construction lifts to the original cone's colimit property.
Русский
Инстанс IsColimit для конструкции uncurry-конуса поднимает свойство колимита к исходному конусу.
LaTeX
$$$\text{IsColimit}(\text{coneOfConeUncurry } Q c) \Rightarrow \text{IsColimit}(c).$$$
Lean4
/-- The Fubini theorem for a functor `F : J ⥤ K ⥤ C`,
showing that the limit of `uncurry.obj F` can be computed as
the limit of the limits of the functors `F.obj j`.
-/
noncomputable def limitUncurryIsoLimitCompLim : limit (uncurry.obj F) ≅ limit (F ⋙ lim) :=
by
let c := limit.cone (uncurry.obj F)
let P : IsLimit c := limit.isLimit _
let G := DiagramOfCones.mkOfHasLimits F
let Q : ∀ j, IsLimit (G.obj j) := fun j => limit.isLimit _
have Q' := coneOfConeUncurryIsLimit Q P
have Q'' := limit.isLimit (F ⋙ lim)
exact IsLimit.conePointUniqueUpToIso Q' Q''
