forget₂Ring_preservesFilteredColimits

English

The forgetful functor forget from CommRingCat to RingCat preserves filtered colimits.

Русский

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

LaTeX

$$PreservesFilteredColimits(forget CommRingCat RingCat)$$

Lean4

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

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