of_isColimit — Mathlib

English

Given a cocone c over F : J ⥤ C with IsColimit hc, and a morphism h specifying W, one gets W.colimitsOfShape J (c.ι.app ⊥).

Русский

При наличии кокона c над F : J ⥤ C с IsColimit hc и данных h, получаем W.colimitsOfShape J (c.ι.app ⊥).

LaTeX

$$W.colimitsOfShape J (c.ι.app ⊥)$$

Lean4

theorem of_isColimit {J : Type*} [Preorder J] [OrderBot J] {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c)
    (h : ∀ (j : J), W (F.map (homOfLE bot_le : ⊥ ⟶ j))) : W.colimitsOfShape J (c.ι.app ⊥) :=
  .mk' _ _ _ _ (isColimitConstCocone J (F.obj ⊥)) hc
    { app k := F.map (homOfLE bot_le)
      naturality _ _
        _ := by
        dsimp
        rw [Category.id_comp, ← Functor.map_comp]
        rfl }
    h _ (by simp)

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