feat(CategoryTheory/Monoidal/Functor): add lemmas (#16778)

leanprover-community · Sep 14, 2024 · d27a23a · d27a23a
1 parent d3dbb49
commit d27a23a
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 1 deletion.
diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean
@@ -355,7 +355,7 @@ theorem inv_id : inv (𝟙 X) = 𝟙 X := by
   apply inv_eq_of_hom_inv_id
   simp
 
-@[simp]
+@[simp, reassoc]
 theorem inv_comp [IsIso f] [IsIso h] : inv (f ≫ h) = inv h ≫ inv f := by
   apply inv_eq_of_hom_inv_id
   simp

diff --git a/Mathlib/CategoryTheory/Monoidal/Functor.lean b/Mathlib/CategoryTheory/Monoidal/Functor.lean
@@ -365,6 +365,22 @@ theorem map_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) :
 theorem map_whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) :
     F.map (f ▷ Z) = inv (F.μ X Z) ≫ F.map f ▷ F.obj Z ≫ F.μ Y Z := by simp
 
+@[reassoc]
+theorem map_associator (X Y Z : C) :
+    F.map (α_ X Y Z).hom =
+      inv (F.μ (X ⊗ Y) Z) ≫ inv (F.μ X Y) ▷ F.obj Z ≫
+        (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ F.μ Y Z ≫ F.μ X (Y ⊗ Z) := by
+  rw [← inv_whiskerRight, ← IsIso.inv_comp_assoc, IsIso.eq_inv_comp]
+  simp
+
+@[reassoc]
+theorem map_associator_inv (X Y Z : C) :
+    F.map (α_ X Y Z).inv =
+      inv (F.μ X (Y ⊗ Z)) ≫ F.obj X ◁ inv (F.μ Y Z) ≫
+        (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ F.μ X Y ▷ F.obj Z ≫ F.μ (X ⊗ Y) Z := by
+  rw [← inv_whiskerLeft, ← IsIso.inv_comp_assoc, IsIso.eq_inv_comp]
+  simp
+
 @[reassoc]
 theorem map_leftUnitor (X : C) :
     F.map (λ_ X).hom = inv (F.μ (𝟙_ C) X) ≫ inv F.ε ▷ F.obj X ≫ (λ_ (F.obj X)).hom := by