English
The directLimitCocone is the cocone on the diagram directLimitDiagram with pt = ModuleCat.of R (DirectLimit G f) and arrows given by universal maps, forming a cocone.
Русский
Кокон directLimitCocone является коконом над диаграммой directLimitDiagram со струной-точкой pt = ModuleCat.of R (DirectLimit G f) и стрелами, заданными через универсальные отображения.
LaTeX
$$$\\text{directLimitCocone}: \\text{Cocone}(\\text{directLimitDiagram } G f)$$$
Lean4
/-- The `Cocone` on `directLimitDiagram` corresponding to
the unbundled `directLimit` of modules.
In `directLimitIsColimit` we show that it is a colimit cocone. -/
@[simps]
def directLimitCocone : Cocone (directLimitDiagram G f)
where
pt := ModuleCat.of R <| DirectLimit G f
ι :=
{ app := fun x => ofHom (Module.DirectLimit.of R ι G f x)
naturality := fun _ _ hij => by
ext
exact DirectLimit.of_f }
