evaluation_preservesFiniteLimits — Mathlib

English

For each X in C, ev_X preserves finite limits: the functor ev_X: PresheafOfModules(R) → ModuleCat(R(X)) preserves finite limits.

Русский

Для каждого X в C оценка ev_X сохраняет конечные пределы: ev_X: PresheafOfModules(R) → ModuleCat(R(X)) сохраняет конечные пределы.

LaTeX

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

Lean4

noncomputable instance evaluation_preservesFiniteLimits (X : Cᵒᵖ) : PreservesFiniteLimits (evaluation.{v} R X) where

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