English
Let R be a ring. The forgetful functor from the category of R-modules to the category of additive commutative groups preserves colimits of diagrams of a fixed size (as long as those colimits exist). In particular, for any diagram of modules with a finite/size-bounded shape, the colimit computed in the module category remains a colimit after forgetting to abelian groups.
Русский
Пусть R — кольцо. Функтор забывания из категории R-модулей в категорию аддитивных абелевых групп сохраняет колимиты диаграмм заданного размера (при условии существования таких колимитов). В частности, для любой диаграммы модулей с ограниченной формой колимита, колимит в категории модулей сохраняется после забывания до абелевых групп.
LaTeX
$$$\\forall J$ (small) $\\forall F: J \\to \\mathrm{Mod}_R$, \\; \\operatorname{Colim}_J F \\;\\text{exists in } \\mathrm{Mod}_R \\;\\Rightarrow\\; \\mathrm{Forget}_R\\bigl(\\operatorname{Colim}_J F\\bigr) \\cong \\operatorname{Colim}_J(\\mathrm{Forget}_R \\circ F) . $$$
Lean4
noncomputable instance [HasColimitsOfSize.{u, v} AddCommGrpMax.{w, w'}] :
PreservesColimitsOfSize.{u, v} (forget₂ (ModuleCat.{max w w'} R) AddCommGrpCat) where
