whiskeringRight_preservesLimitsOfShape

English

For any shape J, if D has limits of shape J and F: D ⥤ E preserves those limits, then whiskering to the right by F preserves limits of shape J.

Русский

Для любой формы J, если у D есть пределы формы J и F: D ⥤ E сохраняет эти пределы, то правое взвешивание на F сохраняет пределы формы J.

LaTeX

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

Lean4

instance whiskeringRight_preservesLimitsOfShape {C : Type*} [Category C] {D : Type*} [Category D] {E : Type*}
    [Category E] {J : Type*} [Category J] [HasLimitsOfShape J D] (F : D ⥤ E) [PreservesLimitsOfShape J F] :
    PreservesLimitsOfShape J ((whiskeringRight C D E).obj F) :=
  ⟨fun {K} =>
    ⟨fun c {hc} =>
      ⟨by
        apply evaluationJointlyReflectsLimits _ (fun k => ?_)
        change IsLimit (((evaluation _ _).obj k ⋙ F).mapCone c)
        exact isLimitOfPreserves _ hc⟩⟩⟩

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