whiskeringLeft_preservesLimits — Mathlib

English

Let C, D, E be categories with D having all limits of the given size. If F: C ⥤ E, then left whiskering by F preserves limits of that size in the functor category.

Русский

Пусть C, D, E — категории, в D существуют пределы данного размера. Тогда левое взвешивание на F: C ⥤ E сохраняет пределы указанного размера в категории Fun(C, E).

LaTeX

$$$\\operatorname{PreservesLimitsOfSize}_{w,w'}\\big(((\\mathrm{whiskeringLeft}\\;C\\;E\\;D).\\mathrm{obj} F)\\big)$$$

Lean4

instance whiskeringLeft_preservesLimits [HasLimitsOfSize.{w, w'} D] (F : C ⥤ E) :
    PreservesLimitsOfSize.{w, w'} ((whiskeringLeft C E D).obj F) :=
  ⟨fun {J} _ => whiskeringLeft_preservesLimitsOfShape J F⟩

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