whiskeringRight_preservesColimitsOfShape

English

For any shape J, if D has colimits of shape J and F preserves those colimits, then whiskeringRight by F preserves colimits of shape J.

Русский

Для любой формы J, если в D существуют колимиты формы J и F сохраняет их, то правое взвешивание на F сохраняет колимиты формы J.

LaTeX

$$$\\operatorname{PreservesColimitsOfShape} J\\big((\\mathrm{whiskeringRight}\\;C\\;D\\;E).\\mathrm{obj} F\\big)$$$

Lean4

instance whiskeringRight_preservesColimitsOfShape {C : Type*} [Category C] {D : Type*} [Category D] {E : Type*}
    [Category E] {J : Type*} [Category J] [HasColimitsOfShape J D] (F : D ⥤ E) [PreservesColimitsOfShape J F] :
    PreservesColimitsOfShape J ((whiskeringRight C D E).obj F) :=
  ⟨fun {K} =>
    ⟨fun c {hc} =>
      ⟨by
        apply evaluationJointlyReflectsColimits _ (fun k => ?_)
        change IsColimit (((evaluation _ _).obj k ⋙ F).mapCocone c)
        exact isColimitOfPreserves _ hc⟩⟩⟩

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