whiskeringLeft_preservesColimit — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance whiskeringLeft_preservesColimit [HasColimitsOfSize.{w, w'} D] (F : C ⥤ E) :
    PreservesColimitsOfSize.{w, w'} ((whiskeringLeft C E D).obj F) :=
  ⟨fun {J} _ => whiskeringLeft_preservesColimitsOfShape J F⟩

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