colimMap — Mathlib

English

Let X and Y be functors J ⥤ C with HasColimit X and HasColimit Y. If a natural transformation f : X ⟶ Y satisfies W in the functor category (hf : W.functorCategory _ f), then the induced morphism between colimits, colimMap f, also has property W.

Русский

Пусть X и Y — объекты-функторы J ⥤ C, у которых существуют колимиты. Если натуральное отображение f : X ⟶ Y удовлетворяет свойству W в категориальной категории-функтор, то индуцированное отображение между колимитами, colimMap f, также имеет свойство W.

LaTeX

$$$W(f) \Rightarrow W(\operatorname{colimMap} f)$$$

Lean4

protected theorem colimMap [W.IsStableUnderColimitsOfShape J] {X Y : J ⥤ C} (f : X ⟶ Y) [HasColimit X] [HasColimit Y]
    (hf : W.functorCategory _ f) : W (colimMap f) :=
  colimitsOfShape_le _ (colimitsOfShape_colimMap _ hf)

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