instSmallColimitType — Mathlib

English

For any diagram F: J → Type u, the diagram has a colimit in Type u if and only if its colimit type F.ColimitType is small. Equivalently, HasColimit F is equivalent to Small(F.ColimitType).

Русский

Для любой диаграммы F: J → Type u существование колимита в категорию типов эквивалентно тому, что колимитный тип F.ColimitType малый. Иными словами, HasColimit F эквивалентно Small(F.ColimitType).

LaTeX

$$$$ HasColimit F \iff Small\ F.ColimitType. $$$$

Lean4

instance [Small.{u} J] (F : J ⥤ Type u) : Small.{u} (F.ColimitType) :=
  small_of_surjective Quot.mk_surjective

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