functorCategoryHasColimit — Mathlib

English

There is an instance giving HasColimit for functor categories when each component has a colimit

Русский

Существует инстанс, обеспечивающий HasColimit для категорий функторов, если для каждого компонента существует колимит

LaTeX

$$$\\text{HasColimit } F$$$

Lean4

instance functorCategoryHasColimit (F : J ⥤ K ⥤ C) [∀ k, HasColimit (F.flip.obj k)] : HasColimit F :=
  HasColimit.mk
    { cocone := combineCocones F fun _ => getColimitCocone _
      isColimit := combinedIsColimit _ _ }

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