Localization functors are preserved through equivalences

In Localization/Predicate.lean, the lemma Localization.of_equivalence_target already showed that the predicate of localized categories is unchanged when we replace the target category (i.e. the candidate localized category) by an equivalent category. In this file, we show the same for the source category (Localization.of_equivalence_source). More generally, Localization.of_equivalences shows that we may replace both the source and target categories by equivalent categories. This is obtained using Localization.isEquivalence which provide a sufficient condition in order to show that a functor between localized categories is an equivalence.

noncomputable def CategoryTheory.Localization.equivalence {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_4} D₁] [CategoryTheory.Category.{u_9, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor C₁ D₂) (G' : CategoryTheory.Functor D₁ D₂) [CategoryTheory.Localization.Lifting L₁ W₁ G G'] (F : CategoryTheory.Functor C₂ D₁) (F' : CategoryTheory.Functor D₂ D₁) [CategoryTheory.Localization.Lifting L₂ W₂ F F'] (α : G.comp F' ≅ L₁) (β : F.comp G' ≅ L₂) : D₁ ≌ D₂

Basic constructor of an equivalence between localized categories

Equations

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

@[simp]

theorem CategoryTheory.Localization.equivalence_counitIso_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_7, u_4} D₁] [CategoryTheory.Category.{u_6, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor C₁ D₂) (G' : CategoryTheory.Functor D₁ D₂) [CategoryTheory.Localization.Lifting L₁ W₁ G G'] (F : CategoryTheory.Functor C₂ D₁) (F' : CategoryTheory.Functor D₂ D₁) [CategoryTheory.Localization.Lifting L₂ W₂ F F'] (α : G.comp F' ≅ L₁) (β : F.comp G' ≅ L₂) (X : C₂) : (CategoryTheory.Localization.equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) = ((CategoryTheory.Localization.Lifting.iso L₂ W₂ (F.comp G') (F'.comp G')).app X).trans (β.app X)

noncomputable def CategoryTheory.Localization.isEquivalence {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_8, u_4} D₁] [CategoryTheory.Category.{u_9, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [L₂.IsLocalization W₂] (G : CategoryTheory.Functor C₁ D₂) (G' : CategoryTheory.Functor D₁ D₂) [CategoryTheory.Localization.Lifting L₁ W₁ G G'] (F : CategoryTheory.Functor C₂ D₁) (F' : CategoryTheory.Functor D₂ D₁) [CategoryTheory.Localization.Lifting L₂ W₂ F F'] (α : G.comp F' ≅ L₁) (β : F.comp G' ≅ L₂) : G'.IsEquivalence

Basic constructor of an equivalence between localized categories

Equations

• CategoryTheory.Localization.isEquivalence L₁ W₁ L₂ W₂ G G' F F' α β = CategoryTheory.Functor.IsEquivalence.ofEquivalence (CategoryTheory.Localization.equivalence L₁ W₁ L₂ W₂ G G' F F' α β)

theorem CategoryTheory.Functor.IsLocalization.of_equivalence_source {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D] (L₁ : CategoryTheory.Functor C₁ D) (W₁ : CategoryTheory.MorphismProperty C₁) (L₂ : CategoryTheory.Functor C₂ D) (W₂ : CategoryTheory.MorphismProperty C₂) (E : C₁ ≌ C₂) (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) [L₁.IsLocalization W₁] (iso : E.functor.comp L₂ ≅ L₁) : L₂.IsLocalization W₂

If L₁ : C₁ ⥤ D is a localization functor for W₁ : MorphismProperty C₁, then it is also the case of a functor L₂ : C₂ ⥤ D for a suitable W₂ : MorphismProperty C₂ when we have an equivalence of category E : C₁ ≌ C₂ and an isomorphism E.functor ⋙ L₂ ≅ L₁.

theorem CategoryTheory.Functor.IsLocalization.of_equivalences {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_7, u_4} D₁] [CategoryTheory.Category.{u_9, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) (E : C₁ ≌ C₂) (E' : D₁ ≌ D₂) [CategoryTheory.CatCommSq E.functor L₁ L₂ E'.functor] (hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor) (hW₂ : W₂.IsInvertedBy L₂) : L₂.IsLocalization W₂

If L₁ : C₁ ⥤ D₁ is a localization functor for W₁ : MorphismProperty C₁, then if we transport this functor L₁ via equivalences C₁ ≌ C₂ and D₁ ≌ D₂ to get a functor L₂ : C₂ ⥤ D₂, then L₂ is also a localization functor for a suitable W₂ : MorphismProperty C₂.