Documentation

Mathlib.CategoryTheory.Localization.Quotient

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.

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
Instances For

    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.
    Instances For

      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
      Instances For

        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.