English
Let C be a category and W a morphism property of arrows in C that is stable under taking limits of shape J. For any functors X, Y: J → C, provided with limits, and any natural transformation f: X ⟶ Y whose components lie in W in the functor category (hf: W.functorCategory J f), the induced map between the limits limMap f: lim X → lim Y also lies in W.
Русский
Пусть C — категория, W — свойство морфизмов в C, устойчивое при взятии пределов формы J. Для любых диаграмм X, Y: J → C, имеющих пределы, и для любого натуралного преобразования f: X ⟶ Y, компоненты которого принадлежат W в категорию-функтор (hf: W.functorCategory J f), индуцированный отображение между пределами limMap f: lim X → lim Y принадлежит W.
LaTeX
$$$[W.IsStableUnderLimitsOfShape J] \Rightarrow \forall X,Y: J \to C, [HasLimit X], [HasLimit Y], (f: X \to Y), hf: W.functorCategory J f \Rightarrow W(\limMap f).$$$
Lean4
protected theorem limMap [W.IsStableUnderLimitsOfShape J] {X Y : J ⥤ C} (f : X ⟶ Y) [HasLimit X] [HasLimit Y]
(hf : W.functorCategory _ f) : W (limMap f) :=
limitsOfShape_le _ (limitsOfShape_limMap _ hf)
