instPreservesColimitsOfShapeTopCatForgetOfSmallOfHasLimitsOfShapeOpposite

English

If C has limits, then the category of sheafed spaces over C has all small colimits.

Русский

Если в C существуют пределы, то у категории SheafedSpace(C) есть все малые колимиты.

LaTeX

$$$\text{If }\mathrm{HasLimits}(C)\text{ then }\mathrm{HasColimits}(\mathrm{SheafedSpace}(C))$$$

Lean4

instance (J : Type w) [Category.{w'} J] [Small.{v} J] [HasLimitsOfShape Jᵒᵖ C] :
    PreservesColimitsOfShape J (forget.{_, _, v} C) :=
  Limits.comp_preservesColimitsOfShape forgetToPresheafedSpace (PresheafedSpace.forget C)

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