forget_preservesFilteredColimits — Mathlib

English

The forgetful functor from Module_R to AddCommGrp preserves filtered colimits.

Русский

Функтор забывания из Module_R в AddCommGrp сохраняет фильтрованные колимиты.

LaTeX

$$$\text{PreservesFilteredColimits}(\mathrm{forget}: \text{ModuleCat }R \to \text{AddCommGrpCat})$$$

Lean4

instance forget_preservesFilteredColimits : PreservesFilteredColimits (forget (ModuleCat.{u} R)) :=
  Limits.comp_preservesFilteredColimits (forget₂ (ModuleCat R) AddCommGrpCat) (forget AddCommGrpCat)

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