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.

  • inverts : W.IsInvertedBy L

    the functor inverts the given MorphismProperty

  • isEquivalence : (CategoryTheory.Localization.Construction.lift L ).IsEquivalence

    the induced functor from the constructed localized category is an equivalence

Instances

    the functor inverts the given MorphismProperty

    the induced functor from the constructed localized category is an equivalence

    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.

    • inverts : W.IsInvertedBy L

      the functor L inverts W

    • lift : (F : CategoryTheory.Functor C E) → W.IsInvertedBy FCategoryTheory.Functor D E

      any functor C ⥤ E which inverts W can be lifted as a functor D ⥤ E

    • fac : ∀ (F : CategoryTheory.Functor C E) (hF : W.IsInvertedBy F), L.comp (self.lift F hF) = F

      there is a factorisation involving the lifted functor

    • uniq : ∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂F₁ = F₂

      uniqueness of the lifted functor

    Instances For

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

      Equations
      Instances For

        When W consists of isomorphisms, the identity satisfies the universal property of the localization.

        Equations
        Instances For
          @[simp]
          @[simp]
          theorem CategoryTheory.Localization.isoOfHom_hom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {X : C} {Y : C} (f : X Y) (hf : W f) :
          def CategoryTheory.Localization.isoOfHom {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] {X : C} {Y : C} (f : X Y) (hf : W f) :
          L.obj X L.obj Y

          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.

          Equations
          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.

            Equations
            Instances For

              Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D, one may identify the functors W.Q and L.

              Equations
              Instances For

                Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D, one may identify the functors L and W.Q.

                Equations
                • One or more equations did not get rendered due to their size.
                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.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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.

                    Equations
                    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.

                      Equations
                      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] [L.IsLocalization 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.

                        • iso' : L.comp F' F

                          the isomorphism relating the localization functor and the two other given functors

                        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.

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

                            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.

                            Equations
                            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₂'.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              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₂'.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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₁.

                                  Equations
                                  Instances For
                                    theorem CategoryTheory.Functor.IsLocalization.of_iso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] (W : CategoryTheory.MorphismProperty C) {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} (e : L₁ L₂) [L₁.IsLocalization W] :
                                    L₂.IsLocalization W
                                    theorem CategoryTheory.Functor.IsLocalization.of_equivalence_target {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_6, u_1} C] [CategoryTheory.Category.{u_7, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) {E : Type u_4} [CategoryTheory.Category.{u_5, u_4} E] (L' : CategoryTheory.Functor C E) (eq : D E) [L.IsLocalization W] (e : L.comp eq.functor L') :
                                    L'.IsLocalization W

                                    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.

                                    def CategoryTheory.Localization.uniq {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W'] :
                                    D₁ D₂

                                    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₂.

                                    Equations
                                    Instances For
                                      theorem CategoryTheory.Localization.uniq_symm {C : Type u_1} [CategoryTheory.Category.{u_8, u_1} C] {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{u_6, u_4} D₁] [CategoryTheory.Category.{u_7, u_5} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W'] :
                                      def CategoryTheory.Localization.compUniqFunctor {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W'] :
                                      L₁.comp (CategoryTheory.Localization.uniq L₁ L₂ W').functor L₂

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        def CategoryTheory.Localization.compUniqInverse {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W'] :
                                        L₂.comp (CategoryTheory.Localization.uniq L₁ L₂ W').inverse L₁

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

                                        Equations
                                        Instances For
                                          def CategoryTheory.Localization.isoUniqFunctor {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D₁ : Type u_5} {D₂ : Type u_6} [CategoryTheory.Category.{u_7, u_5} D₁] [CategoryTheory.Category.{u_8, u_6} D₂] (L₁ : CategoryTheory.Functor C D₁) (L₂ : CategoryTheory.Functor C D₂) (W' : CategoryTheory.MorphismProperty C) [L₁.IsLocalization W'] [L₂.IsLocalization W'] (F : CategoryTheory.Functor D₁ D₂) (e : L₁.comp F L₂) :
                                          F (CategoryTheory.Localization.uniq L₁ L₂ W').functor

                                          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.

                                          Equations
                                          Instances For

                                            The property that two morphisms become equal in the localized category.

                                            Equations
                                            Instances For