forget_preservesFilteredColimits — Mathlib

English

Let F : J ⥤ CommSemiRingCat be a diagram with J small and IsFiltered J. The forgetful functor forget CommSemiRingCat : CommSemiRingCat ⥤ SemiRingCat preserves filtered colimits; i.e., the relevant colimits are computed in SemiRingCat after forgetting.

Русский

Пусть F : J ⥤ CommSemiRingCat, J маленькая и IsFiltered J. Забвение Functor forget CommSemiRingCat сохраняет фильтрованные колимиты; то есть колимит вычисляется в SemiRingCat после забывания.

LaTeX

$$$ \\operatorname{forget CommSemiRingCat\\to SemiRingCat}\\text{ preserves filtered colimits: } \\operatorname{Colim}_J F \\;\\text{in } CommSemiRingCat \\mapsto \\operatorname{Colim}_J (\\mathrm{forget}\\circ F) \\text{ in SemiRingCat}$$$

Lean4

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

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