evaluation_preservesLimitsOfShape

English

Let C be a category and R be a functor from C^op to rings. For any small category J and any presheaf of modules F: J ⥤ PresheafOfModules(R), the evaluation at X, ev_X, preserves limits of shape J.

Русский

Пусть C — категория, R — функтор C^op → RingCat. Пусть J — малая категория, и F: J ⥤ PresheafOfModules(R). Тогда оценка в точке X, ev_X, сохраняет пределы формы J.

LaTeX

$$$\\mathrm{ev}_X: \\mathrm{PresheafOfModules}(R) \\to \\mathrm{ModuleCat}(R(X))$ preserves limits of shape $J$.$$

Lean4

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

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