From d27a23a602240dedf3dffe70ec05cbea7059e8ea Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Sat, 14 Sep 2024 12:37:45 +0000 Subject: [PATCH] feat(CategoryTheory/Monoidal/Functor): add lemmas (#16778) --- Mathlib/CategoryTheory/Iso.lean | 2 +- Mathlib/CategoryTheory/Monoidal/Functor.lean | 16 ++++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean index 5294a89d8becb..bd24ff1c503c6 100644 --- 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 index a07f7efdd632b..019efca02f2f3 100644 --- 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