Localization of adjunctions

In this file, we show that if we have an adjunction adj : G ⊣ F such that both functors G : C₁ ⥤ C₂ and F : C₂ ⥤ C₁ induce functors G' : D₁ ⥤ D₂ and F' : D₂ ⥤ D₁ on localized categories, i.e. that we have localization functors L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ with respect to morphism properties W₁ and W₂ respectively, and 2-commutative diagrams [CatCommSq G L₁ L₂ G'] and [CatCommSq F L₂ L₁ F'], then we have an induced adjunction Adjunction.localization L₁ W₁ L₂ W₂ G' F' : G' ⊣ F'.

noncomputable def CategoryTheory.Adjunction.Localization.ε {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D₁] [CategoryTheory.Category.{u_8, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁} (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (G' : CategoryTheory.Functor D₁ D₂) (F' : CategoryTheory.Functor D₂ D₁) [CategoryTheory.CatCommSq G L₁ L₂ G'] [CategoryTheory.CatCommSq F L₂ L₁ F'] : CategoryTheory.Functor.id D₁ ⟶ G'.comp F'

Auxiliary definition of the unit morphism for the adjunction Adjunction.localization

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Adjunction.Localization.ε_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_5, u_3} D₁] [CategoryTheory.Category.{u_7, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁} (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (W₁ : CategoryTheory.MorphismProperty C₁) [L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (G' : CategoryTheory.Functor D₁ D₂) (F' : CategoryTheory.Functor D₂ D₁) [CategoryTheory.CatCommSq G L₁ L₂ G'] [CategoryTheory.CatCommSq F L₂ L₁ F'] (X₁ : C₁) : (CategoryTheory.Adjunction.Localization.ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) = CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) (F'.map ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').hom.app X₁)))

noncomputable def CategoryTheory.Adjunction.Localization.η {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D₁] [CategoryTheory.Category.{u_8, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁} (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (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'] : F'.comp G' ⟶ CategoryTheory.Functor.id D₂

Auxiliary definition of the counit morphism for the adjunction Adjunction.localization

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Adjunction.Localization.η_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D₁] [CategoryTheory.Category.{u_5, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁} (adj : G ⊣ F) (L₁ : CategoryTheory.Functor C₁ D₁) (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'] (X₂ : C₂) : (CategoryTheory.Adjunction.Localization.η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) = CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').inv.app X₂)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) (L₂.map (adj.counit.app X₂)))

noncomputable def CategoryTheory.Adjunction.localization {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_5, u_1} C₁] [CategoryTheory.Category.{u_6, u_2} C₂] [CategoryTheory.Category.{u_7, u_3} D₁] [CategoryTheory.Category.{u_8, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁} (adj : 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'.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Adjunction.localization_unit_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_5, u_3} D₁] [CategoryTheory.Category.{u_7, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁} (adj : 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'] (X₁ : C₁) : (adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) = CategoryTheory.CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁)) (F'.map ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').hom.app X₁)))

@[simp]

theorem CategoryTheory.Adjunction.localization_counit_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_7, u_2} C₂] [CategoryTheory.Category.{u_6, u_3} D₁] [CategoryTheory.Category.{u_5, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁} (adj : 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'] (X₂ : C₂) : (adj.localization L₁ W₁ L₂ W₂ G' F').counit.app (L₂.obj X₂) = CategoryTheory.CategoryStruct.comp (G'.map ((CategoryTheory.CatCommSq.iso F L₂ L₁ F').inv.app X₂)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂)) (L₂.map (adj.counit.app X₂)))

theorem CategoryTheory.Adjunction.isLocalization {C₁ : Type u_1} {C₂ : Type u_2} [CategoryTheory.Category.{u_6, u_1} C₁] [CategoryTheory.Category.{u_5, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁} (adj : G ⊣ F) [F.Full] [F.Faithful] : G.IsLocalization ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G)