[Merged by Bors] - feat (Category Theory): redefine and extend mates

Mathlib/CategoryTheory/Adjunction/Mates.lean

@@ -1,10 +1,15 @@
 /-
 Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Bhavik Mehta
+Authors: Bhavik Mehta, Emily Riehl
 -/
 import Mathlib.CategoryTheory.Adjunction.Basic
 import Mathlib.CategoryTheory.Conj
+import Mathlib.CategoryTheory.Category.Basic
+import Mathlib.CategoryTheory.Functor.Basic
+import Mathlib.CategoryTheory.Functor.Category
+import Mathlib.CategoryTheory.Whiskering
+
 
 #align_import category_theory.adjunction.mates from "leanprover-community/mathlib"@"cea27692b3fdeb328a2ddba6aabf181754543184"
 
@@ -19,15 +24,12 @@
       E --→ F             E ←-- F
          L₂                  R₂
 
-where `L₁ ⊣ R₁` and `L₂ ⊣ R₂`, and shows that in the special case where `G,H` are identity then the
-bijection preserves and reflects isomorphisms (i.e. we have bijections `(L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂)`, and
-if either side is an iso then the other side is as well).
+where `L₁ ⊣ R₁` and `L₂ ⊣ R₂`. The corresponding natural transformations are called mates.
 
-On its own, this bijection is not particularly useful but it includes a number of interesting cases
-as specializations.
+This bijection includes a number of interesting cases
+as specializations. For instance, in the special case where `G,H` are identity functors then the bijection preserves and reflects isomorphisms (i.e. we have bijections
+`(L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂)`, and if either side is an iso then the other side is as well). This demonstrates that adjoints to a given functor are unique up to isomorphism (since if `L₁ ≅ L₂` then we deduce `R₁ ≅ R₂`).
 
-For instance, this generalises the fact that adjunctions are unique (since if `L₁ ≅ L₂` then we
-deduce `R₁ ≅ R₂`).
 Another example arises from considering the square representing that a functor `H` preserves
 products, in particular the morphism `HA ⨯ H- ⟶ H(A ⨯ -)`. Then provided `(A ⨯ -)` and `HA ⨯ -` have
 left adjoints (for instance if the relevant categories are cartesian closed), the transferred
@@ -39,12 +41,11 @@
 mathlib: https://ncatlab.org/nlab/show/six+operations.
 -/
 
-
-universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
+universe v₁ v₂ v₃ v₄ v₅ v₆ v₇ v₈ v₉ u₁ u₂ u₃ u₄ u₅ u₆ u₇ u₈ u₉
 
 namespace CategoryTheory
 
-open Category
+open Category Functor Adjunction NatTrans
 
 variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D]
 
@@ -73,6 +74,8 @@
 
 Note that if one of the transformations is an iso, it does not imply the other is an iso.
 -/
+
+-- ER: The original definition of the mates equivalence.
 def transferNatTrans : (G ⋙ L₂ ⟶ L₁ ⋙ H) ≃ (R₁ ⋙ G ⟶ H ⋙ R₂) where
   toFun h :=
     { app := fun X => adj₂.unit.app _ ≫ R₂.map (h.app _ ≫ H.map (adj₁.counit.app _))
@@ -108,13 +111,58 @@
       h.naturality, -Functor.map_comp, ← Functor.map_comp_assoc G, R₂.map_comp]
 #align category_theory.transfer_nat_trans CategoryTheory.transferNatTrans
 
