preservesColimit_of_createsColimit_and_hasColimit

English

Final reiteration: preserves colimits if creates and D has them.

Русский

Финальное повторение: сохраняет колимиты, если создает и D имеет их.

LaTeX

$$$$ \text{preservesColimits_of_createsColimits_and_hasColimits} (F) $$$$

Lean4

/-- `F` preserves the colimit of `K` if it creates the colimit and `K ⋙ F` has the colimit. -/
instance (priority := 100) preservesColimit_of_createsColimit_and_hasColimit (K : J ⥤ C) (F : C ⥤ D)
    [CreatesColimit K F] [HasColimit (K ⋙ F)] : PreservesColimit K F where
  preserves
    t :=
    ⟨IsColimit.ofIsoColimit (colimit.isColimit _)
        ((liftedColimitMapsToOriginal (colimit.isColimit _)).symm ≪≫
          (Cocones.functoriality K F).mapIso ((liftedColimitIsColimit (colimit.isColimit _)).uniqueUpToIso t))⟩
      -- see Note [lower instance priority]

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