Localization of the opposite category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If a functor L : C ⥤ D is a localization functor for W : morphism_property C, it is shown in this file that L.op : Cᵒᵖ ⥤ Dᵒᵖ is also a localization functor.

source

def category_theory.localization.strict_universal_property_fixed_target.op {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {L : C ⥤ D} {W : category_theory.morphism_property C} {E : Type u_5} [category_theory.category E] (h : category_theory.localization.strict_universal_property_fixed_target L W Eᵒᵖ) :

category_theory.localization.strict_universal_property_fixed_target L.op W.op E

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

Equations

h.op = {inverts := _, lift := λ (F : Cᵒᵖ ⥤ E) (hF : W.op.is_inverted_by F), (h.lift F.right_op _).left_op, fac := _, uniq := _}

source

@[protected, instance]

def category_theory.localization.is_localization_op {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} :

W.Q.op.is_localization W.op

source

@[protected, instance]

def category_theory.functor.is_localization.op {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {L : C ⥤ D} {W : category_theory.morphism_property C} [h : L.is_localization W] :

L.op.is_localization W.op