English
The cone constructed from HasLimit CurryCompLim is a limit cone; the isLimit proof is provided by a standard lifting argument.
Русский
Конус, построенный через HasLimit CurryCompLim, является пределом; доказательство isLimit следует из стандартного подъема.
LaTeX
$$$\text{isLimitConeOfHasLimitCurryCompLim } G$.$$
Lean4
/-- Given a functor `G : J × K ⥤ C` such that `(curry.obj G ⋙ colim)` makes sense and has a colimit,
we can construct a cocone under `G` with `colimit (curry.obj G ⋙ colim)` as a cocone point -/
noncomputable def coconeOfHasColimitCurryCompColim : Cocone G :=
let Q : DiagramOfCocones (curry.obj G) := .mkOfHasColimits _
{ pt := colimit (curry.obj G ⋙ colim),
ι :=
{ app x := (Q.obj x.fst).ι.app x.snd ≫ colimit.ι (curry.obj G ⋙ colim) x.fst
naturality
{x y} := fun ⟨f₁, f₂⟩ ↦ by
have := (Q.obj y.1).w f₂
dsimp [Q] at this ⊢
rw [← colimit.w (F := curry.obj G ⋙ colim) (f := f₁), Category.assoc, Category.comp_id, Prod.fac' (f₁, f₂),
G.map_comp_assoc, ← curry_obj_map_app, ← curry_obj_obj_map]
dsimp
simp [ι_colimMap_assoc, curry_obj_map_app, reassoc_of% this] } }
