Documentation

Mathlib.CategoryTheory.Localization.Opposite

Localization of the opposite category #

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