instPreservesFiniteLimitsSheafOfModulesSheafification

English

The sheafification functor PresheafOfModules.sheafification preserves finite limits.

Русский

Функтор шейификации PresheafOfModules сохраняет конечные пределы.

LaTeX

$$$ \text{PreservesFiniteLimits} (PresheafOfModules.sheafification α)$$$

Lean4

noncomputable instance : PreservesFiniteLimits (sheafification.{v} α) :=
  preservesFiniteLimits_of_reflects_of_preserves (sheafification.{v} α) (SheafOfModules.toSheaf.{v} R)

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