Documentation

Mathlib.CategoryTheory.Localization.Predicate

Predicate for localized categories #

In this file, a predicate L.IsLocalization W is introduced for a functor L : C ⥤ D and W : MorphismProperty C: it expresses that L identifies D with the localized category of C with respect to W (up to equivalence).

We introduce a universal property StrictUniversalPropertyFixedTarget L W E which states that L inverts the morphisms in W and that all functors C ⥤ E inverting W uniquely factors as a composition of L ⋙ G with G : D ⥤ E. Such universal properties are inputs for the constructor IsLocalization.mk' for L.IsLocalization W.

When L : C ⥤ D is a localization functor for W : MorphismProperty (i.e. when [L.IsLocalization W] holds), for any category E, there is an equivalence FunctorEquivalence L W E : (D ⥤ E) ≌ (W.FunctorsInverting E) that is induced by the composition with the functor L. When two functors F : C ⥤ E and F' : D ⥤ E correspond via this equivalence, we shall say that F' lifts F, and the associated isomorphism L ⋙ F' ≅ F is the datum that is part of the class Lifting L W F F'. The functions liftNatTrans and liftNatIso can be used to lift natural transformations and natural isomorphisms between functors.

The predicate expressing that, up to equivalence, a functor L : C ⥤ D identifies the category D with the localized category of C with respect to W : MorphismProperty C.

Instances

    This universal property states that a functor L : C ⥤ D inverts morphisms in W and the all functors D ⥤ E (for a fixed category E) uniquely factors through L.

    Instances For

      The localized category W.Localization that was constructed satisfies the universal property of the localization.

      Instances For

        The isomorphism L.obj X ≅ L.obj Y that is deduced from a morphism f : X ⟶ Y which belongs to W, when L.IsLocalization W.

        Instances For

          A chosen equivalence of categories W.Localization ≅ D for a functor L : C ⥤ D which satisfies L.IsLocalization W. This shall be used in order to deduce properties of L from properties of W.Q.

          Instances For

            The functor (D ⥤ E) ⥤ W.functors_inverting E induced by the composition with a localization functor L : C ⥤ D with respect to W : morphism_property C.

            Instances For

              The equivalence of categories (D ⥤ E) ≌ (W.FunctorsInverting E) induced by the composition with a localization functor L : C ⥤ D with respect to W : MorphismProperty C.

              Instances For

                The functor (D ⥤ E) ⥤ (C ⥤ E) given by the composition with a localization functor L : C ⥤ D with respect to W : MorphismProperty C.

                Instances For
                  theorem CategoryTheory.Localization.natTrans_ext {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [CategoryTheory.Category.{u_5, u_3} E] [CategoryTheory.Functor.IsLocalization L W] {F₁ : CategoryTheory.Functor D E} {F₂ : CategoryTheory.Functor D E} (τ : F₁ F₂) (τ' : F₁ F₂) (h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)) :
                  τ = τ'

                  When L : C ⥤ D is a localization functor for W : MorphismProperty C and F : C ⥤ E is a functor, we shall say that F' : D ⥤ E lifts F if the obvious diagram is commutative up to an isomorphism.

                  Instances

                    Given a localization functor L : C ⥤ D for W : MorphismProperty C and a functor F : C ⥤ E which inverts W, this is a choice of functor D ⥤ E which lifts F.

                    Instances For

                      The canonical isomorphism L ⋙ lift F hF L ≅ F for any functor F : C ⥤ E which inverts W, when L : C ⥤ D is a localization functor for W.

                      Instances For

                        Given a localization functor L : C ⥤ D for W : MorphismProperty C, if (F₁' F₂' : D ⥤ E) are functors which lifts functors (F₁ F₂ : C ⥤ E), a natural transformation τ : F₁ ⟶ F₂ uniquely lifts to a natural transformation F₁' ⟶ F₂'.

                        Instances For

                          Given a localization functor L : C ⥤ D for W : MorphismProperty C, if (F₁' F₂' : D ⥤ E) are functors which lifts functors (F₁ F₂ : C ⥤ E), a natural isomorphism τ : F₁ ⟶ F₂ lifts to a natural isomorphism F₁' ⟶ F₂'.

                          Instances For

                            Given a localization functor L : C ⥤ D for W : MorphismProperty C, if F₁' : D ⥤ E lifts a functor F₁ : C ⥤ D, then a functor F₂' which is isomorphic to F₁' also lifts a functor F₂ that is isomorphic to F₁.

                            Instances For

                              If L : C ⥤ D is a localization for W : MorphismProperty C, then it is also the case of a functor obtained by post-composing L with an equivalence of categories.

                              If L₁ : C ⥤ D₁ and L₂ : C ⥤ D₂ are two localization functors for the same MorphismProperty C, this is an equivalence of categories D₁ ≌ D₂.

                              Instances For

                                The functor of equivalence of localized categories given by Localization.uniq is compatible with the localization functors.

                                Instances For

                                  The inverse functor of equivalence of localized categories given by Localization.uniq is compatible with the localization functors.

                                  Instances For

                                    If L₁ : C ⥤ D₁ and L₂ : C ⥤ D₂ are two localization functors for the same MorphismProperty C, any functor F : D₁ ⥤ D₂ equipped with an isomorphism L₁ ⋙ F ≅ L₂ is isomorphic to the functor of the equivalence given by uniq.

                                    Instances For