Theorems · Definition · category theory

CategoryTheory.Localization.homEquiv

{C : Type u_1} →
  {D₁ : Type u_5} →
    {D₂ : Type u_6} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] →
          [inst_2 : CategoryTheory.Category.{v_6, 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} → (L₁.obj X ⟶ L₁.obj Y) ≃ (L₂.obj X ⟶ L₂.obj Y)

Bijection between types of morphisms in two localized categories for the same class of morphisms W.

Defined in

Mathlib.CategoryTheory.Localization.HomEquiv

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalization