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

• [Bruno Kahn and Georges Maltsiniotis, Structures de dérivabilité][KahnMaltsiniotis2008]

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

def CategoryTheory.LocalizerMorphism.id {C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] (W₁ : CategoryTheory.MorphismProperty C₁) : CategoryTheory.LocalizerMorphism W₁ W₁

The identity functor as a morphism of localizers.

Equations

• CategoryTheory.LocalizerMorphism.id W₁ = { functor := CategoryTheory.Functor.id C₁, map := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.id_functor {C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] (W₁ : CategoryTheory.MorphismProperty C₁) : (CategoryTheory.LocalizerMorphism.id W₁).functor = CategoryTheory.Functor.id C₁

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

The composition of two localizers morphisms.

Equations

• Φ.comp Ψ = { functor := Φ.functor.comp Ψ.functor, map := ⋯ }

@[simp]

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

def CategoryTheory.LocalizerMorphism.op {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₂) : CategoryTheory.LocalizerMorphism W₁.op W₂.op

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

Equations

• Φ.op = { functor := Φ.functor.op, map := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.op_functor {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₂) : Φ.op.functor = Φ.functor.op

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₂] : CategoryTheory.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

• Φ.localizedFunctor L₁ L₂ = CategoryTheory.Localization.lift (Φ.functor.comp L₂) ⋯ L₁

noncomputable instance CategoryTheory.LocalizerMorphism.liftingLocalizedFunctor {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

• Φ.liftingLocalizedFunctor 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

• Φ.catCommSq L₁ L₂ = { iso' := (CategoryTheory.Localization.Lifting.iso L₁ W₁ (Φ.functor.comp L₂) (Φ.localizedFunctor L₁ L₂)).symm }

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

class CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence {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₂) : Prop

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

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.

instance CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.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₂] [Φ.IsLocalizedEquivalence] : (Φ.functor.comp L₂).IsLocalization W₁

Equations

• ⋯ = ⋯

def CategoryTheory.LocalizerMorphism.arrow {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₂) : CategoryTheory.LocalizerMorphism W₁.arrow W₂.arrow

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

Equations

• Φ.arrow = { functor := Φ.functor.mapArrow, map := ⋯ }

@[simp]

theorem CategoryTheory.LocalizerMorphism.arrow_functor {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₂) : Φ.arrow.functor = Φ.functor.mapArrow