mathlib documentation


Localization of the opposite category #

If a functor L : C ⥤ D is a localization functor for W : morphism_property C, it is shown in this file that L.op : Cᵒᵖ ⥤ Dᵒᵖ is also a localization functor.

If L : C ⥤ D satisfies the universal property of the localisation for W : morphism_property C, then L.op also does.