+-- ER: A new construction with a new name.
+def Mates :
+    (G ⋙ L₂ ⟶ L₁ ⋙ H) ≃ (R₁ ⋙ G ⟶ H ⋙ R₂) where
+      toFun := by
+        intro α
+        have R₁Gη₂ := whiskerLeft (R₁ ⋙ G) adj₂.unit
+        have R₁αR₂ := whiskerRight (whiskerLeft R₁ α) R₂
+        have ε₁HR₂ := whiskerRight adj₁.counit (H ⋙ R₂)
+        exact R₁Gη₂ ≫ R₁αR₂ ≫ ε₁HR₂
+      invFun := by
+        intro β
+        have η₁GL₂ := whiskerRight adj₁.unit (G ⋙ L₂)
+        have L₁βL₂ := whiskerRight (whiskerLeft L₁ β) L₂
+        have HR₂ε₂ := whiskerLeft (L₁ ⋙ H) adj₂.counit
+        exact η₁GL₂ ≫ L₁βL₂ ≫ HR₂ε₂
+      left_inv := by
+        intro α
+        ext
+        unfold whiskerRight whiskerLeft
+        simp only [comp_obj, id_obj, Functor.comp_map, comp_app, map_comp, assoc, counit_naturality,
+          counit_naturality_assoc, left_triangle_components_assoc]
+        rw [← assoc, ← Functor.comp_map, α.naturality, Functor.comp_map, assoc, ← H.map_comp, left_triangle_components, map_id]
+        simp only [comp_obj, comp_id]
+      right_inv := by
+        intro β
+        ext
+        unfold whiskerLeft whiskerRight
+        simp only [comp_obj, id_obj, Functor.comp_map, comp_app, map_comp, assoc,
+          unit_naturality_assoc, right_triangle_components_assoc]
+        rw [← assoc, ← Functor.comp_map, assoc, ← β.naturality, ← assoc, Functor.comp_map, ← G.map_comp, right_triangle_components, map_id, id_comp]
+
+-- ER: Note these definitions agree.
+theorem RightMateEqualsTransferNatTrans
+    (α : G ⋙ L₂ ⟶ L₁ ⋙ H) :
+    Mates adj₁ adj₂ α = (transferNatTrans adj₁ adj₂) α := by
+  ext; unfold Mates transferNatTrans; simp
+
+-- ER: Note these definitions agree.
+theorem LeftMateEqualsTransferNatTrans.symm
+    (α : R₁ ⋙ G ⟶ H ⋙ R₂) :
+    (Mates adj₁ adj₂).symm α = (transferNatTrans adj₁ adj₂).symm α := by
+  ext; unfold Mates transferNatTrans; simp
+
+-- ER: It's not clear to me what this theorem is for.
 theorem transferNatTrans_counit (f : G ⋙ L₂ ⟶ L₁ ⋙ H) (Y : D) :
     L₂.map ((transferNatTrans adj₁ adj₂ f).app _) ≫ adj₂.counit.app _ =
       f.app _ ≫ H.map (adj₁.counit.app Y) := by
   erw [Functor.map_comp]
   simp
 #align category_theory.transfer_nat_trans_counit CategoryTheory.transferNatTrans_counit
 
+-- ER: It's not clear to me what this theorem is for.
 theorem unit_transferNatTrans (f : G ⋙ L₂ ⟶ L₁ ⋙ H) (X : C) :
     G.map (adj₁.unit.app X) ≫ (transferNatTrans adj₁ adj₂ f).app _ =
       adj₂.unit.app _ ≫ R₂.map (f.app _) := by
@@ -127,6 +175,240 @@
 -- See library note [dsimp, simp]
 end Square
 
