refactor(category_theory/monoidal): prove coherence lemmas by coherence (#13406)

kim-em · kim-em · commit b8b8bf3ea0c6 · 2022-04-24T04:20:58.000Z
Now that we have a basic monoidal coherence tactic, we can replace some boring proofs of particular coherence lemmas with `by coherence`.

I've also simply deleted a few lemmas which are not actually used elsewhere in mathlib, and can be proved `by coherence`.



Co-authored-by: Scott Morrison &lt;scott.morrison@gmail.com&gt;
diff --git a/src/category_theory/monoidal/Mon_.lean b/src/category_theory/monoidal/Mon_.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import category_theory.monoidal.braided
 import category_theory.monoidal.discrete
+import category_theory.monoidal.coherence_lemmas
 import category_theory.limits.shapes.terminal
 import algebra.punit_instances
 
diff --git a/src/category_theory/monoidal/braided.lean b/src/category_theory/monoidal/braided.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category_theory.monoidal.coherence
+import category_theory.monoidal.coherence_lemmas
 import category_theory.monoidal.natural_transformation
 import category_theory.monoidal.discrete
 
diff --git a/src/category_theory/monoidal/category.lean b/src/category_theory/monoidal/category.lean
@@ -160,22 +160,6 @@ by { ext, simp [←tensor_comp], }
 
 variables {U V W X Y Z : C}
 
--- When `rewrite_search` lands, add @[search] attributes to
-
--- monoidal_category.tensor_id monoidal_category.tensor_comp monoidal_category.associator_naturality
--- monoidal_category.left_unitor_naturality monoidal_category.right_unitor_naturality
--- monoidal_category.pentagon monoidal_category.triangle
-
--- tensor_comp_id tensor_id_comp comp_id_tensor_tensor_id
--- triangle_assoc_comp_left triangle_assoc_comp_right
--- triangle_assoc_comp_left_inv triangle_assoc_comp_right_inv
--- left_unitor_tensor left_unitor_tensor_inv
--- right_unitor_tensor right_unitor_tensor_inv
--- pentagon_inv
--- associator_inv_naturality
--- left_unitor_inv_naturality
--- right_unitor_inv_naturality
-
 lemma tensor_dite {P : Prop} [decidable P]
   {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)) :
   f ⊗ (if h : P then g h else g' h) = if h : P then f ⊗ g h else f ⊗ g' h :=
@@ -240,28 +224,15 @@ by { rw [←cancel_mono (λ_ Y).hom, left_unitor_naturality, left_unitor_natural
   (f ⊗ (𝟙 (𝟙_ C)) = g ⊗ (𝟙 (𝟙_ C))) ↔ (f = g) :=
 by { rw [←cancel_mono (ρ_ Y).hom, right_unitor_naturality, right_unitor_naturality], simp }
 
--- See Proposition 2.2.4 of <http://www-math.mit.edu/~etingof/egnobookfinal.pdf>
-@[reassoc]
-lemma left_unitor_tensor' (X Y : C) :
-  ((α_ (𝟙_ C) X Y).hom) ≫ ((λ_ (X ⊗ Y)).hom) = ((λ_ X).hom ⊗ (𝟙 Y)) :=
-by
-  rw [←tensor_left_iff, id_tensor_comp, ←cancel_epi (α_ (𝟙_ C) (𝟙_ C ⊗ X) Y).hom,
-    ←cancel_epi ((α_ (𝟙_ C) (𝟙_ C) X).hom ⊗ 𝟙 Y), pentagon_assoc, triangle, ←associator_naturality,
-    ←comp_tensor_id_assoc, triangle, associator_naturality, tensor_id]
-
-@[reassoc, simp]
-lemma left_unitor_tensor (X Y : C) :
-  ((λ_ (X ⊗ Y)).hom) = ((α_ (𝟙_ C) X Y).inv) ≫ ((λ_ X).hom ⊗ (𝟙 Y)) :=
-by { rw [←left_unitor_tensor'], simp }
-
-lemma left_unitor_tensor_inv' (X Y : C) :
-  ((λ_ (X ⊗ Y)).inv) ≫ ((α_ (𝟙_ C) X Y).inv) = ((λ_ X).inv ⊗ (𝟙 Y)) :=
-eq_of_inv_eq_inv (by simp)
+/-! The lemmas in the next section are true by coherence,
+but we prove them directly as they are used in proving the coherence theorem. -/
+section
 
-@[reassoc, simp]
-lemma left_unitor_tensor_inv (X Y : C) :
-  (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ (𝟙 Y)) ≫ (α_ (𝟙_ C) X Y).hom :=
-by { rw [←left_unitor_tensor_inv'], simp }
+@[reassoc]
+lemma pentagon_inv (W X Y Z : C) :
+  ((𝟙 W) ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ (𝟙 Z))
+    = (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv :=
+category_theory.eq_of_inv_eq_inv (by simp [pentagon])
 
 @[reassoc, simp]
 lemma right_unitor_tensor (X Y : C) :
@@ -276,13 +247,23 @@ lemma right_unitor_tensor_inv (X Y : C) :
   ((ρ_ (X ⊗ Y)).inv) = ((𝟙 X) ⊗ (ρ_ Y).inv) ≫ (α_ X Y (𝟙_ C)).inv :=
 eq_of_inv_eq_inv (by simp)
 
-@[reassoc]
-lemma id_tensor_right_unitor_inv (X Y : C) : 𝟙 X ⊗ (ρ_ Y).inv = (ρ_ _).inv ≫ (α_ _ _ _).hom :=
-by simp only [right_unitor_tensor_inv, category.comp_id, iso.inv_hom_id, category.assoc]
+lemma triangle_assoc_comp_left (X Y : C) :
+  (α_ X (𝟙_ C) Y).hom ≫ ((𝟙 X) ⊗ (λ_ Y).hom) = (ρ_ X).hom ⊗ 𝟙 Y :=
+monoidal_category.triangle X Y
 
-@[reassoc]
-lemma left_unitor_inv_tensor_id (X Y : C) : (λ_ X).inv ⊗ 𝟙 Y = (λ_ _).inv ≫ (α_ _ _ _).inv :=
-by simp only [left_unitor_tensor_inv, assoc, comp_id, hom_inv_id]
+@[simp, reassoc] lemma triangle_assoc_comp_right (X Y : C) :
+  (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ⊗ 𝟙 Y) = ((𝟙 X) ⊗ (λ_ Y).hom) :=
+by rw [←triangle_assoc_comp_left, iso.inv_hom_id_assoc]
+
+@[simp, reassoc] lemma triangle_assoc_comp_left_inv (X Y : C) :
+  ((𝟙 X) ⊗ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = ((ρ_ X).inv ⊗ 𝟙 Y) :=
+begin
+  apply (cancel_mono ((ρ_ X).hom ⊗ 𝟙 Y)).1,
+  simp only [triangle_assoc_comp_right, assoc],
+  rw [←id_tensor_comp, iso.inv_hom_id, ←comp_tensor_id, iso.inv_hom_id]
+end
+
+end
 
 @[reassoc]
 lemma associator_inv_naturality {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
@@ -309,53 +290,6 @@ lemma associator_inv_conjugation {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶
   (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) ≫ (α_ X' Y' Z').hom = f ⊗ g ⊗ h :=
 by rw [associator_naturality, inv_hom_id_assoc]
 
-@[reassoc]
-lemma pentagon_inv (W X Y Z : C) :
-  ((𝟙 W) ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ (𝟙 Z))
-    = (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv :=
-category_theory.eq_of_inv_eq_inv (by simp [pentagon])
-
-@[reassoc]
-lemma pentagon_inv_inv_hom (W X Y Z : C) :
-  (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ (𝟙 Z)) ≫ (α_ (W ⊗ X) Y Z).hom
-  = ((𝟙 W) ⊗ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv :=
-begin
-  rw ←((iso.eq_comp_inv _).mp (pentagon_inv W X Y Z)),
-  slice_rhs 1 2 { rw [←id_tensor_comp, iso.hom_inv_id] },
-  simp only [tensor_id, assoc, id_comp]
-end
-
-lemma triangle_assoc_comp_left (X Y : C) :
-  (α_ X (𝟙_ C) Y).hom ≫ ((𝟙 X) ⊗ (λ_ Y).hom) = (ρ_ X).hom ⊗ 𝟙 Y :=
-monoidal_category.triangle X Y
-
-@[simp, reassoc] lemma triangle_assoc_comp_right (X Y : C) :
-  (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ⊗ 𝟙 Y) = ((𝟙 X) ⊗ (λ_ Y).hom) :=
-by rw [←triangle_assoc_comp_left, iso.inv_hom_id_assoc]
-
-@[simp, reassoc] lemma triangle_assoc_comp_right_inv (X Y : C) :
-  ((ρ_ X).inv ⊗ 𝟙 Y) ≫ (α_ X (𝟙_ C) Y).hom = ((𝟙 X) ⊗ (λ_ Y).inv) :=
-begin
-  apply (cancel_mono (𝟙 X ⊗ (λ_ Y).hom)).1,
-  simp only [assoc, triangle_assoc_comp_left],
-  rw [←comp_tensor_id, iso.inv_hom_id, ←id_tensor_comp, iso.inv_hom_id]
-end
-
-@[simp, reassoc] lemma triangle_assoc_comp_left_inv (X Y : C) :
-  ((𝟙 X) ⊗ (λ_ Y).inv) ≫ (α_ X (𝟙_ C) Y).inv = ((ρ_ X).inv ⊗ 𝟙 Y) :=
-begin
-  apply (cancel_mono ((ρ_ X).hom ⊗ 𝟙 Y)).1,
-  simp only [triangle_assoc_comp_right, assoc],
-  rw [←id_tensor_comp, iso.inv_hom_id, ←comp_tensor_id, iso.inv_hom_id]
-end
-
-lemma unitors_equal : (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom :=
-by rw [←tensor_left_iff, ←cancel_epi (α_ (𝟙_ C) (𝟙_ _) (𝟙_ _)).hom, ←cancel_mono (ρ_ (𝟙_ C)).hom,
-       triangle, ←right_unitor_tensor, right_unitor_naturality]
-
-lemma unitors_inv_equal : (λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).inv :=
-by { ext, simp [←unitors_equal] }
-
 @[reassoc]
 lemma right_unitor_inv_comp_tensor (f : W ⟶ X) (g : 𝟙_ C ⟶ Z) :
   (ρ_ _).inv ≫ (f ⊗ g) = f ≫ (ρ_ _).inv ≫ (𝟙 _ ⊗ g) :=
@@ -386,34 +320,6 @@ lemma tensor_inv_hom_id {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z
   (g ⊗ f.inv) ≫ (h ⊗ f.hom) = (g ≫ h) ⊗ 𝟙 W :=
 by rw [←tensor_comp, f.inv_hom_id]
 
-@[reassoc]
-lemma pentagon_hom_inv {W X Y Z : C} :
-  (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv)
-  = (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom :=
-begin
-  have pent := pentagon W X Y Z,
-  rw ←iso.comp_inv_eq at pent,
-  rw [iso.eq_inv_comp, ←pent],
-  simp only [tensor_hom_inv_id, iso.inv_hom_id_assoc, tensor_id, category.comp_id, category.assoc],
-end
-
-@[reassoc]
-lemma pentagon_inv_hom (W X Y Z : C) :
-  (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z)
-  = (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv :=
-begin
-  have pent := pentagon W X Y Z,
-  rw ←iso.inv_comp_eq at pent,
-  rw [←pent],
-  simp only [tensor_id, assoc, id_comp, comp_id, hom_inv_id, tensor_hom_inv_id_assoc],
-end
-
-@[reassoc]
-lemma pentagon_comp_id_tensor {W X Y Z : C} :
-  (α_ W (X ⊗ Y) Z).hom ≫ ((𝟙 W) ⊗ (α_ X Y Z).hom)
-  = ((α_ W X Y).inv ⊗ (𝟙 Z)) ≫ (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom :=
-by { rw ←pentagon W X Y Z, simp }
-
 end
 
 section
diff --git a/src/category_theory/monoidal/coherence_lemmas.lean b/src/category_theory/monoidal/coherence_lemmas.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2018 Michael Jendrusch. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Jendrusch, Scott Morrison, Bhavik Mehta, Jakob von Raumer
+-/
+import category_theory.monoidal.coherence
+
+/-!
+# Lemmas which are consequences of monoidal coherence
+
+These lemmas are all proved `by coherence`.
+
+## Future work
+Investigate whether these lemmas are really needed,
+or if they can be replaced by use of the `coherence` tactic.
+-/
+
+open category_theory
+open category_theory.category
+open category_theory.iso
+
+namespace category_theory.monoidal_category
+
+variables {C : Type*} [category C] [monoidal_category C]
+
+-- See Proposition 2.2.4 of <http://www-math.mit.edu/~etingof/egnobookfinal.pdf>
+@[reassoc]
+lemma left_unitor_tensor' (X Y : C) :
+  ((α_ (𝟙_ C) X Y).hom) ≫ ((λ_ (X ⊗ Y)).hom) = ((λ_ X).hom ⊗ (𝟙 Y)) :=
+by coherence
+
+@[reassoc, simp]
+lemma left_unitor_tensor (X Y : C) :
+  ((λ_ (X ⊗ Y)).hom) = ((α_ (𝟙_ C) X Y).inv) ≫ ((λ_ X).hom ⊗ (𝟙 Y)) :=
+by coherence
+
+@[reassoc]
+lemma left_unitor_tensor_inv (X Y : C) :
+  (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ (𝟙 Y)) ≫ (α_ (𝟙_ C) X Y).hom :=
+by coherence
+
+@[reassoc]
+lemma id_tensor_right_unitor_inv (X Y : C) : 𝟙 X ⊗ (ρ_ Y).inv = (ρ_ _).inv ≫ (α_ _ _ _).hom :=
+by coherence
+
+@[reassoc]
+lemma left_unitor_inv_tensor_id (X Y : C) : (λ_ X).inv ⊗ 𝟙 Y = (λ_ _).inv ≫ (α_ _ _ _).inv :=
+by coherence
+
+@[reassoc]
+lemma pentagon_inv_inv_hom (W X Y Z : C) :
+  (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ (𝟙 Z)) ≫ (α_ (W ⊗ X) Y Z).hom
+  = ((𝟙 W) ⊗ (α_ X Y Z).hom) ≫ (α_ W X (Y ⊗ Z)).inv :=
+by coherence
+
+@[simp, reassoc] lemma triangle_assoc_comp_right_inv (X Y : C) :
+  ((ρ_ X).inv ⊗ 𝟙 Y) ≫ (α_ X (𝟙_ C) Y).hom = ((𝟙 X) ⊗ (λ_ Y).inv) :=
+by coherence
+
+lemma unitors_equal : (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom :=
+by coherence
+
+lemma unitors_inv_equal : (λ_ (𝟙_ C)).inv = (ρ_ (𝟙_ C)).inv :=
+by coherence
+
+@[reassoc]
+lemma pentagon_hom_inv {W X Y Z : C} :
+  (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv)
+  = (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) ≫ (α_ W (X ⊗ Y) Z).hom :=
+by coherence
+
+@[reassoc]
+lemma pentagon_inv_hom (W X Y Z : C) :
+  (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z)
+  = (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv :=
+by coherence
+
+end category_theory.monoidal_category
diff --git a/src/category_theory/monoidal/rigid.lean b/src/category_theory/monoidal/rigid.lean
@@ -3,9 +3,7 @@ Copyright (c) 2021 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jakob von Raumer
 -/
-
-import category_theory.monoidal.coherence
-
+import category_theory.monoidal.coherence_lemmas
 
 /-!
 # Rigid (autonomous) monoidal categories
