comp_reflectsFilteredColimits — Mathlib

English

If F and G reflect filtered colimits, then their composition F ⋙ G reflects filtered colimits.

Русский

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

LaTeX

$$$ReflectsFilteredColimitsOfSize (F ⋙ G)$$$

Lean4

instance comp_reflectsFilteredColimits (F : C ⥤ D) (G : D ⥤ E) [ReflectsFilteredColimitsOfSize.{w, w'} F]
    [ReflectsFilteredColimitsOfSize.{w, w'} G] : ReflectsFilteredColimitsOfSize.{w, w'} (F ⋙ G) where
  reflects_filtered_colimits _ := inferInstance

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