chore(CategoryTheory/Adjunction): deduplicate API for uniqueness of adjoints (#17113)

Removes some API from the file `Adjunction.Unique` which was a duplicate of API from `Adjunction.Mates`

Co-authored-by: @emilyriehl 



Co-authored-by: dagurtomas <dagurtomas@gmail.com>

Author: emilyriehl

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -14,7 +14,9 @@ import Mathlib.CategoryTheory.Yoneda
 
 We provide various useful constructors:
 * `mkOfHomEquiv`
-* `mkOfUnitCounit`
+* `mk'`: construct an adjunction from the data of a hom set equivalence, unit and counit natural
+  transformations together with proofs of the equalities `homEquiv_unit` and `homEquiv_counit`
+  relating them to each other.
 * `leftAdjointOfEquiv` / `rightAdjointOfEquiv`
   construct a left/right adjoint of a given functor given the action on objects and
   the relevant equivalence of morphism spaces.
@@ -30,6 +32,44 @@ adjoint can be obtained as `F.rightAdjoint`.
 `toEquivalence` upgrades an adjunction to an equivalence,
 given witnesses that the unit and counit are pointwise isomorphisms.
 Conversely `Equivalence.toAdjunction` recovers the underlying adjunction from an equivalence.
+
+## Overview of the directory `CategoryTheory.Adjunction`
+
+* Adjoint lifting theorems are in the directory `Lifting`.
+* The file `AdjointFunctorTheorems` proves the adjoint functor theorems.
+* The file `Comma` shows that for a functor `G : D ⥤ C` the data of an initial object in each
+  `StructuredArrow` category on `G` is equivalent to a left adjoint to `G`, as well as the dual.
+* The file `Evaluation` shows that products and coproducts are adjoint to evaluation of functors.
+* The file `FullyFaithful` characterizes when adjoints are full or faithful in terms of the unit
+  and counit.
+* The file `Limits` proves that left adjoints preserve colimits and right adjoints preserve limits.
+* The file `Mates` establishes the bijection between the 2-cells
+  ```
+          L₁                  R₁
+        C --→ D             C ←-- D
+      G ↓  ↗  ↓ H         G ↓  ↘  ↓ H
+        E --→ F             E ←-- F
+          L₂                  R₂
+  ```
+  where `L₁ ⊣ R₁` and `L₂ ⊣ R₂`. Specializing to a pair of adjoints `L₁ L₂ : C ⥤ D`,
+  `R₁ R₂ : D ⥤ C`, it provides equivalences `(L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂)` and `(L₂ ≅ L₁) ≃ (R₁ ≅ R₂)`.
+* The file `Opposites` contains constructions to relate adjunctions of functors to adjunctions of
+  their opposites.
+* The file `Reflective` defines reflective functors, i.e. fully faithful right adjoints. Note that
+  many facts about reflective functors are proved in the earlier file `FullyFaithful`.
+* The file `Restrict` defines the restriction of an adjunction along fully faithful functors.
+* The file `Triple` proves that in an adjoint triple, the left adjoint is fully faithful if and
+  only if the right adjoint is.
+* The file `Unique` proves uniqueness of adjoints.
+* The file `Whiskering` proves that functors `F : D ⥤ E` and `G : E ⥤ D` with an adjunction
+  `F ⊣ G`, induce adjunctions between the functor categories `C ⥤ D` and `C ⥤ E`,
+  and the functor categories `E ⥤ C` and `D ⥤ C`.
+
+## Other files related to adjunctions
+
+* The file `CategoryTheory.Monad.Adjunction` develops the basic relationship between adjunctions
+  and (co)monads. There it is also shown that given an adjunction `L ⊣ R` and an isomorphism
+  `L ⋙ R ≅ 𝟭 C`, the unit is an isomorphism, and similarly for the counit.
 -/
 
 
@@ -59,8 +99,6 @@ hom set equivalence.
 To construct adjoints to a given functor, there are constructors `leftAdjointOfEquiv` and
 `adjunctionOfEquivLeft` (as well as their duals).
 
-Uniqueness of adjoints is shown in `CategoryTheory.Adjunction.Unique`.
-
 See <https://stacks.math.columbia.edu/tag/0037>.
 -/
 structure Adjunction (F : C ⥤ D) (G : D ⥤ C) where

Mathlib/CategoryTheory/Adjunction/Mates.lean

@@ -13,11 +13,13 @@ import Mathlib.Tactic.ApplyFun
 
 This file establishes the bijection between the 2-cells
 
+```
          L₁                  R₁
       C --→ D             C ←-- D
     G ↓  ↗  ↓ H         G ↓  ↘  ↓ H
       E --→ F             E ←-- F
          L₂                  R₂
+```
 
 where `L₁ ⊣ R₁` and `L₂ ⊣ R₂`. The corresponding natural transformations are called mates.
 

Mathlib/CategoryTheory/Adjunction/Unique.lean

@@ -3,30 +3,21 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Thomas Read, Andrew Yang, Dagur Asgeirsson, Joël Riou
 -/
-import Mathlib.CategoryTheory.Adjunction.Basic
+import Mathlib.CategoryTheory.Adjunction.Mates
 /-!
 
 # Uniqueness of adjoints
 
 This file shows that adjoints are unique up to natural isomorphism.
 
 ## Main results
-* `Adjunction.natTransEquiv` and `Adjunction.natIsoEquiv` If `F ⊣ G` and `F' ⊣ G'` are adjunctions,
-  then there are equivalences `(G ⟶ G') ≃ (F' ⟶ F)` and `(G ≅ G') ≃ (F' ≅ F)`.
-Everything else is deduced from this:
 
 * `Adjunction.leftAdjointUniq` : If `F` and `F'` are both left adjoint to `G`, then they are
   naturally isomorphic.
 
 * `Adjunction.rightAdjointUniq` : If `G` and `G'` are both right adjoint to `F`, then they are
   naturally isomorphic.
 
-## TODO
-
-There some overlap with the file `Adjunction.Mates`. In particular, `natTransEquiv` is just a
-special case of `mateEquiv`. However, before removing `natTransEquiv`, in favour of `mateEquiv`,
-the latter needs some more API lemmas such as `natTransEquiv_apply_app`, `natTransEquiv_id`, etc.
-in order to make automation work better in the rest of this file.
 -/
 
 open CategoryTheory
@@ -35,89 +26,9 @@ variable {C D : Type*} [Category C] [Category D]
 
 namespace CategoryTheory.Adjunction
 
-/--
-If `F ⊣ G` and `F' ⊣ G'` are adjunctions, then giving a natural transformation `G ⟶ G'` is the
-same as giving a natural transformation `F' ⟶ F`.
--/
-@[simps]
-def natTransEquiv {F F' : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') :
-    (G ⟶ G') ≃ (F' ⟶ F) where
-  toFun f := {
-    app := fun X ↦ F'.map ((adj1.unit ≫ whiskerLeft F f).app X) ≫ adj2.counit.app _
-    naturality := by
-      intro X Y g
-      simp only [← Category.assoc, ← Functor.map_comp]
-      erw [(adj1.unit ≫ (whiskerLeft F f)).naturality]
-      simp
-  }
-  invFun f := {
-    app := fun X ↦ adj2.unit.app (G.obj X) ≫ G'.map (f.app (G.obj X) ≫ adj1.counit.app X)
-    naturality := by
-      intro X Y g
-      erw [← adj2.unit_naturality_assoc]
-      simp only [← Functor.map_comp]
-      simp
-  }
-  left_inv f := by
-    ext X
-    simp only [Functor.comp_obj, NatTrans.comp_app, Functor.id_obj, whiskerLeft_app,
-      Functor.map_comp, Category.assoc, unit_naturality_assoc, right_triangle_components_assoc]
-    erw [← f.naturality (adj1.counit.app X), ← Category.assoc]
-    simp
-  right_inv f := by
-    ext
-    simp
-
-@[simp]
-lemma natTransEquiv_id {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
-    natTransEquiv adj adj (𝟙 _) = 𝟙 _ := by ext; simp
-
-@[simp]
-lemma natTransEquiv_id_symm {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
-    (natTransEquiv adj adj).symm (𝟙 _) = 𝟙 _ := by ext; simp
-
-@[simp]
-lemma natTransEquiv_comp {F F' F'' : C ⥤ D} {G G' G'' : D ⥤ C}
-    (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (adj3 : F'' ⊣ G'') (f : G ⟶ G') (g : G' ⟶ G'') :
-    natTransEquiv adj2 adj3 g ≫ natTransEquiv adj1 adj2 f = natTransEquiv adj1 adj3 (f ≫ g) := by
-  apply (natTransEquiv adj1 adj3).symm.injective
-  ext X
-  simp only [natTransEquiv_symm_apply_app, Functor.comp_obj, NatTrans.comp_app,
-    natTransEquiv_apply_app, Functor.id_obj, whiskerLeft_app, Functor.map_comp, Category.assoc,
-    unit_naturality_assoc, right_triangle_components_assoc, Equiv.symm_apply_apply,
-    ← g.naturality_assoc, ← g.naturality]
-  simp only [← Category.assoc, unit_naturality, Functor.comp_obj, right_triangle_components,
-    Category.comp_id, ← f.naturality, Category.id_comp]
-
-@[simp]
-lemma natTransEquiv_comp_symm {F F' F'' : C ⥤ D} {G G' G'' : D ⥤ C}
-    (adj1 : F ⊣ G) (adj2 : F' ⊣ G') (adj3 : F'' ⊣ G'') (f : F' ⟶ F) (g : F'' ⟶ F') :
-    (natTransEquiv adj1 adj2).symm f ≫ (natTransEquiv adj2 adj3).symm g =
-      (natTransEquiv adj1 adj3).symm (g ≫ f) := by
-  apply (natTransEquiv adj1 adj3).injective
-  ext
-  simp
-
-/--
-If `F ⊣ G` and `F' ⊣ G'` are adjunctions, then giving a natural isomorphism `G ≅ G'` is the
-same as giving a natural transformation `F' ≅ F`.
--/
-@[simps]
-def natIsoEquiv {F F' : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G') :
-    (G ≅ G') ≃ (F' ≅ F) where
-  toFun i := {
-    hom := natTransEquiv adj1 adj2 i.hom
-    inv := natTransEquiv adj2 adj1 i.inv
-  }
-  invFun i := {
-    hom := (natTransEquiv adj1 adj2).symm i.hom
-    inv := (natTransEquiv adj2 adj1).symm i.inv }
-  left_inv i := by simp
-  right_inv i := by simp
-
 /-- If `F` and `F'` are both left adjoint to `G`, then they are naturally isomorphic. -/
 def leftAdjointUniq {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) : F ≅ F' :=
-  (natIsoEquiv adj1 adj2 (Iso.refl _)).symm
+  ((conjugateIsoEquiv adj1 adj2).symm (Iso.refl G)).symm
 
 -- Porting note (#10618): removed simp as simp can prove this
 theorem homEquiv_leftAdjointUniq_hom_app {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
@@ -141,9 +52,10 @@ theorem unit_leftAdjointUniq_hom_app
 theorem leftAdjointUniq_hom_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G) :
     whiskerLeft G (leftAdjointUniq adj1 adj2).hom ≫ adj2.counit = adj1.counit := by
   ext x
-  simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom, natIsoEquiv_apply_inv,
-    Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app, natTransEquiv_apply_app, whiskerLeft_id',
-    Category.comp_id, Category.assoc]
+  simp only [Functor.comp_obj, Functor.id_obj, leftAdjointUniq, Iso.symm_hom,
+    conjugateIsoEquiv_symm_apply_inv, Iso.refl_inv, NatTrans.comp_app, whiskerLeft_app,
+    conjugateEquiv_symm_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp,
+    Category.assoc]
   rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]
   simp
 
@@ -180,7 +92,7 @@ theorem leftAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
 
 /-- If `G` and `G'` are both right adjoint to `F`, then they are naturally isomorphic. -/
 def rightAdjointUniq {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') : G ≅ G' :=
-  (natIsoEquiv adj1 adj2).symm (Iso.refl _)
+  conjugateIsoEquiv adj1 adj2 (Iso.refl _)
 
 -- Porting note (#10618): simp can prove this
 theorem homEquiv_symm_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G)
@@ -192,8 +104,8 @@ theorem homEquiv_symm_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (a
 theorem unit_rightAdjointUniq_hom_app {F : C ⥤ D} {G G' : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F ⊣ G')
     (x : C) : adj1.unit.app x ≫ (rightAdjointUniq adj1 adj2).hom.app (F.obj x) =
       adj2.unit.app x := by
-  simp only [Functor.id_obj, Functor.comp_obj, rightAdjointUniq, natIsoEquiv_symm_apply_hom,
-    Iso.refl_hom, natTransEquiv_symm_apply_app, NatTrans.id_app, Category.id_comp]
+  simp only [Functor.id_obj, Functor.comp_obj, rightAdjointUniq, conjugateIsoEquiv_apply_hom,
+    Iso.refl_hom, conjugateEquiv_apply_app, NatTrans.id_app, Functor.map_id, Category.id_comp]
   rw [← adj2.unit_naturality_assoc, ← G'.map_comp]
   simp
 
@@ -243,4 +155,7 @@ theorem rightAdjointUniq_refl {F : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) :
 
 end Adjunction
 
+@[deprecated (since := "2024-10-07")] alias Adjunction.natTransEquiv := conjugateEquiv
+@[deprecated (since := "2024-10-07")] alias Adjunction.natIsoEquiv := conjugateIsoEquiv
+
 end CategoryTheory