preservesColimit_comp_of_createsColimit

English

If F creates colimits and G preserves colimits of shape J on K, then K ⋙ F preserves colimits after composing with G.

Русский

Если F создаёт колимиты и G сохраняет колимиты формы J на K, то K ⋙ F сохраняет колимиты после композиции с G.

LaTeX

$$$[\text{CreatesColimit } K F] \wedge [\text{PreservesColimit } K (F \circ G)] \Rightarrow \mathrm{PreservesColimit } (K \circ F) G$$$

Lean4

instance preservesColimit_comp_of_createsColimit [CreatesColimit K F] [PreservesColimit K (F ⋙ G)] :
    PreservesColimit (K ⋙ F) G where
  preserves
    hc :=
    ⟨IsColimit.ofIsoColimit (isColimitOfPreserves (F ⋙ G) (liftedColimitIsColimit hc))
        ((Functor.mapCoconeMapCocone (liftColimit hc)).symm ≪≫
          (Cocones.functoriality _ _).mapIso (liftedColimitMapsToOriginal hc))⟩

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