instPreservesColimitAddCommGrpCatForget₂

English

The forgetful functor forget₂ (ModuleCat R) AddCommGrpCat reflects colimits, i.e., a cocone is a colimit in ModuleCat R if its image under the forgetful functor is a colimit in AddCommGrpCat.

Русский

Забывающая функция forget₂ отражает колимит: кокон является колимитом в ModuleCat R тогда и только тогда, когда его образ в AddCommGrpCat является колимитом.

LaTeX

$$$$ \text{ReflectsColimitsOfShape forget₂} $$$$

Lean4

noncomputable instance : PreservesColimit F (forget₂ _ AddCommGrpCat) :=
  preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F) (colimit.isColimit _)

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