chore(category_theory/monoidal): golf some proofs (#6894)

Golfs proofs of `tensor_left_iff`, `tensor_right_iff`, `left_unitor_tensor'`, `right_unitor_tensor` and `unitors_equal` - in particular removes the file `monoidal/unitors` as all it contained was a proof of `unitors_equal` which is a two line proof.

Author: b-mehta

src/category_theory/monoidal/Mon_.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.monoidal.discrete
-import category_theory.monoidal.unitors
 import category_theory.limits.shapes.terminal
 import algebra.punit_instances
 

src/category_theory/monoidal/category.lean

@@ -1,7 +1,7 @@
 /-
 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
+Authors: Michael Jendrusch, Scott Morrison, Bhavik Mehta
 -/
 import category_theory.products.basic
 
@@ -119,6 +119,7 @@ restate_axiom monoidal_category.right_unitor_naturality'
 attribute [reassoc] monoidal_category.right_unitor_naturality
 restate_axiom monoidal_category.pentagon'
 restate_axiom monoidal_category.triangle'
+attribute [reassoc] monoidal_category.pentagon
 attribute [simp, reassoc] monoidal_category.triangle
 
 open monoidal_category
@@ -175,11 +176,11 @@ variables {U V W X Y Z : C}
 -- left_unitor_inv_naturality
 -- right_unitor_inv_naturality
 
-@[simp] lemma comp_tensor_id (f : W ⟶ X) (g : X ⟶ Y) :
+@[reassoc, simp] lemma comp_tensor_id (f : W ⟶ X) (g : X ⟶ Y) :
   (f ≫ g) ⊗ (𝟙 Z) = (f ⊗ (𝟙 Z)) ≫ (g ⊗ (𝟙 Z)) :=
 by { rw ←tensor_comp, simp }
 
-@[simp] lemma id_tensor_comp (f : W ⟶ X) (g : X ⟶ Y) :
+@[reassoc, simp] lemma id_tensor_comp (f : W ⟶ X) (g : X ⟶ Y) :
   (𝟙 Z) ⊗ (f ≫ g) = (𝟙 Z ⊗ f) ≫ (𝟙 Z ⊗ g) :=
 by { rw ←tensor_comp, simp }
 
@@ -220,123 +221,20 @@ by rw [left_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_co
 @[simp] lemma tensor_left_iff
   {X Y : C} (f g : X ⟶ Y) :
   ((𝟙 (𝟙_ C)) ⊗ f = (𝟙 (𝟙_ C)) ⊗ g) ↔ (f = g) :=
-begin
-  split,
-  { intro h,
-    have h' := congr_arg (λ k, (λ_ _).inv ≫ k) h,
-    dsimp at h',
-    rw [←left_unitor_inv_naturality, ←left_unitor_inv_naturality] at h',
-    exact (cancel_mono _).1 h', },
-  { intro h, subst h, }
-end
+by { rw [←cancel_mono (λ_ Y).hom, left_unitor_naturality, left_unitor_naturality], simp }
 
 @[simp] lemma tensor_right_iff
   {X Y : C} (f g : X ⟶ Y) :
   (f ⊗ (𝟙 (𝟙_ C)) = g ⊗ (𝟙 (𝟙_ C))) ↔ (f = g) :=
-begin
-  split,
-  { intro h,
-    have h' := congr_arg (λ k, (ρ_ _).inv ≫ k) h,
-    dsimp at h',
-    rw [←right_unitor_inv_naturality, ←right_unitor_inv_naturality] at h',
-    exact (cancel_mono _).1 h' },
-  { intro h, subst h, }
-end
-
--- We now prove:
---   ((α_ (𝟙_ C) X Y).hom) ≫
---     ((λ_ (X ⊗ Y)).hom)
---   = ((λ_ X).hom ⊗ (𝟙 Y))
--- (and the corresponding fact for right unitors)
--- following the proof on nLab:
--- Lemma 2.2 at <https://ncatlab.org/nlab/revision/monoidal+category/115>
-
-lemma left_unitor_product_aux_perimeter (X Y : C) :
-    ((α_ (𝟙_ C) (𝟙_ C) X).hom ⊗ (𝟙 Y)) ≫
-    (α_ (𝟙_ C) ((𝟙_ C) ⊗ X) Y).hom ≫
-    ((𝟙 (𝟙_ C)) ⊗ (α_ (𝟙_ C) X Y).hom) ≫
-    ((𝟙 (𝟙_ C)) ⊗ (λ_ (X ⊗ Y)).hom)
-  = (((ρ_ (𝟙_ C)).hom ⊗ (𝟙 X)) ⊗ (𝟙 Y)) ≫
-    (α_ (𝟙_ C) X Y).hom :=
-begin
-  conv_lhs { congr, skip, rw [←category.assoc] },
-  rw [←category.assoc, monoidal_category.pentagon, associator_naturality, tensor_id,
-      ←monoidal_category.triangle, ←category.assoc]
-end
-
-lemma left_unitor_product_aux_triangle (X Y : C) :
-    ((α_ (𝟙_ C) (𝟙_ C) X).hom ⊗ (𝟙 Y)) ≫
-    (((𝟙 (𝟙_ C)) ⊗ (λ_ X).hom) ⊗ (𝟙 Y))
-  = ((ρ_ (𝟙_ C)).hom ⊗ (𝟙 X)) ⊗ (𝟙 Y) :=
-by rw [←comp_tensor_id, ←monoidal_category.triangle]
-
-lemma left_unitor_product_aux_square (X Y : C) :
-    (α_ (𝟙_ C) ((𝟙_ C) ⊗ X) Y).hom ≫
-    ((𝟙 (𝟙_ C)) ⊗ (λ_ X).hom ⊗ (𝟙 Y))
-  = (((𝟙 (𝟙_ C)) ⊗ (λ_ X).hom) ⊗ (𝟙 Y)) ≫
-    (α_ (𝟙_ C) X Y).hom :=
-by rw associator_naturality
-
-lemma left_unitor_product_aux (X Y : C) :
-    ((𝟙 (𝟙_ C)) ⊗ (α_ (𝟙_ C) X Y).hom) ≫
-    ((𝟙 (𝟙_ C)) ⊗ (λ_ (X ⊗ Y)).hom)
-  = (𝟙 (𝟙_ C)) ⊗ ((λ_ X).hom ⊗ (𝟙 Y)) :=
-begin
-  rw ←(cancel_epi (α_ (𝟙_ C) ((𝟙_ C) ⊗ X) Y).hom),
-  rw left_unitor_product_aux_square,
-  rw ←(cancel_epi ((α_ (𝟙_ C) (𝟙_ C) X).hom ⊗ (𝟙 Y))),
-  slice_rhs 1 2 { rw left_unitor_product_aux_triangle },
-  conv_lhs { rw [left_unitor_product_aux_perimeter] }
-end
-
-lemma right_unitor_product_aux_perimeter (X Y : C) :
-    ((α_ X Y (𝟙_ C)).hom ⊗ (𝟙 (𝟙_ C))) ≫
-    (α_ X (Y ⊗ (𝟙_ C)) (𝟙_ C)).hom ≫
-    ((𝟙 X) ⊗ (α_ Y (𝟙_ C) (𝟙_ C)).hom) ≫
-    ((𝟙 X) ⊗ (𝟙 Y) ⊗ (λ_ (𝟙_ C)).hom)
-  = ((ρ_ (X ⊗ Y)).hom ⊗ (𝟙 (𝟙_ C))) ≫
-    (α_ X Y (𝟙_ C)).hom :=
-begin
-  transitivity (((α_ X Y _).hom ⊗ 𝟙 _) ≫ (α_ X _ _).hom ≫
-    (𝟙 X ⊗ (α_ Y _ _).hom)) ≫
-    (𝟙 X ⊗ 𝟙 Y ⊗ (λ_ _).hom),
-  { conv_lhs { congr, skip, rw [←category.assoc] },
-    conv_rhs { rw [category.assoc] } },
-  { conv_lhs { congr, rw [monoidal_category.pentagon] },
-    conv_rhs { congr, rw [←monoidal_category.triangle] },
-    conv_rhs { rw [category.assoc] },
-    conv_rhs { congr, skip, congr, congr, rw [←tensor_id] },
-    conv_rhs { congr, skip, rw [associator_naturality] },
-    conv_rhs { rw [←category.assoc] } }
-end
-
-lemma right_unitor_product_aux_triangle (X Y : C) :
-    ((𝟙 X) ⊗ (α_ Y (𝟙_ C) (𝟙_ C)).hom) ≫
-    ((𝟙 X) ⊗ (𝟙 Y) ⊗ (λ_ (𝟙_ C)).hom)
-  = (𝟙 X) ⊗ (ρ_ Y).hom ⊗ (𝟙 (𝟙_ C)) :=
-by rw [←id_tensor_comp, ←monoidal_category.triangle]
-
-lemma right_unitor_product_aux_square (X Y : C) :
-    (α_ X (Y ⊗ (𝟙_ C)) (𝟙_ C)).hom ≫
-    ((𝟙 X) ⊗ (ρ_ Y).hom ⊗ (𝟙 (𝟙_ C)))
-  = (((𝟙 X) ⊗ (ρ_ Y).hom) ⊗ (𝟙 (𝟙_ C))) ≫
-    (α_ X Y (𝟙_ C)).hom :=
-by rw [associator_naturality]
-
-lemma right_unitor_product_aux (X Y : C) :
-    ((α_ X Y (𝟙_ C)).hom ⊗ (𝟙 (𝟙_ C))) ≫
-    (((𝟙 X) ⊗ (ρ_ Y).hom) ⊗ (𝟙 (𝟙_ C)))
-  = ((ρ_ (X ⊗ Y)).hom ⊗ (𝟙 (𝟙_ C))) :=
-begin
-  rw ←(cancel_mono (α_ X Y (𝟙_ C)).hom),
-  slice_lhs 2 3 { rw ←right_unitor_product_aux_square },
-  rw [←right_unitor_product_aux_triangle, ←right_unitor_product_aux_perimeter],
-end
+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>
 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, left_unitor_product_aux]
+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]
 
 @[simp]
 lemma left_unitor_tensor (X Y : C) :
@@ -349,13 +247,16 @@ eq_of_inv_eq_inv (by simp)
 
 @[simp]
 lemma left_unitor_tensor_inv (X Y : C) :
-  ((λ_ (X ⊗ Y)).inv) = ((λ_ X).inv ⊗ (𝟙 Y)) ≫ ((α_ (𝟙_ C) X Y).hom) :=
+  (λ_ (X ⊗ Y)).inv = ((λ_ X).inv ⊗ (𝟙 Y)) ≫ (α_ (𝟙_ C) X Y).hom :=
 by { rw [←left_unitor_tensor_inv'], simp }
 
 @[simp]
 lemma right_unitor_tensor (X Y : C) :
-  ((ρ_ (X ⊗ Y)).hom) = ((α_ X Y (𝟙_ C)).hom) ≫ ((𝟙 X) ⊗ (ρ_ Y).hom) :=
-by rw [←tensor_right_iff, comp_tensor_id, right_unitor_product_aux]
+  (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ ((𝟙 X) ⊗ (ρ_ Y).hom) :=
+by
+  rw [←tensor_right_iff, comp_tensor_id, ←cancel_mono (α_ X Y (𝟙_ C)).hom, assoc,
+      associator_naturality, ←triangle_assoc, ←triangle, id_tensor_comp, pentagon_assoc,
+      ←associator_naturality, tensor_id]
 
 @[simp]
 lemma right_unitor_tensor_inv (X Y : C) :
@@ -364,27 +265,20 @@ eq_of_inv_eq_inv (by simp)
 
 lemma associator_inv_naturality {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
   (f ⊗ (g ⊗ h)) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) :=
-begin
-  apply (cancel_mono (α_ X' Y' Z').hom).1,
-  simp only [assoc, comp_id, iso.inv_hom_id],
-  rw [associator_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
-end
+by { rw [comp_inv_eq, assoc, associator_naturality], simp }
 
 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 :=
-begin
-  apply category_theory.eq_of_inv_eq_inv,
-  simp [monoidal_category.pentagon]
-end
+category_theory.eq_of_inv_eq_inv (by simp [pentagon])
 
 lemma triangle_assoc_comp_left (X Y : C) :
   (α_ X (𝟙_ C) Y).hom ≫ ((𝟙 X) ⊗ (λ_ Y).hom) = (ρ_ X).hom ⊗ 𝟙 Y :=
 monoidal_category.triangle X Y
 
 @[simp] lemma triangle_assoc_comp_right (X Y : C) :
   (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ⊗ 𝟙 Y) = ((𝟙 X) ⊗ (λ_ Y).hom) :=
-by rw [←triangle_assoc_comp_left, ←category.assoc, iso.inv_hom_id, category.id_comp]
+by rw [←triangle_assoc_comp_left, iso.inv_hom_id_assoc]
 
 @[simp] lemma triangle_assoc_comp_right_inv (X Y : C) :
   ((ρ_ X).inv ⊗ 𝟙 Y) ≫ (α_ X (𝟙_ C) Y).hom = ((𝟙 X) ⊗ (λ_ Y).inv) :=
@@ -402,6 +296,10 @@ begin
   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]
+
 end
 
 section