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₂} [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₂

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

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₃) : 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₃} [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₃) : (Φ.comp Ψ).functor = Φ.functor.comp Ψ.functor

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

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

• Φ.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₅} [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

• Φ.liftingLocalizedFunctor L₁ L₂ = id inferInstance

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

• Φ.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₅} [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] : 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'] : G.IsEquivalence ↔ G'.IsEquivalence

class CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence {C₁ : Type u₁} {C₂ : Type u₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : 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₅} [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] : Φ.IsLocalizedEquivalence

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] : 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₅} [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] : (Φ.localizedFunctor L₁ L₂).IsEquivalence

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

theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_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₂] [(Φ.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₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : 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₅} [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₂) : 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₂} [Category.{v₁, u₁} C₁] [Category.{v₂, u₂} C₂] {W₁ : MorphismProperty C₁} {W₂ : MorphismProperty C₂} (Φ : LocalizerMorphism W₁ W₂) : Φ.arrow.functor = Φ.functor.mapArrow