Documentation

Mathlib.CategoryTheory.Localization.Construction

Construction of the localized category #

This file constructs the localized category, obtained by formally inverting a class of maps W : MorphismProperty C in a category C.

We first construct a quiver LocQuiver W whose objects are the same as those of C and whose maps are the maps in C and placeholders for the formal inverses of the maps in W.

The localized category W.Localization is obtained by taking the quotient of the path category of LocQuiver W by the congruence generated by four types of relations.

The obvious functor Q W : C ⥤ W.Localization satisfies the universal property of the localization. Indeed, if G : C ⥤ D sends morphisms in W to isomorphisms in D (i.e. we have hG : W.IsInvertedBy G), then there exists a unique functor G' : W.Localization ⥤ D such that Q W ≫ G' = G. This G' is lift G hG. The expected property of lift G hG if expressed by the lemma fac and the uniqueness is expressed by uniq.

References #

  • obj : C

    underlying object

If W : MorphismProperty C, LocQuiver W is a quiver with the same objects as C, and whose morphisms are those in C and placeholders for formal inverses of the morphisms in W.

Instances For

    The morphism in the path category associated to a morphism in the original category.

    Instances For

      The morphism in the path category corresponding to a formal inverse.

      Instances For

        The relations by which we take the quotient in order to get the localized category.

        Instances For

          The localized category obtained by formally inverting the morphisms in W : MorphismProperty C

          Instances For

            The isomorphism in W.Localization associated to a morphism w in W

            Instances For
              @[inline, reducible]

              The formal inverse in W.Localization of a morphism w in W.

              Instances For

                The canonical bijection between objects in a category and its localization with respect to a morphism_property W

                Instances For

                  A MorphismProperty in W.Localization is satisfied by all morphisms in the localized category if it contains the image of the morphisms in the original category, the inverses of the morphisms in W and if it is stable under composition

                  A MorphismProperty in W.Localization is satisfied by all morphisms in the localized category if it contains the image of the morphisms in the original category, if is stable under composition and if the property is stable by passing to inverses.

                  If F₁ and F₂ are functors W.Localization ⥤ D and if we have τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂, we shall define a natural transformation F₁ ⟶ F₂. This is the app field of this natural transformation.

                  Instances For

                    The equivalence of categories (W.localization ⥤ D) ≌ (W.FunctorsInverting D) induced by the composition with W.Q : C ⥤ W.localization.

                    Instances For