forget₂Mon_preservesFilteredColimits

English

The forgetful functor from SemiRingCat to MonCat preserves filtered colimits after composing with forget from SemiRingCat to MonCat.

Русский

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

LaTeX

$$PreservesFilteredColimits( forget₂ SemiRingCat MonCat )$$

Lean4

instance forget₂Mon_preservesFilteredColimits : PreservesFilteredColimits (forget₂ SemiRingCat MonCat.{u}) where
  preserves_filtered_colimits
    {J hJ1 _} :=
    letI : Category J := hJ1
    {
      preservesColimit := fun {F} =>
        preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F)
          (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ SemiRingCat MonCat.{u})) }

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