forget₂Mon_preservesFilteredColimits

English

The forgetful functor from CommMonCat to MonCat preserves filtered colimits.

Русский

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

LaTeX

$$$\mathrm{forget MonCat}(\mathrm{colim}_{J} F) \cong \mathrm{colim}_{J}(\mathrm{forget MonCat} \circ F)$$$

Lean4

@[to_additive forget₂AddMonPreservesFilteredColimits]
noncomputable instance forget₂Mon_preservesFilteredColimits : PreservesFilteredColimits (forget₂ CommMonCat MonCat.{u})
    where
  preserves_filtered_colimits _ _
    _ :=
    ⟨fun {F} =>
      preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F)
        (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ CommMonCat MonCat.{u}))⟩

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