hasColimit_iff_hasInitial_cocone — Mathlib

English

A functor F has a colimit if and only if cocone F has an initial object; equivalently, HasColimit F ↔ HasInitial (Cocone F).

Русский

Существование колимита для F эквивалентно существованию инициализации для Cocone F; HasColimit F ↔ HasInitial (Cocone F).

LaTeX

$$$\\text{HasColimit}(F) \\iff \\text{HasInitial}(\\text{Cocone}(F))$$$

Lean4

theorem hasColimit_iff_hasInitial_cocone (F : J ⥤ C) : HasColimit F ↔ HasInitial (Cocone F) :=
  ⟨fun _ => (Cocone.isColimitEquivIsInitial _ (colimit.isColimit F)).hasInitial, fun h =>
    haveI : HasInitial (Cocone F) := h
    ⟨⟨⟨⊥_ _, (Cocone.isColimitEquivIsInitial _).symm initialIsInitial⟩⟩⟩⟩

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