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}
[Category.{u_8, u_2} C₁]
[Category.{u_9, u_3} C₂]
[Category.{u_10, u_5} D₁]
[Category.{u_11, u_6} D₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : 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}
[Category.{u_8, u_2} C₁]
[Category.{u_10, u_3} C₂]
[Category.{u_11, u_5} D₁]
[Category.{u_9, u_6} D₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : 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}
[Category.{u_10, u_2} C₁]
[Category.{u_9, u_3} C₂]
[Category.{u_11, u_5} D₁]
[Category.{u_8, u_6} D₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : Functor C₂ D₂)
[L₂.IsLocalization W₂]
(X : C₁)
:
Φ.homMap L₁ L₂ (CategoryStruct.id (L₁.obj X)) = 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}
[Category.{u_9, u_2} C₁]
[Category.{u_11, u_3} C₂]
[Category.{u_8, u_5} D₁]
[Category.{u_10, u_6} D₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : 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₂ (CategoryStruct.comp f g) = 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}
[Category.{u_9, u_2} C₁]
[Category.{u_11, u_3} C₂]
[Category.{u_8, u_5} D₁]
[Category.{u_10, u_6} D₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : 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✝)
:
CategoryStruct.comp (Φ.homMap L₁ L₂ (CategoryStruct.comp f g)) h = CategoryStruct.comp (Φ.homMap L₁ L₂ f) (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}
[Category.{u_10, u_2} C₁]
[Category.{u_11, u_3} C₂]
[Category.{u_8, u_5} D₁]
[Category.{u_9, u_6} D₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : Functor C₂ D₂)
[L₂.IsLocalization W₂]
{X Y : C₁}
(G : Functor D₁ D₂)
(e : Φ.functor.comp L₂ ≅ L₁.comp G)
(f : L₁.obj X ⟶ L₁.obj Y)
:
Φ.homMap L₁ L₂ f = CategoryStruct.comp (e.hom.app X) (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}
[Category.{u_10, u_2} C₁]
[Category.{u_11, u_3} C₂]
[Category.{u_8, u_5} D₁]
[Category.{u_9, u_6} D₂]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
(Φ : LocalizerMorphism W₁ W₂)
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : Functor C₂ D₂)
[L₂.IsLocalization W₂]
{X Y : C₁}
(G : 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)
:
CategoryStruct.comp (Φ.homMap L₁ L₂ f) h = CategoryStruct.comp (e.hom.app X) (CategoryStruct.comp (G.map f) (CategoryStruct.comp (e.inv.app Y) h))
@[simp]
theorem
CategoryTheory.LocalizerMorphism.id_homMap
{C₁ : Type u_2}
{D₁ : Type u_5}
[Category.{u_9, u_2} C₁]
[Category.{u_8, u_5} D₁]
{W₁ : MorphismProperty C₁}
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
{X Y : C₁}
(f : L₁.obj X ⟶ L₁.obj Y)
:
@[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}
[Category.{u_9, u_2} C₁]
[Category.{u_12, u_3} C₂]
[Category.{u_11, u_4} C₃]
[Category.{u_8, u_5} D₁]
[Category.{u_13, u_6} D₂]
[Category.{u_10, u_7} D₃]
{W₁ : MorphismProperty C₁}
{W₂ : MorphismProperty C₂}
{W₃ : MorphismProperty C₃}
(Φ : LocalizerMorphism W₁ W₂)
(Ψ : LocalizerMorphism W₂ W₃)
(L₁ : Functor C₁ D₁)
[L₁.IsLocalization W₁]
(L₂ : Functor C₂ D₂)
[L₂.IsLocalization W₂]
(L₃ : 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}
[Category.{u_8, u_1} C]
[Category.{u_9, u_5} D₁]
[Category.{u_10, u_6} D₂]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : 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}
[Category.{u_8, u_1} C]
[Category.{u_9, u_5} D₁]
[Category.{u_10, u_6} D₂]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(f : L₁.obj X ⟶ L₁.obj Y)
:
(homEquiv W L₁ L₂) f = (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}
[Category.{u_9, u_1} C]
[Category.{u_10, u_5} D₁]
[Category.{u_8, u_6} D₂]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(g : L₂.obj X ⟶ L₂.obj Y)
:
theorem
CategoryTheory.Localization.homEquiv_eq
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{u_10, u_1} C]
[Category.{u_8, u_5} D₁]
[Category.{u_9, u_6} D₂]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(G : Functor D₁ D₂)
(e : L₁.comp G ≅ L₂)
(f : L₁.obj X ⟶ L₁.obj Y)
:
(homEquiv W L₁ L₂) f = CategoryStruct.comp (e.inv.app X) (CategoryStruct.comp (G.map f) (e.hom.app Y))
@[simp]
theorem
CategoryTheory.Localization.homEquiv_refl
{C : Type u_1}
{D₁ : Type u_5}
[Category.{u_9, u_1} C]
[Category.{u_8, u_5} D₁]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
{X Y : C}
(f : L₁.obj X ⟶ L₁.obj Y)
:
theorem
CategoryTheory.Localization.homEquiv_trans
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
{D₃ : Type u_7}
[Category.{u_9, u_1} C]
[Category.{u_8, u_5} D₁]
[Category.{u_11, u_6} D₂]
[Category.{u_10, u_7} D₃]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : Functor C D₂)
[L₂.IsLocalization W]
(L₃ : Functor C D₃)
[L₃.IsLocalization W]
{X Y : C}
(f : L₁.obj X ⟶ L₁.obj Y)
:
theorem
CategoryTheory.Localization.homEquiv_comp
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{u_9, u_1} C]
[Category.{u_8, u_5} D₁]
[Category.{u_10, u_6} D₂]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : Functor C D₂)
[L₂.IsLocalization W]
{X Y Z : C}
(f : L₁.obj X ⟶ L₁.obj Y)
(g : L₁.obj Y ⟶ L₁.obj Z)
:
(homEquiv W L₁ L₂) (CategoryStruct.comp f g) = CategoryStruct.comp ((homEquiv W L₁ L₂) f) ((homEquiv W L₁ L₂) g)
@[simp]
theorem
CategoryTheory.Localization.homEquiv_map
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{u_8, u_1} C]
[Category.{u_10, u_5} D₁]
[Category.{u_9, u_6} D₂]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Localization.homEquiv_id
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{u_9, u_1} C]
[Category.{u_10, u_5} D₁]
[Category.{u_8, u_6} D₂]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : Functor C D₂)
[L₂.IsLocalization W]
(X : C)
:
(homEquiv W L₁ L₂) (CategoryStruct.id (L₁.obj X)) = CategoryStruct.id (L₂.obj X)
theorem
CategoryTheory.Localization.homEquiv_isoOfHom_inv
{C : Type u_1}
{D₁ : Type u_5}
{D₂ : Type u_6}
[Category.{u_8, u_1} C]
[Category.{u_10, u_5} D₁]
[Category.{u_9, u_6} D₂]
(W : MorphismProperty C)
(L₁ : Functor C D₁)
[L₁.IsLocalization W]
(L₂ : Functor C D₂)
[L₂.IsLocalization W]
{X Y : C}
(f : Y ⟶ X)
(hf : W f)
: