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
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Localization.isLocalization_op
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{W : CategoryTheory.MorphismProperty C}
:
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}
[CategoryTheory.Functor.IsLocalization L W]
:
Equations
- ⋯ = ⋯