English
Let C be a category with a localization L for a morphism property W. For a finite index shape J with products in C that are stable under W, the induced map to the localization inverts all W-morphisms when taking pointwise limits over J. Equivalently, the composite lim ⋙ L inverts the morphisms coming from W in the functor category over the discrete J.
Русский
Пусть C — категория с локализацией L по свойству морфизмов W. Пусть J — конечная форма со сцеплениями в C, сохраняющимися относительно W. Тогда композиция предела и локализации инвертирует все морфизмы из W в категории-функторов над Discrete J. Иными словами, lim ⋙ L инвертирует морфизмы W в соответствующей категории функторов.
LaTeX
$$$ (W.functorCategory (Discrete J)).IsInvertedBy (lim \\circ L) $$$
Lean4
theorem inverts : (W.functorCategory (Discrete J)).IsInvertedBy (lim ⋙ L) := fun _ _ f hf =>
Localization.inverts L W _ (MorphismProperty.limMap f hf)
