evaluation_preservesColimitsOfShape

English

The presheaf category PresheafOfModules(R) has finite colimits; for any small finite shape J, HasColimitsOfShape J holds in PresheafOfModules(R).

Русский

Категория прешейфов PresheafOfModules(R) имеет конечные колимиты; для любой малой формы J конечной формы соблюдается HasColimitsOfShape J.

LaTeX

$$$\\text{HasFiniteColimits}\\,(\\text{PresheafOfModules}(R))$$$

Lean4

noncomputable instance evaluation_preservesColimitsOfShape (X : Cᵒᵖ) :
    PreservesColimitsOfShape J (evaluation R X : PresheafOfModules.{v} R ⥤ _) where

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