From 289ebe58fe25ff99536bd6e7d9e07a9f5aaf7069 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Sat, 18 Dec 2021 20:11:20 +0000
Subject: [PATCH] =?UTF-8?q?chore(category=5Ftheory/monoidal/End):=20Adding?=
 =?UTF-8?q?=20API=20for=20monoidal=20functors=20into=20`C=20=E2=A5=A4=20C`?=
 =?UTF-8?q?=20(#10841)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Needed for the shift refactor
---
 src/category_theory/functor_category.lean    |   9 +
 src/category_theory/monoidal/End.lean        | 219 ++++++++++++++++++-
 src/category_theory/monoidal/functor.lean    |  20 +-
 src/category_theory/natural_isomorphism.lean |   3 +
 4 files changed, 243 insertions(+), 8 deletions(-)

diff --git a/src/category_theory/functor_category.lean b/src/category_theory/functor_category.lean
index 0a4c61e546824..baa5ded9706ee 100644
--- a/src/category_theory/functor_category.lean
+++ b/src/category_theory/functor_category.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
 import category_theory.natural_transformation
+import category_theory.isomorphism
 
 /-!
 # The category of functors and natural transformations between two fixed categories.
@@ -123,4 +124,12 @@ protected def flip (F : C ⥤ (D ⥤ E)) : D ⥤ (C ⥤ E) :=
 
 end functor
 
+@[simp, reassoc] lemma map_hom_inv_app (F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) :
+  (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 _ :=
+by simp [← nat_trans.comp_app, ← functor.map_comp]
+
+@[simp, reassoc] lemma map_inv_hom_app (F : C ⥤ D ⥤ E) {X Y : C} (e : X ≅ Y) (Z : D) :
+  (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 _ :=
+by simp [← nat_trans.comp_app, ← functor.map_comp]
+
 end category_theory
diff --git a/src/category_theory/monoidal/End.lean b/src/category_theory/monoidal/End.lean
index 41d33b7917c10..8eb24cc502613 100644
--- a/src/category_theory/monoidal/End.lean
+++ b/src/category_theory/monoidal/End.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Andrew Yang
 -/
 import category_theory.monoidal.functor
 
@@ -38,8 +38,6 @@ def endofunctor_monoidal_category : monoidal_category (C ⥤ C) :=
 
 open category_theory.monoidal_category
 
-variables [monoidal_category.{v} C]
-
 local attribute [instance] endofunctor_monoidal_category
 local attribute [reducible] endofunctor_monoidal_category
 
@@ -47,7 +45,7 @@ local attribute [reducible] endofunctor_monoidal_category
 Tensoring on the right gives a monoidal functor from `C` into endofunctors of `C`.
 -/
 @[simps]
-def tensoring_right_monoidal : monoidal_functor C (C ⥤ C) :=
+def tensoring_right_monoidal [monoidal_category.{v} C] : monoidal_functor C (C ⥤ C) :=
 { ε := (right_unitor_nat_iso C).inv,
   μ := λ X Y,
   { app := λ Z, (α_ Z X Y).hom,
@@ -70,4 +68,217 @@ def tensoring_right_monoidal : monoidal_functor C (C ⥤ C) :=
     by tidy⟩⟩,
   ..tensoring_right C }.
 
+variable {C}
+variables {M : Type*} [category M] [monoidal_category M] (F : monoidal_functor M (C ⥤ C))
+
+@[simp, reassoc]
+lemma μ_hom_inv_app (i j : M) (X : C) :
+  (F.μ i j).app X ≫ (F.μ_iso i j).inv.app X = 𝟙 _ := (F.μ_iso i j).hom_inv_id_app X
+
+@[simp, reassoc]
+lemma μ_inv_hom_app (i j : M) (X : C) :
+   (F.μ_iso i j).inv.app X ≫ (F.μ i j).app X = 𝟙 _ := (F.μ_iso i j).inv_hom_id_app X
+
+@[simp, reassoc]
+lemma ε_hom_inv_app (X : C) :
+  F.ε.app X ≫ F.ε_iso.inv.app X = 𝟙 _ := F.ε_iso.hom_inv_id_app X
+
+@[simp, reassoc]
+lemma ε_inv_hom_app (X : C) :
+  F.ε_iso.inv.app X ≫ F.ε.app X = 𝟙 _ := F.ε_iso.inv_hom_id_app X
+
+@[simp, reassoc]
+lemma ε_naturality {X Y : C} (f : X ⟶ Y) :
+  F.ε.app X ≫ (F.obj (𝟙_M)).map f = f ≫ F.ε.app Y := (F.ε.naturality f).symm
+
+@[simp, reassoc]
+lemma ε_inv_naturality {X Y : C} (f : X ⟶ Y) :
+  (F.obj (𝟙_M)).map f ≫ F.ε_iso.inv.app Y = F.ε_iso.inv.app X ≫ f :=
+F.ε_iso.inv.naturality f
+
+@[simp, reassoc]
+lemma μ_naturality {m n : M} {X Y : C} (f : X ⟶ Y) :
+  (F.obj n).map ((F.obj m).map f) ≫ (F.μ m n).app Y = (F.μ m n).app X ≫ (F.obj _).map f :=
+(F.to_lax_monoidal_functor.μ m n).naturality f
+
+-- This is a simp lemma in the reverse direction via `nat_trans.naturality`.
+@[reassoc]
+lemma μ_inv_naturality {m n : M} {X Y : C} (f : X ⟶ Y) :
+  (F.μ_iso m n).inv.app X ≫ (F.obj n).map ((F.obj m).map f) =
+    (F.obj _).map f ≫ (F.μ_iso m n).inv.app Y :=
+((F.μ_iso m n).inv.naturality f).symm
+
+-- This is not a simp lemma since it could be proved by the lemmas later.
+@[reassoc]
+lemma μ_naturality₂ {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) :
+  (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (F.μ m' n').app X =
+    (F.μ m n).app X ≫ (F.map (f ⊗ g)).app X :=
+begin
+  have := congr_app (F.to_lax_monoidal_functor.μ_natural f g) X,
+  dsimp at this,
+  simpa using this,
+end
+
+@[simp, reassoc]
+lemma μ_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) :
+  (F.obj n).map((F.map f).app X) ≫ (F.μ m' n).app X =
+    (F.μ m n).app X ≫ (F.map (f ⊗ 𝟙 n)).app X :=
+begin
+  rw ← μ_naturality₂ F f (𝟙 n) X,
+  simp,
+end
+
+@[simp, reassoc]
+lemma μ_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) :
+  (F.map g).app ((F.obj m).obj X) ≫ (F.μ m n').app X =
+    (F.μ m n).app X ≫ (F.map (𝟙 m ⊗ g)).app X :=
+begin
+  rw ← μ_naturality₂ F (𝟙 m) g X,
+  simp,
+end
+
+@[reassoc]
+lemma left_unitality_app (n : M) (X : C) :
+  (F.obj n).map (F.ε.app X) ≫ (F.μ (𝟙_M) n).app X
+    ≫ (F.map (λ_ n).hom).app X = 𝟙 _ :=
+begin
+  have := congr_app (F.to_lax_monoidal_functor.left_unitality n) X,
+  dsimp at this,
+  simpa using this.symm,
+end
+
+@[reassoc, simp]
+lemma obj_ε_app (n : M) (X : C) :
+  (F.obj n).map (F.ε.app X) =
+    (F.map (λ_ n).inv).app X ≫ (F.μ_iso (𝟙_M) n).inv.app X :=
+begin
+  refine eq.trans _ (category.id_comp _),
+  rw [← category.assoc, ← is_iso.comp_inv_eq, ← is_iso.comp_inv_eq, category.assoc],
+  convert left_unitality_app F n X,
+  { simp },
+  { ext, simpa }
+end
+
+@[reassoc, simp]
+lemma obj_ε_inv_app (n : M) (X : C) :
+  (F.obj n).map (F.ε_iso.inv.app X) =
+    (F.μ (𝟙_M) n).app X ≫ (F.map (λ_ n).hom).app X  :=
+begin
+  rw [← cancel_mono ((F.obj n).map (F.ε.app X)), ← functor.map_comp],
+  simpa,
+end
+
+@[reassoc]
+lemma right_unitality_app (n : M) (X : C) :
+  F.ε.app ((F.obj n).obj X) ≫ (F.μ n (𝟙_M)).app X ≫ (F.map (ρ_ n).hom).app X = 𝟙 _ :=
+begin
+  have := congr_app (F.to_lax_monoidal_functor.right_unitality n) X,
+  dsimp at this,
+  simpa using this.symm,
+end
+
+@[simp]
+lemma ε_app_obj (n : M) (X : C) :
+  F.ε.app ((F.obj n).obj X) =
+    (F.map (ρ_ n).inv).app X ≫ (F.μ_iso n (𝟙_M)).inv.app X :=
+begin
+  refine eq.trans _ (category.id_comp _),
+  rw [← category.assoc, ← is_iso.comp_inv_eq, ← is_iso.comp_inv_eq, category.assoc],
+  convert right_unitality_app F n X,
+  { simp },
+  { ext, simpa }
+end
+
+@[simp]
+lemma ε_inv_app_obj (n : M) (X : C) :
+  F.ε_iso.inv.app ((F.obj n).obj X) =
+    (F.μ n (𝟙_M)).app X ≫ (F.map (ρ_ n).hom).app X :=
+begin
+  rw [← cancel_mono (F.ε.app ((F.obj n).obj X)), ε_inv_hom_app],
+  simpa
+end
+
+@[reassoc]
+lemma associativity_app (m₁ m₂ m₃: M) (X : C) :
+  (F.obj m₃).map ((F.μ m₁ m₂).app X) ≫ (F.μ (m₁ ⊗ m₂) m₃).app X ≫
+    (F.map (α_ m₁ m₂ m₃).hom).app X =
+  (F.μ m₂ m₃).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (m₂ ⊗ m₃)).app X :=
+begin
+  have := congr_app (F.to_lax_monoidal_functor.associativity m₁ m₂ m₃) X,
+  dsimp at this,
+  simpa using this,
+end
+
+@[reassoc, simp]
+lemma obj_μ_app (m₁ m₂ m₃ : M) (X : C) :
+  (F.obj m₃).map ((F.μ m₁ m₂).app X) =
+  (F.μ m₂ m₃).app ((F.obj m₁).obj X) ≫ (F.μ m₁ (m₂ ⊗ m₃)).app X ≫
+    (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (F.μ_iso (m₁ ⊗ m₂) m₃).inv.app X :=
+begin
+  rw [← associativity_app_assoc],
+  dsimp,
+  simp,
+  dsimp,
+  simp,
+end
+
+@[reassoc, simp]
+lemma obj_μ_inv_app (m₁ m₂ m₃ : M) (X : C) :
+  (F.obj m₃).map ((F.μ_iso m₁ m₂).inv.app X) =
+  (F.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X ≫
+  (F.μ_iso m₁ (m₂ ⊗ m₃)).inv.app X ≫
+  (F.μ_iso m₂ m₃).inv.app ((F.obj m₁).obj X) :=
+begin
+  rw ← is_iso.inv_eq_inv,
+  convert obj_μ_app F m₁ m₂ m₃ X using 1,
+  { ext, rw ← functor.map_comp, simp },
+  { simp only [monoidal_functor.μ_iso_hom, category.assoc, nat_iso.inv_inv_app, is_iso.inv_comp],
+    congr,
+    { ext, simp },
+    { ext, simpa } }
+end
+
+@[simp, reassoc]
+lemma obj_zero_map_μ_app {m : M} {X Y : C} (f : X ⟶ (F.obj m).obj Y) :
+  (F.obj (𝟙_M)).map f ≫ (F.μ m (𝟙_M)).app _ =
+    F.ε_iso.inv.app _ ≫ f ≫ (F.map (ρ_ m).inv).app _ :=
+begin
+  rw [← is_iso.inv_comp_eq, ← is_iso.comp_inv_eq],
+  simp,
+end
+
+@[simp]
+lemma obj_μ_zero_app (m₁ m₂ : M) (X : C) :
+  (F.obj m₂).map ((F.μ m₁ (𝟙_M)).app X) =
+  (F.μ (𝟙_M) m₂).app ((F.obj m₁).obj X) ≫ (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫
+    (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X) :=
+begin
+  rw [← obj_ε_inv_app_assoc, ← functor.map_comp],
+  congr, simp,
+end
+
+/-- If `m ⊗ n ≅ 𝟙_M`, then `F.obj m` is a left inverse of `F.obj n`. -/
+@[simps] noncomputable
+def unit_of_tensor_iso_unit (m n : M) (h : m ⊗ n ≅ 𝟙_M) : F.obj m ⋙ F.obj n ≅ 𝟭 C :=
+F.μ_iso m n ≪≫ F.to_functor.map_iso h ≪≫ F.ε_iso.symm
+
+/-- If `m ⊗ n ≅ 𝟙_M` and `n ⊗ m ≅ 𝟙_M` (subject to some commuting constraints),
+  then `F.obj m` and `F.obj n` forms a self-equivalence of `C`. -/
+@[simps] noncomputable
+def equiv_of_tensor_iso_unit (m n : M) (h₁ : m ⊗ n ≅ 𝟙_M) (h₂ : n ⊗ m ≅ 𝟙_M)
+  (H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom) : C ≌ C :=
+{ functor := F.obj m,
+  inverse := F.obj n,
+  unit_iso := (unit_of_tensor_iso_unit F m n h₁).symm,
+  counit_iso := unit_of_tensor_iso_unit F n m h₂,
+  functor_unit_iso_comp' :=
+  begin
+    intro X,
+    dsimp,
+    simp only [μ_naturalityᵣ_assoc, μ_naturalityₗ_assoc, ε_inv_app_obj, category.assoc,
+      obj_μ_inv_app, functor.map_comp, μ_inv_hom_app_assoc, obj_ε_app,
+      unit_of_tensor_iso_unit_inv_app],
+    simp [← nat_trans.comp_app, ← F.to_functor.map_comp, ← H, - functor.map_comp]
+  end }
+
 end category_theory
diff --git a/src/category_theory/monoidal/functor.lean b/src/category_theory/monoidal/functor.lean
index 748ac9776ba92..9211029b454f9 100644
--- a/src/category_theory/monoidal/functor.lean
+++ b/src/category_theory/monoidal/functor.lean
@@ -179,12 +179,13 @@ namespace monoidal_functor
 section
 variables {C : Type u₁} [category.{v₁} C] [monoidal_category.{v₁} C]
 variables {D : Type u₂} [category.{v₂} D] [monoidal_category.{v₂} D]
+variable (F : monoidal_functor.{v₁ v₂} C D)
 
-lemma map_tensor (F : monoidal_functor.{v₁ v₂} C D) {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
+lemma map_tensor {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
   F.map (f ⊗ g) = inv (F.μ X X') ≫ ((F.map f) ⊗ (F.map g)) ≫ F.μ Y Y' :=
 by simp
 
-lemma map_left_unitor (F : monoidal_functor.{v₁ v₂} C D) (X : C) :
+lemma map_left_unitor (X : C) :
   F.map (λ_ X).hom = inv (F.μ (𝟙_ C) X) ≫ (inv F.ε ⊗ 𝟙 (F.obj X)) ≫ (λ_ (F.obj X)).hom :=
 begin
   simp only [lax_monoidal_functor.left_unitality],
@@ -192,7 +193,7 @@ begin
   simp,
 end
 
-lemma map_right_unitor (F : monoidal_functor.{v₁ v₂} C D) (X : C) :
+lemma map_right_unitor (X : C) :
   F.map (ρ_ X).hom = inv (F.μ X (𝟙_ C)) ≫ (𝟙 (F.obj X) ⊗ inv F.ε) ≫ (ρ_ (F.obj X)).hom :=
 begin
   simp only [lax_monoidal_functor.right_unitality],
@@ -202,11 +203,22 @@ end
 
 /-- The tensorator as a natural isomorphism. -/
 noncomputable
-def μ_nat_iso (F : monoidal_functor.{v₁ v₂} C D) :
+def μ_nat_iso :
   (functor.prod F.to_functor F.to_functor) ⋙ (tensor D) ≅ (tensor C) ⋙ F.to_functor :=
 nat_iso.of_components
   (by { intros, apply F.μ_iso })
   (by { intros, apply F.to_lax_monoidal_functor.μ_natural })
+
+@[simp] lemma μ_iso_hom (X Y : C) : (F.μ_iso X Y).hom = F.μ X Y := rfl
+@[simp, reassoc] lemma μ_inv_hom_id (X Y : C) : (F.μ_iso X Y).inv ≫ F.μ X Y = 𝟙 _ :=
+(F.μ_iso X Y).inv_hom_id
+@[simp] lemma μ_hom_inv_id (X Y : C) : F.μ X Y ≫ (F.μ_iso X Y).inv = 𝟙 _ :=
+(F.μ_iso X Y).hom_inv_id
+
+@[simp] lemma ε_iso_hom : F.ε_iso.hom = F.ε := rfl
+@[simp, reassoc] lemma ε_inv_hom_id : F.ε_iso.inv ≫ F.ε = 𝟙 _ := F.ε_iso.inv_hom_id
+@[simp] lemma ε_hom_inv_id : F.ε ≫ F.ε_iso.inv = 𝟙 _ := F.ε_iso.hom_inv_id
+
 end
 
 section
diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean
index 20414563146b5..83d3624bca609 100644
--- a/src/category_theory/natural_isomorphism.lean
+++ b/src/category_theory/natural_isomorphism.lean
@@ -123,6 +123,9 @@ by simp only [←category.assoc, cancel_mono]
   f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g' :=
 by simp only [←category.assoc, cancel_mono]
 
+@[simp] lemma inv_inv_app {F G : C ⥤ D} (e : F ≅ G) (X : C) :
+   inv (e.inv.app X) = e.hom.app X := by { ext, simp }
+
 end
 
 variables {X Y : C}