comp_preservesFilteredColimits — Mathlib

English

If F and G preserve filtered colimits, then F ⋙ G preserves filtered colimits.

Русский

Если F и G сохраняют отфильтрованные колимиты, то последовательное применение F ⋙ G сохраняет отфильтрованные колимиты.

LaTeX

$$$PreservesFilteredColimitsOfSize.{w,w'} (F ⋙ G)$$$

Lean4

instance comp_preservesFilteredColimits (F : C ⥤ D) (G : D ⥤ E) [PreservesFilteredColimitsOfSize.{w, w'} F]
    [PreservesFilteredColimitsOfSize.{w, w'} G] : PreservesFilteredColimitsOfSize.{w, w'} (F ⋙ G) where
  preserves_filtered_colimits _ := inferInstance

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