Localization of quotient categories

Given a relation homRel : HomRel C on morphisms in a category C and W : MorphismProperty C, we introduce a property homRel.FactorsThroughLocalization W expressing that related morphisms are mapped to the same morphism in the localized category with respect to W. When W is compatible with homRel (i.e. there is a class of morphisms W' such that hW : W = W'.inverseImage (Quotient.functor homRel)), we show that LocalizerMorphism.ofEq hW : LocalizerMorphism W W' induces an equivalence on localized categories.

def HomRel.FactorsThroughLocalization {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] (homRel : HomRel C) (W : CategoryTheory.MorphismProperty C) : Prop

Given homRel : HomRel C and W : MorphismProperty C, this is the property that whenever homRel f g, then the morphisms f and g are sent to the same morphism in the localization category with respect to W.

Equations

• homRel.FactorsThroughLocalization W = ∀ ⦃X Y : C⦄ ⦃f g : X ⟶ Y⦄, homRel f g → CategoryTheory.AreEqualizedByLocalization W f g

def HomRel.FactorsThroughLocalization.strictUniversalPropertyFixedTarget {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] {homRel : HomRel C} {W : CategoryTheory.MorphismProperty C} (h : homRel.FactorsThroughLocalization W) {W' : CategoryTheory.MorphismProperty (CategoryTheory.Quotient homRel)} (hW : W = W'.inverseImage (CategoryTheory.Quotient.functor homRel)) {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] (L' : CategoryTheory.Functor (CategoryTheory.Quotient homRel) D) (univ : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L' W' E) : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget ((CategoryTheory.Quotient.functor homRel).comp L') W E

If L' : Quotient homRel ⥤ D satisfies the strict universal property of the localization, then Quotient.functor homRel ⋙ L' also satisfies it.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HomRel.FactorsThroughLocalization.strictUniversalPropertyFixedTarget' {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {homRel : HomRel C} {W : CategoryTheory.MorphismProperty C} (h : homRel.FactorsThroughLocalization W) {W' : CategoryTheory.MorphismProperty (CategoryTheory.Quotient homRel)} (hW : W = W'.inverseImage (CategoryTheory.Quotient.functor homRel)) (E : Type u_3) [CategoryTheory.Category.{u_5, u_3} E] : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget ((CategoryTheory.Quotient.functor homRel).comp W'.Q) W E

If homRel : HomRel C satisfies homRel.FactorsThroughLocalization W and that the class of morphisms W induces a class of morphism W' on the quotient category, then Quotient.functor homRel ⋙ W'.Q satisfies the universal property of the localization. This is used in HomRel.FactorsThroughLocalization.isLocalizedEquivalence in order to show that as a localizer morphism, the quotient functor induces an equivalence on localized categories.

Equations

• h.strictUniversalPropertyFixedTarget' hW E = h.strictUniversalPropertyFixedTarget hW W'.Q (CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ W' E)

theorem HomRel.FactorsThroughLocalization.isLocalizedEquivalence {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {homRel : HomRel C} {W : CategoryTheory.MorphismProperty C} (h : homRel.FactorsThroughLocalization W) {W' : CategoryTheory.MorphismProperty (CategoryTheory.Quotient homRel)} (hW : W = W'.inverseImage (CategoryTheory.Quotient.functor homRel)) : (CategoryTheory.LocalizerMorphism.ofEq hW).IsLocalizedEquivalence

If homRel : HomRel C satisfies homRel.FactorsThroughLocalization W and that the class of morphisms W induces a class of morphism W' on the quotient category, then the localizer morphism given by the functor Quotient.functor HomRel : C ⥤ Quotient homRel induces equivalences on localized categories.