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 W.op E

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

Equations
  • h.op = { inverts := ⋯, lift := fun (F : CategoryTheory.Functor Cᵒᵖ E) (hF : W.op.IsInvertedBy F) => (h.lift F.rightOp ⋯).leftOp, fac := ⋯, uniq := ⋯ }
Instances For
    source
    instance CategoryTheory.Localization.isLocalization_op {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {W : CategoryTheory.MorphismProperty C} :
    W.Q.op.IsLocalization W.op
    Equations
    • ⋯ = ⋯
    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} [L.IsLocalization W] :
    L.op.IsLocalization W.op
    Equations
    • ⋯ = ⋯