reflectsColimitsOfShape — Mathlib

English

For rings R and shape J with HasColimitsOfSize on AddCommGrpCat, forget₂ : ModuleCat R → AddCommGrpCat preserves colimits of shape J.

Русский

Для колец R и формы J с HasColimitsOfSize на AddCommGrpCat забывающая функция forget₂: ModuleCat R → AddCommGrpCat сохраняет колимиты формы J.

LaTeX

$$$$ \mathrm{forget₂} : \mathrm{ModuleCat}(R) \to \mathrm{AddCommGrpCat} \text{ preserves colimits of shape } J $$$$

Lean4

noncomputable instance reflectsColimitsOfShape [HasColimitsOfShape J AddCommGrpCat.{w'}] :
    ReflectsColimitsOfShape J (forget₂ (ModuleCat.{w'} R) AddCommGrpCat) where

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