finite_colimit_eq_finset_univ_sup

English

For a functor F : J ⥤ α with finite J, the colimit equals the supremum of the image: colimit F = sup_j F(j).

Русский

Для F : J ⥤ α с конечной диаграммой J ко-лимит равен наибольшему элементу образа: colimit F = sup_j F(j).

LaTeX

$$$\mathrm{colim} F = \bigvee_{j\in J} F(j)$$$

Lean4

/-- The colimit of a functor from a finite diagram into a `SemilatticeSup` with `OrderBot`
is the supremum of the objects in the image.
-/
theorem finite_colimit_eq_finset_univ_sup [SemilatticeSup α] [OrderBot α] (F : J ⥤ α) :
    colimit F = Finset.univ.sup F.obj :=
  (IsColimit.coconePointUniqueUpToIso (colimit.isColimit F) (finiteColimitCocone F).isColimit).to_eq

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