Theorems · Definition · category theory

CategoryTheory.Localization.equivalence

{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D₁] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D₂] →
                (L₁ : CategoryTheory.Functor C₁ D₁) →
                  (W₁ : CategoryTheory.MorphismProperty C₁) →
                    [L₁.IsLocalization W₁] →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₂ : CategoryTheory.MorphismProperty C₂) →
                          [L₂.IsLocalization W₂] →
                            (G : CategoryTheory.Functor C₁ D₂) →
                              (G' : CategoryTheory.Functor D₁ D₂) →
                                [CategoryTheory.Localization.Lifting L₁ W₁ G G'] →
                                  (F : CategoryTheory.Functor C₂ D₁) →
                                    (F' : CategoryTheory.Functor D₂ D₁) →
                                      [CategoryTheory.Localization.Lifting L₂ W₂ F F'] →
                                        (G.comp F' ≅ L₁) → (F.comp G' ≅ L₂) → (D₁ ≌ D₂)

Basic constructor of an equivalence between localized categories

Defined in

Mathlib.CategoryTheory.Localization.Equivalence

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationCategoryTheory.Localization.LiftingCategoryTheory.Localization.Lifting