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
- homRel.FactorsThroughLocalization W = ∀ ⦃X Y : C⦄ ⦃f g : X ⟶ Y⦄, homRel f g → CategoryTheory.AreEqualizedByLocalization W f g
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.