whiskeringLeft_preservesColimitsOfShape

English

For any J, if HasColimitsOfShape J D holds, then whiskeringLeft preserves colimits of shape J.

Русский

Для любого J, если существуют колимиты формы J в D, то whiskeringLeft сохраняет колимиты формы J.

LaTeX

$$$\forall J\, [\text{Category } J], [\text{HasColimitsOfShape } J D] \Rightarrow \mathrm{PreservesColimitsOfShape}(J, (\mathrm{whiskeringLeft}\; C\; E\; D).\mathrm{obj} F)$$$

Lean4

instance whiskeringLeft_preservesColimitsOfShape (J : Type u) [Category.{v} J] [HasColimitsOfShape J D] (F : C ⥤ E) :
    PreservesColimitsOfShape J ((whiskeringLeft C E D).obj F) :=
  ⟨fun {K} =>
    ⟨fun c {hc} =>
      ⟨by
        apply evaluationJointlyReflectsColimits
        intro Y
        change IsColimit (((evaluation E D).obj (F.obj Y)).mapCocone c)
        exact isColimitOfPreserves _ hc⟩⟩⟩

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