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}
[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ᵒᵖ)
:
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
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
- ⋯ = ⋯
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
- ⋯ = ⋯
theorem
CategoryTheory.Localization.isoOfHom_unop
{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]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(w : X ⟶ Y)
(hw : W.op w)
:
(CategoryTheory.Localization.isoOfHom L.op W.op w hw).unop = CategoryTheory.Localization.isoOfHom L W w.unop hw
theorem
CategoryTheory.Localization.isoOfHom_op_inv
{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]
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(w : X ⟶ Y)
(hw : W.op w)
:
(CategoryTheory.Localization.isoOfHom L.op W.op w hw).inv = (CategoryTheory.Localization.isoOfHom L W w.unop hw).inv.op