toPresheaf_preservesFiniteLimits

Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

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

English

The functor toPresheaf(R) preserves finite limits.

Русский

Функтор toPresheaf(R) сохраняет конечные пределы.

LaTeX

$$$\\text{PreservesFiniteLimits}(\\mathrm{toPresheaf}(R)).$$$

Lean4

noncomputable instance toPresheaf_preservesFiniteLimits : PreservesFiniteLimits (toPresheaf.{v} R) where

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

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

Разделы

Аффилиация

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