forget₂SemiRing_preservesFilteredColimits

English

The forgetful functor forget₂ from RingCat to SemiRingCat preserves filtered colimits.

Русский

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

LaTeX

$$PreservesFilteredColimits(forget₂ RingCat SemiRingCat)$$

Lean4

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

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