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.

def CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.op {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_5, u_2} D] {L : Functor C D} {W : MorphismProperty C} {E : Type u_3} [Category.{u_6, u_3} E] (h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ) : 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 := ⋯ }

instance CategoryTheory.Localization.isLocalization_op {C : Type u_1} [Category.{u_3, u_1} C] {W : MorphismProperty C} : W.Q.op.IsLocalization W.op

instance CategoryTheory.Functor.IsLocalization.op {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] : L.op.IsLocalization W.op

theorem CategoryTheory.Localization.isoOfHom_unop {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {X Y : Cᵒᵖ} (w : X ⟶ Y) (hw : W.op w) : (isoOfHom L.op W.op w hw).unop = isoOfHom L W w.unop hw

theorem CategoryTheory.Localization.isoOfHom_op_inv {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (L : Functor C D) (W : MorphismProperty C) [L.IsLocalization W] {X Y : Cᵒᵖ} (w : X ⟶ Y) (hw : W.op w) : (isoOfHom L.op W.op w hw).inv = (isoOfHom L W w.unop hw).inv.op