forget₂AddCommGroup_preservesFilteredColimits

English

The forgetful functor from Module_R to AddCommGrp preserves filtered colimits; equivalently, filtered colimits computed in Module_R correspond to those computed after forgetting the module structure to abelian groups.

Русский

Функтор забывания из Module_R в AddCommGrp сохраняет фильтрованные колимиты; эквивалентно тому, что колимиты фильтрованных диаграмм совпадают после забывания модуля по группе.

LaTeX

$$$\text{PreservesFilteredColimits} (\mathrm{forget}_{\mathrm{AddCommGrpCat}} \circ \mathrm{forget} )$$$

Lean4

instance forget₂AddCommGroup_preservesFilteredColimits :
    PreservesFilteredColimits (forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u}) where
  preserves_filtered_colimits _ _
    _ :=
    {
      preservesColimit := fun {F} =>
        preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit F)
          (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u})) }

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