instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf

Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf

English

The functor from SheafOfModules to presheaf preserves finite limits in a reflectively exact way.

Русский

Функтор отражает конечные пределы в условиях точности.

LaTeX

$$$ (\mathrm{SheafOfModules.toSheaf} R). ReflectsFiniteLimits $$$

Lean4

noncomputable instance : ReflectsFiniteLimits (SheafOfModules.toSheaf.{v} R) where reflects _ _ _ := inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru