forget_preservesFilteredColimits — Mathlib

English

For every diagram F : J ⥤ MonCat with IsFiltered J, the forgetful functor to Type preserves the filtered colimit; i.e., colimits commute with forgetful functor.

Русский

Для каждого диаграммного F: J ⥤ MonCat с IsFiltered J, забывающий функтор в Type сохраняет фильтрованные колимиты; т.е. колимиты коммутируют с забывающим функтором.

LaTeX

$$$\mathrm{colim}_{J}(F \circ \mathrm{forget MonCat}) \cong \mathrm{forget MonCat}(\mathrm{colim}_{J} F)$$$

Lean4

@[to_additive]
instance forget_preservesFilteredColimits : PreservesFilteredColimits (forget MonCat.{u}) where
  preserves_filtered_colimits _ _
    _ :=
    ⟨fun {F} =>
      preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F)
        (Types.TypeMax.colimitCoconeIsColimit (F ⋙ forget MonCat.{u}))⟩

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