Theorems · Theorem · category theory

CategoryTheory.Functor.IsLocalization.of_equivalences

∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_3 : CategoryTheory.Category.{v_5, 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],
  W₁ ≤ W₂.isoClosure.inverseImage E.functor → 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₂.

Defined in

Mathlib.CategoryTheory.Localization.Equivalence

Cited by

0 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.CatCommSq