English
Let F: J ⥤ Module_R be a diagram indexed by a filtered category J. Then there is a cocone over F whose vertex is the colimit of F, and whose legs are given by the canonical cocone morphism coconeMorphism F; this cocone is built inside the category of R-modules.
Русский
Пусть F: J ⥤ модульная категория модулей над R будет диаграммой, индексируемой фильтрованной категорией J. Тогда существует кокон над F, вершина которого есть колимит F, а ножки заданы каноническим кокон-монотонным отображением coconeMorphism F; этот кокон размещён внутри категории левых R-модулей.
LaTeX
$$$\text{colimitCocone}(F) = (\operatorname{colim} F,\ ι = \{ app := \mathrm{coconeMorphism} F \},\ \text{naturality})$$$
Lean4
/-- The cocone over the proposed colimit module. -/
def colimitCocone : Cocone F where
pt := colimit F
ι :=
{ app := coconeMorphism F
naturality := fun _ _' f =>
hom_ext <| LinearMap.coe_injective ((Types.TypeMax.colimitCocone (F ⋙ forget (ModuleCat R))).ι.naturality f) }
