forget_preservesFilteredColimits — Mathlib

English

The forgetful functor forget from RingCat to its underlying category preserves filtered colimits.

Русский

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

LaTeX

$$PreservesFilteredColimits(forget RingCat)$$

Lean4

instance forget_preservesFilteredColimits : PreservesFilteredColimits (forget RingCat.{u}) :=
  Limits.comp_preservesFilteredColimits (forget₂ RingCat SemiRingCat) (forget SemiRingCat.{u})

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