whiskeringLeft_preservesLimitsOfShape

English

For any J, if HasLimitsOfShape J D holds, then whiskeringLeft preserves limits of shape J.

Русский

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

LaTeX

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

Lean4

instance whiskeringLeft_preservesLimitsOfShape (J : Type u) [Category.{v} J] [HasLimitsOfShape J D] (F : C ⥤ E) :
    PreservesLimitsOfShape J ((whiskeringLeft C E D).obj F) :=
  ⟨fun {K} =>
    ⟨fun c {hc} =>
      ⟨by
        apply evaluationJointlyReflectsLimits
        intro Y
        change IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)
        exact isLimitOfPreserves _ hc⟩⟩⟩

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