# Documentation

Mathlib.CategoryTheory.Localization.Equivalence

# 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} [] [] [] [] (L₁ : ) (W₁ : ) (L₂ : ) (W₂ : ) (G : ) (G' : ) [] (F : ) (F' : ) [] (α : L₁) (β : L₂) :
D₁ D₂

Basic constructor of an equivalence between localized categories

Instances For
@[simp]
theorem CategoryTheory.Localization.equivalence_counitIso_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [] [] [] [] (L₁ : ) (W₁ : ) (L₂ : ) (W₂ : ) (G : ) (G' : ) [] (F : ) (F' : ) [] (α : L₁) (β : 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₂ () ()).app X ≪≫ β.app X
noncomputable def CategoryTheory.Localization.isEquivalence {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [] [] [] [] (L₁ : ) (W₁ : ) (L₂ : ) (W₂ : ) (G : ) (G' : ) [] (F : ) (F' : ) [] (α : L₁) (β : L₂) :

Basic constructor of an equivalence between localized categories

Instances For
theorem CategoryTheory.Functor.IsLocalization.of_equivalence_source {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [] [] [] (L₁ : ) (W₁ : ) (L₂ : ) (W₂ : ) (E : C₁ C₂) (hW₁ : ) (hW₂ : ) (iso : CategoryTheory.Functor.comp E.functor L₂ L₁) :

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} [] [] [] [] (L₁ : ) (W₁ : ) (L₂ : ) (W₂ : ) (E : C₁ C₂) (E' : D₁ D₂) [CategoryTheory.CatCommSq E.functor L₁ L₂ E'.functor] (hW₁ : ) (hW₂ : ) :

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₂.