instPreservesColimitsOfShapeFunctorLim

English

For fixed C, D, E and J, if F: D ⥤ E preserves colimits of shape J, then whiskeringRight by F preserves colimits of shape J in the functor category.

Русский

Для фиксированных C, D, E и J, если F: D ⥤ E сохраняет колимиты формы J, то whiskeringRight по F сохраняет колимиты формы J в категории функционалов.

LaTeX

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

Lean4

noncomputable instance : PreservesColimitsOfShape J (lim : (K ⥤ D ⥤ C) ⥤ _) :=
  preservesColimitsOfShape_of_evaluation _ _
    (fun d =>
      let i :
        (lim : (K ⥤ D ⥤ C) ⥤ _) ⋙ (evaluation D C).obj d ≅
          limit ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip :=
        NatIso.ofComponents
          (fun X =>
            (limitObjIsoLimitCompEvaluation _ _) ≪≫
              (by exact HasLimit.isoOfNatIso (Iso.refl _)) ≪≫ (limitObjIsoLimitCompEvaluation _ _).symm)
          (fun {F G} η => limit_obj_ext (fun j => by simp [← NatTrans.comp_app]))
      preservesColimitsOfShape_of_natIso (i ≪≫ limitFlipIsoCompLim _).symm)

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