instPreservesFiniteLimitsModuleCatForget₂

Mathlib.Algebra.Category.FGModuleCat.Limits

URI: https://scilib.ai/kg/mathlib#FGModuleCat.instPreservesFiniteLimitsModuleCatForget₂

English

The forget₂ functor preserves finite limits.

Русский

Забывающий функтор сохраняет конечные пределы.

LaTeX

$$$\operatorname{PreservesFiniteLimits}(\operatorname{forget}_2( FGModuleCat(k), ModuleCat(k) ))$$$

Lean4

instance : PreservesFiniteLimits (forget₂ (FGModuleCat k) (ModuleCat.{v} k)) where
  preservesFiniteLimits _ _ _ := inferInstance

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

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

Разделы

Аффилиация

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