+-- ER: A new section proving that the mates bijection commutes with vertical composition of squares.
+section MatesVComp
+
+variable {A : Type u₁} {B : Type u₂} {C : Type u₃}
+variable {D : Type u₄} {E : Type u₅} {F : Type u₆}
+variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C]
+variable [Category.{v₄} D] [Category.{v₅} E][Category.{v₆} F]
+variable {G₁ : A ⥤ C}{G₂ : C ⥤ E}{H₁ : B ⥤ D}{H₂ : D ⥤ F}
+variable {L₁ : A ⥤ B}{R₁ : B ⥤ A} {L₂ : C ⥤ D}{R₂ : D ⥤ C}
+variable {L₃ : E ⥤ F}{R₃ : F ⥤ E}
+variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃)
+
+def LeftAdjointSquare.vcomp :
+    (G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁) → (G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂) →
+    ((G₁ ⋙ G₂) ⋙ L₃ ⟶ L₁ ⋙ (H₁ ⋙ H₂)) := fun α β ↦
+  (whiskerLeft G₁ β) ≫ (whiskerRight α H₂)
+
+def RightAdjointSquare.vcomp :
+    (R₁ ⋙ G₁ ⟶ H₁ ⋙ R₂) → (R₂ ⋙ G₂ ⟶ H₂ ⋙ R₃) →
+    (R₁ ⋙ (G₁ ⋙ G₂) ⟶ (H₁ ⋙ H₂) ⋙ R₃) := fun α β ↦
+  (whiskerRight α G₂) ≫ (whiskerLeft H₁ β)
+
+theorem Mates_vcomp
+  (α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁)
+  (β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂) :
+  (Mates (G := G₁ ⋙ G₂) (H := H₁ ⋙ H₂) adj₁ adj₃) (LeftAdjointSquare.vcomp α β)
+    =
+  RightAdjointSquare.vcomp
+  ( (Mates (G := G₁) (H := H₁) adj₁ adj₂) α)
+  ( (Mates (G := G₂) (H := H₂) adj₂ adj₃) β)
+     := by
+  unfold LeftAdjointSquare.vcomp RightAdjointSquare.vcomp Mates
+  ext b
+  simp
+  slice_rhs 1 4 =>
+    {
+      rw [← assoc, ← assoc]
+      rw [← unit_naturality (adj₃)]
+    }
+  rw [L₃.map_comp, R₃.map_comp]
+  slice_rhs 3 4  =>
+    { rw [← Functor.comp_map G₂ L₃, ← R₃.map_comp]
+      rw [β.naturality]
+    }
+  rw [L₃.map_comp, R₃.map_comp]
+  slice_rhs 3 4 =>
+    { rw [← R₃.map_comp, ← Functor.comp_map G₂ L₃, ← assoc]
+      rw [β.naturality]
+    }
+  rw [R₃.map_comp, R₃.map_comp]
+  slice_rhs 2 3 =>
+    {
+      rw [← R₃.map_comp, ← Functor.comp_map G₂ L₃]
+      rw [β.naturality]
+    }
+  slice_rhs 4 5 =>
+    {
+      rw [← R₃.map_comp, Functor.comp_map L₂ _, ← Functor.comp_map _ L₂, ← H₂.map_comp]
+      rw [adj₂.counit.naturality]
+    }
+  simp
+  slice_rhs 4 5 =>
+    {
+      rw [← R₃.map_comp, ← H₂.map_comp, ← Functor.comp_map _ L₂]
+      rw [adj₂.counit.naturality]
+    }
+  simp
+  slice_rhs 3 4 =>
+    {
+      rw [← R₃.map_comp, ← H₂.map_comp]
+      rw [left_triangle_components]
+    }
+  simp only [map_id, id_comp]
+
+end MatesVComp
+
+-- ER: A new section proving that the mates bijection commutes with horizontal composition of squares.
+section MatesHComp
+
+variable {A : Type u₁} {B : Type u₂} {C : Type u₃}
+variable {D : Type u₄} {E : Type u₅} {F : Type u₆}
+variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C]
+variable [Category.{v₄} D] [Category.{v₅} E][Category.{v₆} F]
+variable {G : A ⥤ D}{H : B ⥤ E}{K : C ⥤ F}
+variable {L₁ : A ⥤ B}{R₁ : B ⥤ A} {L₂ : D ⥤ E}{R₂ : E ⥤ D}
+variable {L₃ : B ⥤ C}{R₃ : C ⥤ B} {L₄ : E ⥤ F}{R₄ : F ⥤ E}
+variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
+variable (adj₃ : L₃ ⊣ R₃) (adj₄ : L₄ ⊣ R₄)
+
+def LeftAdjointSquare.hcomp :
+    (G ⋙ L₂ ⟶ L₁ ⋙ H) → (H ⋙ L₄ ⟶ L₃ ⋙ K) →
+    (G ⋙ (L₂ ⋙ L₄) ⟶ (L₁ ⋙ L₃) ⋙ K) := fun α β ↦
+  (whiskerRight α L₄) ≫ (whiskerLeft L₁ β)
+
+def RightAdjointSquare.hcomp :
+    (R₁ ⋙ G ⟶ H ⋙ R₂) → (R₃ ⋙ H ⟶ K ⋙ R₄) →
+    ((R₃ ⋙ R₁) ⋙ G ⟶ K ⋙ (R₄ ⋙ R₂)) := fun α β ↦
+  (whiskerLeft R₃ α) ≫ (whiskerRight β R₂)
+
+theorem Mates_hcomp
+    (α : G ⋙ L₂ ⟶ L₁ ⋙ H)
+    (β : H ⋙ L₄ ⟶ L₃ ⋙ K) :
+    (Mates (G := G) (H := K)
+      (adj₁.comp adj₃) (adj₂.comp adj₄)) (LeftAdjointSquare.hcomp α β) =
+    RightAdjointSquare.hcomp
+      ((Mates adj₁ adj₂) α)
+      ((Mates adj₃ adj₄) β) := by
+  unfold LeftAdjointSquare.hcomp RightAdjointSquare.hcomp Mates Adjunction.comp
+  ext c
+  simp
+  slice_rhs 3 4 =>
+    {
+      rw [← R₂.map_comp]
+      rw [← unit_naturality (adj₄)]
+    }
+  slice_rhs 2 3 =>
+    {
+      rw [← R₂.map_comp, ← assoc]
+      rw [← unit_naturality (adj₄)]
+    }
+  rw [R₂.map_comp, R₂.map_comp]
+  slice_rhs 4 5 =>
+    {
+      rw [← R₂.map_comp, ← R₄.map_comp, ← Functor.comp_map _ L₄]
+      rw [β.naturality]
+    }
+  simp only [comp_obj, Functor.comp_map, map_comp, assoc]
+
+end MatesHComp
+
+-- ER: Combining the previous sections, we can compose squares of squares and again this commutes with the mates bijection. These results form the basis for an isomorphism of double categories to be proven later.
+section MatesSquareComp
+
+variable {A : Type u₁} {B : Type u₂} {C : Type u₃}
+variable {D : Type u₄} {E : Type u₅} {F : Type u₆}
+variable {X : Type u₇} {Y : Type u₈} {Z : Type u₉}
+variable [Category.{v₁} A] [Category.{v₂} B][Category.{v₃} C]
+variable [Category.{v₄} D] [Category.{v₅} E][Category.{v₆} F]
+variable [Category.{v₇} X] [Category.{v₈} Y][Category.{v₉} Z]
+variable {G₁ : A ⥤ D} {H₁ : B ⥤ E} {K₁ : C ⥤ F}
+variable {G₂ : D ⥤ X} {H₂ : E ⥤ Y} {K₂ : F ⥤ Z}
+variable {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : B ⥤ C}{R₂ : C ⥤ B}
+variable {L₃ : D ⥤ E} {R₃ : E ⥤ D} {L₄ : E ⥤ F}{R₄ : F ⥤ E}
+variable {L₅ : X ⥤ Y} {R₅ : Y ⥤ X} {L₆ : Y ⥤ Z}{R₆ : Z ⥤ Y}
+variable (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
+variable (adj₃ : L₃ ⊣ R₃) (adj₄ : L₄ ⊣ R₄)
+variable (adj₅ : L₅ ⊣ R₅) (adj₆ : L₆ ⊣ R₆)
+
+def LeftAdjointSquare.comp
+    (α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁) (β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁)
+    (γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂) (δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂) :
+    ((G₁ ⋙ G₂) ⋙ (L₅ ⋙ L₆)) ⟶ ((L₁ ⋙ L₂) ⋙ (K₁ ⋙ K₂))
+  := LeftAdjointSquare.vcomp
+      ( LeftAdjointSquare.hcomp α β)
+      ( LeftAdjointSquare.hcomp γ δ)
+
+theorem LeftAdjointSquare.comp_vhcomp
+    (α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁) (β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁)
+    (γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂) (δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂) :
+    LeftAdjointSquare.comp α β γ δ =
+    LeftAdjointSquare.vcomp
+      ( LeftAdjointSquare.hcomp α β)
+      ( LeftAdjointSquare.hcomp γ δ) := rfl
+
+theorem LeftAdjointSquare.comp_hvcomp
+    (α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁) (β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁)
+    (γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂) (δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂) :
+    LeftAdjointSquare.comp α β γ δ =
+    LeftAdjointSquare.hcomp
+    ( LeftAdjointSquare.vcomp α γ)
+    ( LeftAdjointSquare.vcomp β δ) := by
+  unfold LeftAdjointSquare.comp
+  unfold LeftAdjointSquare.hcomp LeftAdjointSquare.vcomp
+  unfold whiskerLeft whiskerRight
+  ext a
+  simp only [comp_obj, comp_app, map_comp, assoc]
+  slice_rhs 2 3 =>
+    {
+      rw [← Functor.comp_map _ L₆]
+      rw [δ.naturality]
+    }
+  simp only [comp_obj, Functor.comp_map, assoc]
+
+def RightAdjointSquare.comp
+    (α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃) (β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄)
+    (γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅) (δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆) :
+    ((R₂ ⋙ R₁) ⋙ (G₁ ⋙ G₂) ⟶ (K₁ ⋙ K₂) ⋙ (R₆ ⋙ R₅))
+  := RightAdjointSquare.vcomp
+    ( RightAdjointSquare.hcomp α β)
+    ( RightAdjointSquare.hcomp γ δ)
+
+theorem RightAdjointSquare.comp_vhcomp
+    (α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃) (β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄)
+    (γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅) (δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆) :
+    RightAdjointSquare.comp α β γ δ =
+    RightAdjointSquare.vcomp
+    ( RightAdjointSquare.hcomp α β)
+    ( RightAdjointSquare.hcomp γ δ) := rfl
+
+theorem RightAdjointSquare.comp_hvcomp
+    (α : R₁ ⋙ G₁ ⟶ H₁ ⋙ R₃) (β : R₂ ⋙ H₁ ⟶ K₁ ⋙ R₄)
+    (γ : R₃ ⋙ G₂ ⟶ H₂ ⋙ R₅) (δ : R₄ ⋙ H₂ ⟶ K₂ ⋙ R₆) :
+    RightAdjointSquare.comp α β γ δ =
+    RightAdjointSquare.hcomp
+    ( RightAdjointSquare.vcomp α γ)
+    ( RightAdjointSquare.vcomp β δ) := by
+  unfold RightAdjointSquare.comp
+  unfold RightAdjointSquare.hcomp RightAdjointSquare.vcomp
+  unfold whiskerLeft whiskerRight
+  ext c
+  simp only [comp_obj, comp_app, map_comp, assoc]
+  slice_rhs 2 3 =>
+    {
+      rw [← Functor.comp_map _ R₅]
+      rw [← γ.naturality]
+    }
+  simp only [comp_obj, Functor.comp_map, assoc]
+
+theorem Mates_square
+    (α : G₁ ⋙ L₃ ⟶ L₁ ⋙ H₁) (β : H₁ ⋙ L₄ ⟶ L₂ ⋙ K₁)
+    (γ : G₂ ⋙ L₅ ⟶ L₃ ⋙ H₂) (δ : H₂ ⋙ L₆ ⟶ L₄ ⋙ K₂) :
+    (Mates (G := G₁ ⋙ G₂) (H := K₁ ⋙ K₂)
+      (adj₁.comp adj₂) (adj₅.comp adj₆)) (LeftAdjointSquare.comp α β γ δ) =
+    RightAdjointSquare.comp
+      ((Mates adj₁ adj₃) α) ((Mates adj₂ adj₄) β)
+      ((Mates adj₃ adj₅) γ) ((Mates adj₄ adj₆) δ) := by
+  have vcomp := Mates_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆) (LeftAdjointSquare.hcomp α β) (LeftAdjointSquare.hcomp γ δ)
+  have hcomp1 := Mates_hcomp adj₁ adj₃ adj₂ adj₄ α β
+  have hcomp2 := Mates_hcomp adj₃ adj₅ adj₄ adj₆ γ δ
+  rw [hcomp1, hcomp2] at vcomp
+  exact vcomp
+
+end MatesSquareComp
+
 section Self
 
 variable {L₁ L₂ L₃ : C ⥤ D} {R₁ R₂ R₃ : D ⥤ C}