Documentation

Mathlib.CategoryTheory.Localization.Adjunction

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'.

source
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₁) [CategoryTheory.Functor.IsLocalization L₁ 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₁ ⟶ CategoryTheory.Functor.comp G' 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.
Instances For
    source
    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₁) [CategoryTheory.Functor.IsLocalization L₁ 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₁)))
    source
    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₂) [CategoryTheory.Functor.IsLocalization L₂ W₂] (G' : CategoryTheory.Functor D₁ D₂) (F' : CategoryTheory.Functor D₂ D₁) [CategoryTheory.CatCommSq G L₁ L₂ G'] [CategoryTheory.CatCommSq F L₂ L₁ F'] :
    CategoryTheory.Functor.comp F' 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.
    Instances For
      source
      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₂) [CategoryTheory.Functor.IsLocalization L₂ 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₂)))
      source
      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₁) [CategoryTheory.Functor.IsLocalization L₁ W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [CategoryTheory.Functor.IsLocalization L₂ 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.
      Instances For
        source
        @[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₁) [CategoryTheory.Functor.IsLocalization L₁ W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [CategoryTheory.Functor.IsLocalization L₂ 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₁ 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₁)))
        source
        @[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₁) [CategoryTheory.Functor.IsLocalization L₁ W₁] (L₂ : CategoryTheory.Functor C₂ D₂) (W₂ : CategoryTheory.MorphismProperty C₂) [CategoryTheory.Functor.IsLocalization L₂ 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₁ 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₂)))