CategoryTheory.Functor.IsLocalization.of_equivalence_source
theorem CategoryTheory.Functor.IsLocalization.of_equivalence_source :
∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{u_6, u_1} C₁]
[inst_1 : CategoryTheory.Category.{u_8, u_2} C₂] [inst_2 : 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₂),
W₁ ≤ W₂.isoClosure.inverseImage E.functor →
W₂.IsInvertedBy L₂ → ∀ [inst_3 : L₁.IsLocalization W₁], (E.functor.comp L₂ ≅ L₁) → L₂.IsLocalization W₂
This theorem, `CategoryTheory.Functor.IsLocalization.of_equivalence_source`, states that if a functor `L₁ : C₁ ⥤ D` is a localization for a certain class of morphisms `W₁` in category `C₁`, then there exists another functor `L₂ : C₂ ⥤ D` that serves as a localization for a different class of morphisms `W₂` in another category `C₂`. The theorem requires an equivalence of categories `E : C₁ ≌ C₂` and an isomorphism `E.functor ⋙ L₂ ≅ L₁`. Furthermore, it requires `W₁` to be a subset of the inverse image of `W₂` under `E.functor` and `W₂` to be inverted by `L₂`. Under these conditions, it asserts that `L₂` is a localization of `W₂`.
More concisely: If functor `L₁` is a localization of morphisms `W₁` in category `C₁` via an equivalence `E : C₁ ≌ C₂` and isomorphism `L₁ ≅ E.functor ⋙ L₂`, where `W₂` is the inverse image of `W₁` under `E.functor` and is inverted by `L₂`, then `L₂` is a localization of `W₂` in category `C₂`.
|
CategoryTheory.Functor.IsLocalization.of_equivalences
theorem CategoryTheory.Functor.IsLocalization.of_equivalences :
∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [inst : CategoryTheory.Category.{u_6, u_1} C₁]
[inst_1 : CategoryTheory.Category.{u_8, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_7, u_4} D₁]
[inst_3 : CategoryTheory.Category.{u_9, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁)
(W₁ : CategoryTheory.MorphismProperty C₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
(W₂ : CategoryTheory.MorphismProperty C₂) (E : C₁ ≌ C₂) (E' : D₁ ≌ D₂)
[inst_5 : CategoryTheory.CatCommSq E.functor L₁ L₂ E'.functor],
W₁ ≤ W₂.isoClosure.inverseImage E.functor → W₂.IsInvertedBy L₂ → L₂.IsLocalization W₂
The theorem `CategoryTheory.Functor.IsLocalization.of_equivalences` states that if there is a localization functor `L₁` for a morphism property `W₁` in category `C₁` which maps to category `D₁`, then after transporting this functor `L₁` via equivalences from `C₁` to `C₂` and `D₁` to `D₂` to get a new functor `L₂` from `C₂` to `D₂`, `L₂` is also a localization functor for a suitable morphism property `W₂` in `C₂`. This is contingent on `W₁` being a subset of the inverse image of `W₂` under the equivalence from `C₁` to `C₂`, and `W₂` being inverted by `L₂`.
More concisely: If `L₁` is a localization functor in category `C₁` for morphism property `W₁` and there are equivalences `F : C₁ ⟶ C₂` and `G : D₁ ⟶ D₂`, then `L₂ = L₁ ∘ F` is a localization functor in category `C₂` for morphism property `W₂ = {F(w) | w ∈ W₁} ∩ W₂`, if `W₂` is inverted by `L₂`.
|