instHasColimits — Mathlib

English

If the ambient category C has all limits, then the category of presheafed spaces valued in C has all small colimits.

Русский

Если в категории C существуют все пределы, тогда категория прешефдов пространства над C имеет все малые колимиты.

LaTeX

$$$\forall C [\mathsf{Category}\,C], [\mathsf{HasLimits}\,C] \Rightarrow \mathsf{HasColimits}(\mathrm{PresheafedSpace}\,C)$$$

Lean4

/-- When `C` has limits, the category of presheafed spaces with values in `C` itself has colimits.
-/
instance instHasColimits [HasLimits C] : HasColimits (PresheafedSpace.{_, _, v} C) :=
  ⟨fun {_ _} => ⟨fun {F} => ⟨colimitCocone F, colimitCoconeIsColimit F⟩⟩⟩

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