Bijections between morphisms in two localized categories #
Given two localization functors L₁ : C ⥤ D₁ and L₂ : C ⥤ D₂ for the same
class of morphisms W : MorphismProperty C, we define a bijection
Localization.homEquiv W L₁ L₂ : (L₁.obj X ⟶ L₁.obj Y) ≃ (L₂.obj X ⟶ L₂.obj Y)
between the types of morphisms in the two localized categories.
More generally, given a localizer morphism Φ : LocalizerMorphism W₁ W₂, we define a map
Φ.homMap L₁ L₂ : (L₁.obj X ⟶ L₁.obj Y) ⟶ (L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y)).
The definition Localization.homEquiv is obtained by applying the construction
to the identity localizer morphism.
noncomputable def
CategoryTheory.LocalizerMorphism.homMap
{C₁ : Type u_2}
{C₂ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_8, u_2} C₁]
[CategoryTheory.Category.{u_9, u_3} C₂]
[CategoryTheory.Category.{u_10, u_5} D₁]
[CategoryTheory.Category.{u_11, u_6} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
{X Y : C₁}
(f : L₁.obj X ⟶ L₁.obj Y)
:
L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y)
If Φ : LocalizerMorphism W₁ W₂ is a morphism of localizers, L₁ and L₂
are localization functors for W₁ and W₂, then this is the induced map
(L₁.obj X ⟶ L₁.obj Y) ⟶ (L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
for all objects X and Y.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.LocalizerMorphism.homMap_map
{C₁ : Type u_2}
{C₂ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_8, u_2} C₁]
[CategoryTheory.Category.{u_10, u_3} C₂]
[CategoryTheory.Category.{u_11, u_5} D₁]
[CategoryTheory.Category.{u_9, u_6} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
{X Y : C₁}
(f : X ⟶ Y)
:
Φ.homMap L₁ L₂ (L₁.map f) = L₂.map (Φ.functor.map f)
@[simp]
theorem
CategoryTheory.LocalizerMorphism.homMap_id
{C₁ : Type u_2}
{C₂ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_10, u_2} C₁]
[CategoryTheory.Category.{u_9, u_3} C₂]
[CategoryTheory.Category.{u_11, u_5} D₁]
[CategoryTheory.Category.{u_8, u_6} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
(X : C₁)
:
Φ.homMap L₁ L₂ (CategoryTheory.CategoryStruct.id (L₁.obj X)) = CategoryTheory.CategoryStruct.id (L₂.obj (Φ.functor.obj X))
theorem
CategoryTheory.LocalizerMorphism.homMap_comp
{C₁ : Type u_2}
{C₂ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_9, u_2} C₁]
[CategoryTheory.Category.{u_11, u_3} C₂]
[CategoryTheory.Category.{u_8, u_5} D₁]
[CategoryTheory.Category.{u_10, u_6} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
{X Y Z : C₁}
(f : L₁.obj X ⟶ L₁.obj Y)
(g : L₁.obj Y ⟶ L₁.obj Z)
:
Φ.homMap L₁ L₂ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ f) (Φ.homMap L₁ L₂ g)
theorem
CategoryTheory.LocalizerMorphism.homMap_comp_assoc
{C₁ : Type u_2}
{C₂ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_9, u_2} C₁]
[CategoryTheory.Category.{u_11, u_3} C₂]
[CategoryTheory.Category.{u_8, u_5} D₁]
[CategoryTheory.Category.{u_10, u_6} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
{X Y Z : C₁}
(f : L₁.obj X ⟶ L₁.obj Y)
(g : L₁.obj Y ⟶ L₁.obj Z)
{Z✝ : D₂}
(h : L₂.obj (Φ.functor.obj Z) ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ f) (CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ g) h)
theorem
CategoryTheory.LocalizerMorphism.homMap_apply
{C₁ : Type u_2}
{C₂ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_10, u_2} C₁]
[CategoryTheory.Category.{u_11, u_3} C₂]
[CategoryTheory.Category.{u_8, u_5} D₁]
[CategoryTheory.Category.{u_9, u_6} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
{X Y : C₁}
(G : CategoryTheory.Functor D₁ D₂)
(e : Φ.functor.comp L₂ ≅ L₁.comp G)
(f : L₁.obj X ⟶ L₁.obj Y)
:
Φ.homMap L₁ L₂ f = CategoryTheory.CategoryStruct.comp (e.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (e.inv.app Y))
theorem
CategoryTheory.LocalizerMorphism.homMap_apply_assoc
{C₁ : Type u_2}
{C₂ : Type u_3}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_10, u_2} C₁]
[CategoryTheory.Category.{u_11, u_3} C₂]
[CategoryTheory.Category.{u_8, u_5} D₁]
[CategoryTheory.Category.{u_9, u_6} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
{X Y : C₁}
(G : CategoryTheory.Functor D₁ D₂)
(e : Φ.functor.comp L₂ ≅ L₁.comp G)
(f : L₁.obj X ⟶ L₁.obj Y)
{Z : D₂}
(h : L₂.obj (Φ.functor.obj Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (Φ.homMap L₁ L₂ f) h = CategoryTheory.CategoryStruct.comp (e.hom.app X)
(CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.CategoryStruct.comp (e.inv.app Y) h))
@[simp]
theorem
CategoryTheory.LocalizerMorphism.id_homMap
{C₁ : Type u_2}
{D₁ : Type u_5}
[CategoryTheory.Category.{u_9, u_2} C₁]
[CategoryTheory.Category.{u_8, u_5} D₁]
{W₁ : CategoryTheory.MorphismProperty C₁}
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
{X Y : C₁}
(f : L₁.obj X ⟶ L₁.obj Y)
:
(CategoryTheory.LocalizerMorphism.id W₁).homMap L₁ L₁ f = f
@[simp]
theorem
CategoryTheory.LocalizerMorphism.homMap_homMap
{C₁ : Type u_2}
{C₂ : Type u_3}
{C₃ : Type u_4}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[CategoryTheory.Category.{u_9, u_2} C₁]
[CategoryTheory.Category.{u_12, u_3} C₂]
[CategoryTheory.Category.{u_11, u_4} C₃]
[CategoryTheory.Category.{u_8, u_5} D₁]
[CategoryTheory.Category.{u_13, u_6} D₂]
[CategoryTheory.Category.{u_10, u_7} D₃]
{W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂}
{W₃ : CategoryTheory.MorphismProperty C₃}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
(Ψ : CategoryTheory.LocalizerMorphism W₂ W₃)
(L₁ : CategoryTheory.Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : CategoryTheory.Functor C₂ D₂)
[L₂.IsLocalization W₂]
(L₃ : CategoryTheory.Functor C₃ D₃)
[L₃.IsLocalization W₃]
{X Y : C₁}
(f : L₁.obj X ⟶ L₁.obj Y)
:
Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f
noncomputable def
CategoryTheory.Localization.homEquiv
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_8, u_1} C]
[CategoryTheory.Category.{u_9, u_5} D₁]
[CategoryTheory.Category.{u_10, u_6} D₂]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
:
Bijection between types of morphisms in two localized categories
for the same class of morphisms W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Localization.homEquiv_apply
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_8, u_1} C]
[CategoryTheory.Category.{u_9, u_5} D₁]
[CategoryTheory.Category.{u_10, u_6} D₂]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(f : L₁.obj X ⟶ L₁.obj Y)
:
(CategoryTheory.Localization.homEquiv W L₁ L₂) f = (CategoryTheory.LocalizerMorphism.id W).homMap L₁ L₂ f
@[simp]
theorem
CategoryTheory.Localization.homEquiv_symm_apply
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_9, u_1} C]
[CategoryTheory.Category.{u_10, u_5} D₁]
[CategoryTheory.Category.{u_8, u_6} D₂]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(g : L₂.obj X ⟶ L₂.obj Y)
:
(CategoryTheory.Localization.homEquiv W L₁ L₂).symm g = (CategoryTheory.Localization.homEquiv W L₂ L₁) g
theorem
CategoryTheory.Localization.homEquiv_eq
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_10, u_1} C]
[CategoryTheory.Category.{u_8, u_5} D₁]
[CategoryTheory.Category.{u_9, u_6} D₂]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(G : CategoryTheory.Functor D₁ D₂)
(e : L₁.comp G ≅ L₂)
(f : L₁.obj X ⟶ L₁.obj Y)
:
(CategoryTheory.Localization.homEquiv W L₁ L₂) f = CategoryTheory.CategoryStruct.comp (e.inv.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (e.hom.app Y))
@[simp]
theorem
CategoryTheory.Localization.homEquiv_refl
{C : Type u_1}
{D₁ : Type u_5}
[CategoryTheory.Category.{u_9, u_1} C]
[CategoryTheory.Category.{u_8, u_5} D₁]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
{X Y : C}
(f : L₁.obj X ⟶ L₁.obj Y)
:
(CategoryTheory.Localization.homEquiv W L₁ L₁) f = f
theorem
CategoryTheory.Localization.homEquiv_trans
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[CategoryTheory.Category.{u_9, u_1} C]
[CategoryTheory.Category.{u_8, u_5} D₁]
[CategoryTheory.Category.{u_11, u_6} D₂]
[CategoryTheory.Category.{u_10, u_7} D₃]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
(L₃ : CategoryTheory.Functor C D₃)
[L₃.IsLocalization W]
{X Y : C}
(f : L₁.obj X ⟶ L₁.obj Y)
:
(CategoryTheory.Localization.homEquiv W L₂ L₃) ((CategoryTheory.Localization.homEquiv W L₁ L₂) f) = (CategoryTheory.Localization.homEquiv W L₁ L₃) f
theorem
CategoryTheory.Localization.homEquiv_comp
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_9, u_1} C]
[CategoryTheory.Category.{u_8, u_5} D₁]
[CategoryTheory.Category.{u_10, u_6} D₂]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
{X Y Z : C}
(f : L₁.obj X ⟶ L₁.obj Y)
(g : L₁.obj Y ⟶ L₁.obj Z)
:
(CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.homEquiv W L₁ L₂) f)
((CategoryTheory.Localization.homEquiv W L₁ L₂) g)
@[simp]
theorem
CategoryTheory.Localization.homEquiv_map
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_8, u_1} C]
[CategoryTheory.Category.{u_10, u_5} D₁]
[CategoryTheory.Category.{u_9, u_6} D₂]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(f : X ⟶ Y)
:
(CategoryTheory.Localization.homEquiv W L₁ L₂) (L₁.map f) = L₂.map f
@[simp]
theorem
CategoryTheory.Localization.homEquiv_id
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_9, u_1} C]
[CategoryTheory.Category.{u_10, u_5} D₁]
[CategoryTheory.Category.{u_8, u_6} D₂]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
(X : C)
:
(CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.CategoryStruct.id (L₁.obj X)) = CategoryTheory.CategoryStruct.id (L₂.obj X)
theorem
CategoryTheory.Localization.homEquiv_isoOfHom_inv
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[CategoryTheory.Category.{u_8, u_1} C]
[CategoryTheory.Category.{u_10, u_5} D₁]
[CategoryTheory.Category.{u_9, u_6} D₂]
(W : CategoryTheory.MorphismProperty C)
(L₁ : CategoryTheory.Functor C D₁)
[L₁.IsLocalization W]
(L₂ : CategoryTheory.Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(f : Y ⟶ X)
(hf : W f)
:
(CategoryTheory.Localization.homEquiv W L₁ L₂) (CategoryTheory.Localization.isoOfHom L₁ W f hf).inv = (CategoryTheory.Localization.isoOfHom L₂ W f hf).inv