forget_preservesFilteredColimits — Mathlib

English

The forgetful functor forget GrpCat to Type preserves filtered colimits.

Русский

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

LaTeX

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

Lean4

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

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