English
For a function U : ι → α into a complete lattice, there is a natural cone morphism from every diagram Object to the supremum iSup U. Concretely, single i maps by le_iSup i, and pair i j factors through inf_left then le_iSup i.
Русский
Для функции U : ι → α в полную решётку существует естественная стрелка-конос над каждому объекту диаграммы к наивному пределу iSup U. Конкретно, для единственных i применим le_iSup i, а для пары i j композиция через inf_left и le_iSup i.
LaTeX
$$$\mathrm{cocone}_{\iota\_App}(U) : o \mapsto \mathrm{diagramObj}\,U\,o \to iSup\,U, \\ \text{with } \mathrm{cocone}_{\iota\_App}(\mathrm{single\;i}) = \mathrm{homOfLE}(\mathrm{le\_iSup}(U,i)), \\ \mathrm{cocone}_{\iota\_App}(\mathrm{pair\;i\;j}) = \mathrm{homOfLE}(\inf\le\text{Left}) \circ \mathrm{homOfLE}(\mathrm{le\_iSup}(U,i)).$$$
Lean4
/-- Auxiliary definition for `cocone`. -/
def coconeιApp : ∀ o : Pairwise ι, diagramObj U o ⟶ iSup U
| single i => homOfLE (le_iSup U i)
| pair i _ => homOfLE inf_le_left ≫ homOfLE (le_iSup U i)
