instAdditiveFunctorColim

Mathlib.Algebra.Category.Grp.AB

URI: https://scilib.ai/kg/mathlib#instAdditiveFunctorColim

English

FGModuleCat(k) has finite limits.

Русский

FGModuleCat(k) имеет конечные пределы.

LaTeX

$$$\operatorname{HasFiniteLimits}( FGModuleCat(k) )$$$

Lean4

instance {J C : Type*} [Category J] [Category C] [HasColimitsOfShape J C] [Preadditive C] :
    (colim (J := J) (C := C)).Additive where

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

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

Разделы

Аффилиация

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