instHasColimitsOfShape — Mathlib

English

For any shape J and any category C, the category of presheafed spaces over C has all colimits of shape J. Given a diagram F: J → PresheafedSpace(C), its colimit is obtained from a canonical colimit cocone, and this cocone satisfies the universal property of a colimit.

Русский

Для любой формы J и любой категории C категория пространств с прешебаф-подстановками над C имеет все колимиты формы J. Для диаграммы F: J → PresheafedSpace(C) колимит получается из канонического кокона колимита, и этот кокон удовлетворяет универсальной свойству колимита.

LaTeX

$$$\forall F: J \to \mathsf{PresheafedSpace}(C),\; \exists\, \mathrm{colim}_J F \in \mathsf{PresheafedSpace}(C)\text{ с коконом } \mathrm{colimitCocone} F,\; \mathrm{colimitCocone} F\ \text{есть колимитный кокон.}$$$

Lean4

instance : HasColimitsOfShape J (PresheafedSpace.{_, _, v} C) where
  has_colimit F := ⟨colimitCocone F, colimitCoconeIsColimit F⟩

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