isLocalization_op — Mathlib

English

Let C be a category and W a morphism property on C. Then the opposite category C^op, equipped with the opposite morphism property W^op, is localized by the opposite of the chosen inverting data, i.e., the opposite localization structure exists and is compatible with taking opposites.

Русский

Пусть C — категория и W — свойство морфизмов в C. Тогда противоположная категория C^op, снабжённая противоположным свойством морфизмов W^op, локализуется относительно противоположного набора инвертируемых морфизмов.

LaTeX

$$$(W^{op}.Q^{op}).IsLocalization(W^{op})$$$

Lean4

instance isLocalization_op : W.Q.op.IsLocalization W.op :=
  Functor.IsLocalization.mk' W.Q.op W.op (strictUniversalPropertyFixedTargetQ W _).op
    (strictUniversalPropertyFixedTargetQ W _).op

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