Documentation

Mathlib.CategoryTheory.Localization.LocalizerMorphism

Morphisms of localizers #

A morphism of localizers consists of a functor F : C₁ ⥤ C₂ between two categories equipped with morphism properties W₁ and W₂ such that F sends morphisms in W₁ to morphisms in W₂.

If Φ : LocalizerMorphism W₁ W₂, and that L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ are localization functors for W₁ and W₂, the induced functor D₁ ⥤ D₂ is denoted Φ.localizedFunctor L₁ L₂; we introduce the condition Φ.IsLocalizedEquivalence which expresses that this functor is an equivalence of categories. This condition is independent of the choice of the localized categories.

References #

structure CategoryTheory.LocalizerMorphism {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) :
Type (max (max (max u₁ u₂) v₁) v₂)

If W₁ : MorphismProperty C₁ and W₂ : MorphismProperty C₂, a LocalizerMorphism W₁ W₂ is the datum of a functor C₁ ⥤ C₂ which sends morphisms in W₁ to morphisms in W₂

  • functor : CategoryTheory.Functor C₁ C₂

    a functor between the two categories

  • map : W₁ W₂.inverseImage self.functor

    the functor is compatible with the MorphismProperty

Instances For
    theorem CategoryTheory.LocalizerMorphism.map {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (self : CategoryTheory.LocalizerMorphism W₁ W₂) :
    W₁ W₂.inverseImage self.functor

    the functor is compatible with the MorphismProperty

    The identity functor as a morphism of localizers.

    Equations
    Instances For

      The composition of two localizers morphisms.

      Equations
      • Φ.comp Ψ = { functor := Φ.functor.comp Ψ.functor, map := }
      Instances For

        The opposite localizer morphism LocalizerMorphism W₁.op W₂.op deduced from Φ : LocalizerMorphism W₁ W₂.

        Equations
        • Φ.op = { functor := Φ.functor.op, map := }
        Instances For
          theorem CategoryTheory.LocalizerMorphism.inverts {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] :
          W₁.IsInvertedBy (Φ.functor.comp L₂)
          noncomputable def CategoryTheory.LocalizerMorphism.localizedFunctor {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] :

          When Φ : LocalizerMorphism W₁ W₂ and that L₁ and L₂ are localization functors for W₁ and W₂, then Φ.localizedFunctor L₁ L₂ is the induced functor on the localized categories. -

          Equations
          Instances For
            noncomputable instance CategoryTheory.LocalizerMorphism.instLiftingCompFunctorLocalizedFunctor {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] :
            CategoryTheory.Localization.Lifting L₁ W₁ (Φ.functor.comp L₂) (Φ.localizedFunctor L₁ L₂)
            Equations
            • Φ.instLiftingCompFunctorLocalizedFunctor L₁ L₂ = id inferInstance
            noncomputable instance CategoryTheory.LocalizerMorphism.catCommSq {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] :
            CategoryTheory.CatCommSq Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)

            The 2-commutative square expressing that Φ.localizedFunctor L₁ L₂ lifts the functor Φ.functor

            Equations
            theorem CategoryTheory.LocalizerMorphism.isEquivalence_imp {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [CategoryTheory.Category.{v₄', u₄'} D₁'] [CategoryTheory.Category.{v₅', u₅'} D₂'] (L₁' : CategoryTheory.Functor C₁ D₁') (L₂' : CategoryTheory.Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : CategoryTheory.Functor D₁' D₂') [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'] [G.IsEquivalence] :
            G'.IsEquivalence

            If a localizer morphism induces an equivalence on some choice of localized categories, it will be so for any choice of localized categoriees.

            theorem CategoryTheory.LocalizerMorphism.isEquivalence_iff {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [CategoryTheory.Category.{v₄', u₄'} D₁'] [CategoryTheory.Category.{v₅', u₅'} D₂'] (L₁' : CategoryTheory.Functor C₁ D₁') (L₂' : CategoryTheory.Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : CategoryTheory.Functor D₁' D₂') [CategoryTheory.CatCommSq Φ.functor L₁' L₂' G'] :
            G.IsEquivalence G'.IsEquivalence

            Condition that a LocalizerMorphism induces an equivalence on the localized categories

            • isEquivalence : (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence

              the induced functor on the constructed localized categories is an equivalence

            Instances
              theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isEquivalence {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} [self : Φ.IsLocalizedEquivalence] :
              (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence

              the induced functor on the constructed localized categories is an equivalence

              theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk' {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] [G.IsEquivalence] :
              Φ.IsLocalizedEquivalence
              theorem CategoryTheory.LocalizerMorphism.isEquivalence {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor D₁ D₂) [h : Φ.IsLocalizedEquivalence] [CategoryTheory.CatCommSq Φ.functor L₁ L₂ G] :
              G.IsEquivalence

              If a LocalizerMorphism is a localized equivalence, then any compatible functor between the localized categories is an equivalence.

              instance CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₄, u₄} D₁] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedEquivalence] :
              (Φ.localizedFunctor L₁ L₂).IsEquivalence

              If a LocalizerMorphism is a localized equivalence, then the induced functor on the localized categories is an equivalence

              Equations
              • =
              theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] [CategoryTheory.Category.{v₆, u₅} D₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [L₂.IsLocalization W₂] [(Φ.functor.comp L₂).IsLocalization W₁] :
              Φ.IsLocalizedEquivalence

              When Φ : LocalizerMorphism W₁ W₂, if the composition Φ.functor ⋙ L₂ is a localization functor for W₁, then Φ is a localized equivalence.

              theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [Φ.functor.IsEquivalence] (h : W₂ W₁.map Φ.functor) :
              Φ.IsLocalizedEquivalence

              When the underlying functor Φ.functor of Φ : LocalizerMorphism W₁ W₂ is an equivalence of categories and that W₁ and W₂ essentially correspond to each other via this equivalence, then Φ is a localized equivalence.