feat: localization of adjunctions between categories (#6235)

This PR shows that under suitable assumptions, adjunctions can be localized.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: joelriou

Mathlib.lean

@@ -1044,6 +1044,7 @@ import Mathlib.CategoryTheory.Linear.Basic
 import Mathlib.CategoryTheory.Linear.FunctorCategory
 import Mathlib.CategoryTheory.Linear.LinearFunctor
 import Mathlib.CategoryTheory.Linear.Yoneda
+import Mathlib.CategoryTheory.Localization.Adjunction
 import Mathlib.CategoryTheory.Localization.Construction
 import Mathlib.CategoryTheory.Localization.Equivalence
 import Mathlib.CategoryTheory.Localization.Opposite

Mathlib/CategoryTheory/Localization/Adjunction.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2023 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+import Mathlib.CategoryTheory.CatCommSq
+import Mathlib.CategoryTheory.Localization.Predicate
+
+/-!
+# 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 `adj.localization L₁ W₁ L₂ W₂ G' F' : G' ⊣ F'`.
+
+-/
+
+namespace CategoryTheory
+
+open Localization Category
+
+variable {C₁ C₂ D₁ D₂ : Type _} [Category C₁] [Category C₂] [Category D₁] [Category D₂]
+  {G : C₁ ⥤ C₂} {F : C₂ ⥤ C₁} (adj : G ⊣ F)
+  (L₁ : C₁ ⥤ D₁) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁]
+  (L₂ : C₂ ⥤ D₂) (W₂ : MorphismProperty C₂) [L₂.IsLocalization W₂]
+  (G' : D₁ ⥤ D₂) (F' : D₂ ⥤ D₁)
+  [CatCommSq G L₁ L₂ G'] [CatCommSq F L₂ L₁ F']
+
+namespace Adjunction
+
+namespace Localization
+
+/-- Auxiliary definition of the unit morphism for the adjunction `Adjunction.localization` -/
+noncomputable def ε : 𝟭 D₁ ⟶ G' ⋙ F' := by
+  letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') :=
+    Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso'.symm
+  exact Localization.liftNatTrans L₁ W₁ L₁ ((G ⋙ F) ⋙ L₁) (𝟭 D₁) (G' ⋙ F')
+    (whiskerRight adj.unit L₁)
+
+lemma ε_app (X₁ : C₁) :
+    (ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) =
+      L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫
+        F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) := by
+  letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') :=
+    Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso'.symm
+  simp only [ε, liftNatTrans_app, Lifting.iso, Iso.symm,
+    Functor.id_obj, Functor.comp_obj, Lifting.id_iso', Functor.rightUnitor_hom_app,
+      whiskerRight_app, CatCommSq.hComp_iso'_hom_app, id_comp]
+
+/-- Auxiliary definition of the counit morphism for the adjunction `Adjunction.localization` -/
+noncomputable def η : F' ⋙ G' ⟶ 𝟭 D₂ := by
+  letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') :=
+    Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso'.symm
+  exact liftNatTrans L₂ W₂ ((F ⋙ G) ⋙ L₂) L₂ (F' ⋙ G') (𝟭 D₂) (whiskerRight adj.counit L₂)
+
+lemma η_app (X₂ : C₂) :
+    (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
+      G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
+        (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫
+        L₂.map (adj.counit.app X₂) := by
+  letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') :=
+    Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso'.symm
+  simp only [η, liftNatTrans_app, Lifting.iso, Iso.symm, CatCommSq.hComp_iso'_inv_app,
+    whiskerRight_app, Lifting.id_iso', Functor.rightUnitor_inv_app, comp_id, assoc]
+
+end Localization
+
+/-- 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'`. -/
+noncomputable def localization : G' ⊣ F' :=
+  Adjunction.mkOfUnitCounit
+    { unit := Localization.ε adj L₁ W₁ L₂ G' F'
+      counit := Localization.η adj L₁ L₂ W₂ G' F'
+      left_triangle := by
+        apply natTrans_ext L₁ W₁
+        intro X₁
+        have eq := congr_app adj.left_triangle X₁
+        dsimp at eq
+        rw [NatTrans.comp_app, NatTrans.comp_app, whiskerRight_app, Localization.ε_app,
+          Functor.associator_hom_app, id_comp, whiskerLeft_app, G'.map_comp, G'.map_comp,
+          assoc, assoc]
+        erw [(Localization.η adj L₁ L₂ W₂ G' F').naturality, Localization.η_app,
+          assoc, assoc, ← G'.map_comp_assoc, ← G'.map_comp_assoc, assoc, Iso.hom_inv_id_app,
+          comp_id, (CatCommSq.iso G L₁ L₂ G').inv.naturality_assoc, ← L₂.map_comp_assoc, eq,
+          L₂.map_id, id_comp, Iso.inv_hom_id_app]
+        rfl
+      right_triangle := by
+        apply natTrans_ext L₂ W₂
+        intro X₂
+        have eq := congr_app adj.right_triangle X₂
+        dsimp at eq
+        rw [NatTrans.comp_app, NatTrans.comp_app, whiskerLeft_app, whiskerRight_app,
+          Localization.η_app, Functor.associator_inv_app, id_comp, F'.map_comp, F'.map_comp]
+        erw [← (Localization.ε _ _ _ _ _ _).naturality_assoc, Localization.ε_app,
+          assoc, assoc, ← F'.map_comp_assoc, Iso.hom_inv_id_app, F'.map_id, id_comp,
+          ← NatTrans.naturality, ← L₁.map_comp_assoc, eq, L₁.map_id, id_comp,
+          Iso.inv_hom_id_app]
+        rfl }
+
+@[simp]
+lemma localization_unit_app (X₁ : C₁) :
+  (adj.localization L₁ W₁ L₂ W₂ G' F').unit.app (L₁.obj X₁) =
+    L₁.map (adj.unit.app X₁) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫
+      F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) := by
+  apply Localization.ε_app
+
+@[simp]
+lemma localization_counit_app (X₂ : C₂) :
+  (adj.localization L₁ W₁ L₂ W₂ G' F').counit.app (L₂.obj X₂) =
+    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
+      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫
+      L₂.map (adj.counit.app X₂) := by
+  apply Localization.η_app
+
+end Adjunction
+
+end CategoryTheory