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.

source
def CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.op {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {L : CategoryTheory.Functor C D} {W : CategoryTheory.MorphismProperty C} {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (h : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W Eᵒᵖ) :
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L.op (CategoryTheory.MorphismProperty.op W) E

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance CategoryTheory.Localization.isLocalization_op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} :
    CategoryTheory.Functor.IsLocalization (CategoryTheory.MorphismProperty.Q W).op (CategoryTheory.MorphismProperty.op W)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    instance CategoryTheory.Functor.IsLocalization.op {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {L : CategoryTheory.Functor C D} {W : CategoryTheory.MorphismProperty C} [CategoryTheory.Functor.IsLocalization L W] :
    CategoryTheory.Functor.IsLocalization L.op (CategoryTheory.MorphismProperty.op W)
    Equations