comp_preservesColimit — Mathlib

English

If F preserves colimits of shape J and G preserves colimits of shape J, then F ⋙ G preserves colimits of shape J.

Русский

Если F сохраняет колимиты формы J и G сохраняет колимиты формы J, тогда F ⋙ G сохраняет колимиты формы J.

LaTeX

$$$$\mathrm{PreservesColimitsOfShape}(J,F) \land \mathrm{PreservesColimitsOfShape}(J,G) \Rightarrow \mathrm{PreservesColimitsOfShape}(J,F\circ G).$$$$

Lean4

instance comp_preservesColimit [PreservesColimit K F] [PreservesColimit (K ⋙ F) G] : PreservesColimit K (F ⋙ G) where
  preserves hc := ⟨isColimitOfPreserves G (isColimitOfPreserves F hc)⟩

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