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₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] (W₁ : MorphismProperty C₁) (W₂ : 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₂

The identity functor as a morphism of localizers.

Equations
def CategoryTheory.LocalizerMorphism.comp {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₃) :

The composition of two localizers morphisms.

Equations
@[simp]
theorem CategoryTheory.LocalizerMorphism.comp_functor {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₃, u₃} C₃] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} {W₃ : MorphismProperty C₃} (Φ : LocalizerMorphism W₁ W₂) (Ψ : LocalizerMorphism W₂ W₃) :
def CategoryTheory.LocalizerMorphism.op {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) :

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

Equations
@[simp]
theorem CategoryTheory.LocalizerMorphism.op_functor {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) :
theorem CategoryTheory.LocalizerMorphism.inverts {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₂ : 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₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] :
Functor D₁ D₂

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
noncomputable instance CategoryTheory.LocalizerMorphism.liftingLocalizedFunctor {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] :
Localization.Lifting L₁ W₁ (Φ.functor.comp L₂) (Φ.localizedFunctor L₁ L₂)
Equations
noncomputable instance CategoryTheory.LocalizerMorphism.catCommSq {C₁ : Type u₁} {C₂ : Type u₂} {D₁ : Type u₄} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] :
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₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [Category.{v₄', u₄'} D₁'] [Category.{v₅', u₅'} D₂'] (L₁' : Functor C₁ D₁') (L₂' : Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : Functor D₁' D₂') [CatCommSq Φ.functor L₁' L₂' G'] [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₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] (G : Functor D₁ D₂) [CatCommSq Φ.functor L₁ L₂ G] {D₁' : Type u₄'} {D₂' : Type u₅'} [Category.{v₄', u₄'} D₁'] [Category.{v₅', u₅'} D₂'] (L₁' : Functor C₁ D₁') (L₂' : Functor C₂ D₂') [L₁'.IsLocalization W₁] [L₂'.IsLocalization W₂] (G' : Functor D₁' D₂') [CatCommSq Φ.functor L₁' L₂' G'] :

Condition that a LocalizerMorphism induces an equivalence on the localized categories

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

    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₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₄, u₄} D₁] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₁ : Functor C₁ D₁) [L₁.IsLocalization W₁] (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedEquivalence] :

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

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

    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.

    instance CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] [Category.{v₅, u₅} D₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) (L₂ : Functor C₂ D₂) [L₂.IsLocalization W₂] [Φ.IsLocalizedEquivalence] :
    (Φ.functor.comp L₂).IsLocalization W₁
    def CategoryTheory.LocalizerMorphism.arrow {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) :

    The localizer morphism from W₁.arrow to W₂.arrow that is induced by Φ : LocalizerMorphism W₁ W₂.

    Equations