English
The cone built from HasLimit CurryCompLim is a limit cone; i.e., the cone c with apex lim and legs provided by limit projections is universal.
Русский
Конус, построенный из HasLimit для CurryCompLim, является пределом; то есть конус с апексом lim и мономерами, заданными проекциями лимита, является универсальным.
LaTeX
$$$\text{IsLimit}(\text{coneOfHasLimitCurryCompLim } G)$.$$
Lean4
/-- Given a functor `G : J × K ⥤ C` such that `(curry.obj G ⋙ lim)` makes sense and has a limit,
we can construct a cone over `G` with `limit (curry.obj G ⋙ lim)` as a cone point -/
noncomputable def coneOfHasLimitCurryCompLim : Cone G :=
let Q : DiagramOfCones (curry.obj G) := .mkOfHasLimits _
{ pt := limit (curry.obj G ⋙ lim),
π :=
{ app x := limit.π (curry.obj G ⋙ lim) x.fst ≫ (Q.obj x.fst).π.app x.snd
naturality
{x y} := fun ⟨f₁, f₂⟩ ↦ by
have := (Q.obj x.1).w f₂
dsimp [Q] at this ⊢
rw [← limit.w (F := curry.obj G ⋙ lim) (f := f₁)]
dsimp
simp only [Category.assoc, Category.id_comp, Prod.fac (f₁, f₂), G.map_comp, limMap_π, curry_obj_map_app,
reassoc_of% this] } }
