forget_preservesFilteredColimits — Mathlib

English

The forgetful functor forget CommGrpCat to Type preserves filtered colimits.

Русский

Забывающий функтор forget CommGrpCat в Type сохраняет фильтрованные колимиты.

LaTeX

$$$$ \mathrm{PreservesFilteredColimits}(\mathrm{forget CommGrpCat}) $$$$

Lean4

@[to_additive]
noncomputable instance forget_preservesFilteredColimits : PreservesFilteredColimits (forget CommGrpCat.{u}) :=
  Limits.comp_preservesFilteredColimits (forget₂ CommGrpCat GrpCat) (forget GrpCat.{u})

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