From 292fc0423c6c1a679ddf564f36413ce23951d2a7 Mon Sep 17 00:00:00 2001
From: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Sun, 24 May 2020 15:07:07 +0000
Subject: [PATCH] feat(category_theory): adjunction convenience defs (#2754)

Transport adjunctions along natural isomorphisms, and `is_left_adjoint` or `is_right_adjoint` versions of existing adjunction properties.
---
 src/category_theory/adjunction/basic.lean | 86 ++++++++++++++++++++++-
 1 file changed, 85 insertions(+), 1 deletion(-)

diff --git a/src/category_theory/adjunction/basic.lean b/src/category_theory/adjunction/basic.lean
index 82c75b27a7732..98631f30a4cca 100644
--- a/src/category_theory/adjunction/basic.lean
+++ b/src/category_theory/adjunction/basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Reid Barton. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Reid Barton, Johan Commelin
+Authors: Reid Barton, Johan Commelin, Bhavik Mehta
 -/
 import category_theory.equivalence
 import data.equiv.basic
@@ -204,9 +204,68 @@ def id : 𝟭 C ⊣ 𝟭 C :=
   unit := 𝟙 _,
   counit := 𝟙 _ }
 
+/-- If F and G are naturally isomorphic functors, establish an equivalence of hom-sets. -/
+def equiv_homset_left_of_nat_iso
+  {F F' : C ⥤ D} (iso : F ≅ F') {X : C} {Y : D} :
+  (F.obj X ⟶ Y) ≃ (F'.obj X ⟶ Y) :=
+{ to_fun := λ f, iso.inv.app _ ≫ f,
+  inv_fun := λ g, iso.hom.app _ ≫ g,
+  left_inv := λ f, by simp,
+  right_inv := λ g, by simp }
+
+@[simp]
+lemma equiv_homset_left_of_nat_iso_apply {F F' : C ⥤ D} (iso : F ≅ F') {X : C} {Y : D} (f : F.obj X ⟶ Y) :
+  (equiv_homset_left_of_nat_iso iso) f = iso.inv.app _ ≫ f := rfl
+
+@[simp]
+lemma equiv_homset_left_of_nat_iso_symm_apply {F F' : C ⥤ D} (iso : F ≅ F') {X : C} {Y : D} (g : F'.obj X ⟶ Y) :
+  (equiv_homset_left_of_nat_iso iso).symm g = iso.hom.app _ ≫ g := rfl
+
+/-- If G and H are naturally isomorphic functors, establish an equivalence of hom-sets. -/
+def equiv_homset_right_of_nat_iso
+  {G G' : D ⥤ C} (iso : G ≅ G') {X : C} {Y : D} :
+  (X ⟶ G.obj Y) ≃ (X ⟶ G'.obj Y) :=
+{ to_fun := λ f, f ≫ iso.hom.app _,
+  inv_fun := λ g, g ≫ iso.inv.app _,
+  left_inv := λ f, by simp,
+  right_inv := λ g, by simp }
+
+@[simp]
+lemma equiv_homset_right_of_nat_iso_apply {G G' : D ⥤ C} (iso : G ≅ G') {X : C} {Y : D} (f : X ⟶ G.obj Y)  :
+  (equiv_homset_right_of_nat_iso iso) f = f ≫ iso.hom.app _ := rfl
+
+@[simp]
+lemma equiv_homset_right_of_nat_iso_symm_apply {G G' : D ⥤ C} (iso : G ≅ G') {X : C} {Y : D} (g : X ⟶ G'.obj Y) :
+  (equiv_homset_right_of_nat_iso iso).symm g = g ≫ iso.inv.app _ := rfl
+
+/-- Transport an adjunction along an natural isomorphism on the left. -/
+def of_nat_iso_left
+  {F G : C ⥤ D} {H : D ⥤ C} (adj : F ⊣ H) (iso : F ≅ G) :
+  G ⊣ H :=
+adjunction.mk_of_hom_equiv
+{ hom_equiv := λ X Y, (equiv_homset_left_of_nat_iso iso.symm).trans (adj.hom_equiv X Y) }
+
+/-- Transport an adjunction along an natural isomorphism on the right. -/
+def of_nat_iso_right
+  {F : C ⥤ D} {G H : D ⥤ C} (adj : F ⊣ G) (iso : G ≅ H) :
+  F ⊣ H :=
+adjunction.mk_of_hom_equiv
+{ hom_equiv := λ X Y, (adj.hom_equiv X Y).trans (equiv_homset_right_of_nat_iso iso) }
+
+/-- Transport being a right adjoint along a natural isomorphism. -/
+def right_adjoint_of_nat_iso {F G : C ⥤ D} (h : F ≅ G) [r : is_right_adjoint F] : is_right_adjoint G :=
+{ left := r.left,
+  adj := of_nat_iso_right r.adj h }
+
+/-- Transport being a left adjoint along a natural isomorphism. -/
+def left_adjoint_of_nat_iso {F G : C ⥤ D} (h : F ≅ G) [r : is_left_adjoint F] : is_left_adjoint G :=
+{ right := r.right,
+  adj := of_nat_iso_left r.adj h }
+
 section
 variables {E : Type u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
 
+/-- Show that adjunctions can be composed. -/
 def comp (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F ⋙ H ⊣ I ⋙ G :=
 { hom_equiv := λ X Z, equiv.trans (adj₂.hom_equiv _ _) (adj₁.hom_equiv _ _),
   unit := adj₁.unit ≫
@@ -214,6 +273,18 @@ def comp (adj₁ : F ⊣ G) (adj₂ : H ⊣ I) : F ⋙ H ⊣ I ⋙ G :=
   counit := (functor.associator _ _ _).hom ≫
     (whisker_left I $ whisker_right adj₁.counit H) ≫ adj₂.counit }
 
+/-- If `F` and `G` are left adjoints then `F ⋙ G` is a left adjoint too. -/
+instance left_adjoint_of_comp {E : Type u₃} [ℰ : category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E)
+  [Fl : is_left_adjoint F] [Gl : is_left_adjoint G] : is_left_adjoint (F ⋙ G) :=
+{ right := Gl.right ⋙ Fl.right,
+  adj := comp _ _ Fl.adj Gl.adj }
+
+/-- If `F` and `G` are right adjoints then `F ⋙ G` is a right adjoint too. -/
+instance right_adjoint_of_comp {E : Type u₃} [ℰ : category.{v₃} E] {F : C ⥤ D} {G : D ⥤ E}
+  [Fr : is_right_adjoint F] [Gr : is_right_adjoint G] : is_right_adjoint (F ⋙ G) :=
+{ left := Gr.left ⋙ Fr.left,
+  adj := comp _ _ Gr.adj Fr.adj }
+
 end
 
 section construct_left
@@ -297,9 +368,22 @@ end equivalence
 
 namespace functor
 
+/-- An equivalence `E` is left adjoint to its inverse. -/
 def adjunction (E : C ⥤ D) [is_equivalence E] : E ⊣ E.inv :=
 (E.as_equivalence).to_adjunction
 
+/-- If `F` is an equivalence, it's a left adjoint. -/
+@[priority 10]
+instance left_adjoint_of_equivalence {F : C ⥤ D} [is_equivalence F] : is_left_adjoint F :=
+{ right := _,
+  adj := functor.adjunction F }
+
+/-- If `F` is an equivalence, it's a right adjoint. -/
+@[priority 10]
+instance right_adjoint_of_equivalence {F : C ⥤ D} [is_equivalence F] : is_right_adjoint F :=
+{ left := _,
+  adj := functor.adjunction F.inv }
+
 end functor
 
 end category_theory