preservesColimitsOfShape_of_final

English

If F is final and G preserves colimits, then F ⋙ G preserves colimits.

Русский

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

LaTeX

$$$$ \text{PreservesColimitsOfShape}(F \circ G, H) \Leftarrow \text{PreservesColimitsOfShape} (C, H). $$$$

Lean4

theorem preservesColimitsOfShape_of_final {B : Type u₄} [Category.{v₄} B] (H : E ⥤ B) [PreservesColimitsOfShape C H] :
    PreservesColimitsOfShape D H where preservesColimit := preservesColimit_of_comp F

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