whiskeringRightPreservesLimits — Mathlib

English

For fixed C, D, E, if there is a functor F: D ⥤ E preserving limits of shape J, then whiskeringRight by F preserves limits of shape J in the functor category.

Русский

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

LaTeX

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

Lean4

instance whiskeringRightPreservesLimits {C : Type*} [Category C] {D : Type*} [Category D] {E : Type*} [Category E]
    (F : D ⥤ E) [HasLimitsOfSize.{w, w'} D] [PreservesLimitsOfSize.{w, w'} F] :
    PreservesLimitsOfSize.{w, w'} ((whiskeringRight C D E).obj F) :=
  ⟨inferInstance⟩

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