instHasColimitObjFunctorConstInitial

English

If a category C has an initial object ⊥, then for any index category J the constant diagram with value ⊥ has a colimit; concretely, the apex is ⊥ and the structure maps are given by the canonical initial arrows to each component.

Русский

Если у категории C есть начальный объект ⊥, то для любой индексной категории J константный диаграмме, заданной значением ⊥, существует колимит; в частности вершина колимита равна ⊥, а конечно-структурные отображения задаются каноническимиMorphisms from начального объекта ко всем компонентам.

LaTeX

$$$$\\mathrm{HasColimit}\\left((\\mathrm{const}\\ J)\\,(\\perp_C)\\right)$$$$

Lean4

instance {J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C] :
    HasColimit ((CategoryTheory.Functor.const J).obj (⊥_ C)) :=
  HasColimit.mk
    { cocone :=
        { pt := ⊥_ C
          ι := { app := fun _ => initial.to _ } }
      isColimit := { desc := fun _ => initial.to _ } }

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