toPresheaf_preservesColimit — Mathlib

English

The forgetful functor to presheaves preserves colimits: colimits of presheaves with module structure are computed by forgetting the module operations and taking the corresponding colimits as presheaves.

Русский

Функтор забывания до прешейфов сохраняет колимиты: колимиты прешейфов с модульной структурой вычисляются после забывания модульной структуры.

LaTeX

$$$\\text{toPresheafPreservesColimit}:\\; \\mathrm{PresheafOfModules}(R) \\to \\mathrm{Presheaf}( , )\\; \\text{preserves colimits}$$$

Lean4

instance toPresheaf_preservesColimit : PreservesColimit F (toPresheaf R) :=
  preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F)
    (Limits.evaluationJointlyReflectsColimits _
      (fun X => isColimitOfPreserves (evaluation R X ⋙ forget₂ _ AddCommGrpCat) (isColimitColimitCocone F)))

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