cocone — Mathlib

English

Under similar hypotheses to initialSeg results, α-shaped colimits exist in C when α is obtained as an initial segment of J.

Русский

При аналогичных предположениях существую колимиты формы α в C, если α получается как начальный сегмент J.

LaTeX

$$$\mathrm{HasColimitsOfShape}(\alpha, C)$$$

Lean4

/-- When `f : α <i β` and a functor `F : β ⥤ C`, this is the cocone
for `f.monotone.functor ⋙ F : α ⥤ C` whose point if `F.obj f.top`. -/
@[simps]
def cocone {α β : Type*} [PartialOrder α] [PartialOrder β] (f : α <i β) {C : Type*} [Category C] (F : β ⥤ C) :
    Cocone (f.monotone.functor ⋙ F) where
  pt := F.obj f.top
  ι :=
    { app i := F.map (homOfLE (f.lt_top i).le)
      naturality i j
        f := by
        dsimp
        rw [← F.map_comp, comp_id]
        rfl }

Похожие утверждения