English
Given a diagram D of cocones under curry.obj G j and a family of colimits Q j, together with a cocone c under G, one can assemble a cocone on the diagram formed by the cocone points D.coconePoints.
Русский
Для диаграммы cocone под curry.obj G и семейства ко-лимитов Q_j, а также для кокона c над G можно построить кокон над диаграммой, составляющей точки коконoв D.coconePoints.
LaTeX
$$$D : \\text{DiagramOfCocones}(\\text{curry.obj } G),\\ Q : \\forall j, \\text{IsColimit }(D.obj j),\\ c : \\text{Cocone } G \\;\\Rightarrow \\; \\text{Cocone } D.coconePoints$$$
Lean4
/-- Given a diagram `D` of colimit cocones under the `curry.obj G j`, and a cocone under `G`,
we can construct a cocone under the diagram consisting of the cocone points from `D`.
-/
@[simps]
def coconeOfCoconeCurry {D : DiagramOfCocones (curry.obj G)} (Q : ∀ j, IsColimit (D.obj j)) (c : Cocone G) :
Cocone D.coconePoints where
pt := c.pt
ι :=
{ app
j :=
(Q j).desc
{ pt := c.pt
ι := { app k := c.ι.app (j, k) } }
naturality {j _} _ := (Q j).hom_ext (by simp) }
