Theorems · Definition · category theory

CategoryTheory.Adjunction.localization

{C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                {G : CategoryTheory.Functor C₁ C₂} →
                  {F : CategoryTheory.Functor C₂ C₁} →
                    (G ⊣ F) →
                      (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 D₁ D₂) →
                                    (F' : CategoryTheory.Functor D₂ D₁) →
                                      [CategoryTheory.CatCommSq G L₁ L₂ G'] →
                                        [CategoryTheory.CatCommSq F L₂ L₁ F'] → G' ⊣ F'

If adj : G ⊣ F is an adjunction between two categories C₁ and C₂ that are equipped with localization functors L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ with respect to W₁ : MorphismProperty C₁ and W₂ : MorphismProperty C₂, and that the functors F : C₂ ⥤ C₁ and G : C₁ ⥤ C₂ induce functors F' : D₂ ⥤ D₁ and G' : D₁ ⥤ D₂ on the localized categories, then the adjunction adj induces an adjunction G' ⊣ F'.

Defined in

Mathlib.CategoryTheory.Localization.Adjunction

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationCategoryTheory.CatCommSqCategoryTheory.CatCommSq