instPreservesFiniteLimitsSheafAddCommGrpCatToSheaf

English

There is an instance asserting that the functor SheafOfModules.toSheafR preserves finite limits.

Русский

Существует экземпляр, утверждающий, что функтор SheafOfModules.toSheaf R сохраняет конечные пределы.

LaTeX

$$$\operatorname{PreservesFiniteLimits}\big(\mathrm{SheafOfModules.toSheaf}(R)\big)$$$

Lean4

noncomputable instance : PreservesFiniteLimits (SheafOfModules.toSheaf.{v} R) :=
  preservesFiniteLimits_of_reflects_of_preserves _ (sheafToPresheaf _ _)

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