Commit 2024-06-24 08:03 0b2d94a0
View on Github →feat: bijections between morphisms in two localized categories (#13956)
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.