evaluation_preservesColimit — Mathlib

English

For F: J ⥤ PresheafOfModules(R) and each Xᵒᵖ, evaluation at X preserves colimits: the colimit of F, evaluated at X, is the colimit of F evaluated at X.

Русский

Для F: J ⥤ PresheafOfModules(R) и каждого Xᵒᵖ операция вычисления в X сохраняет колимиты: колимит диаграммы внутри Evaluation при X равен колимиту исходной диаграммы при X.

LaTeX

$$$\\text{evaluationPreservesColimit }(F, X):\\; \\mathrm{Colim}_J (F)\\big|_X \\cong \\mathrm{Colim}_J (F|_X)$$$

Lean4

instance evaluation_preservesColimit (X : Cᵒᵖ) : PreservesColimit F (evaluation R X) :=
  preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F) (colimit.isColimit _)

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