chore(category_theory): speed-up monoidal.of_has_finite_products (#1616)

leanprover-community · Oct 29, 2019 · 6030ff0 · 6030ff0
1 parent e6e25d0
commit 6030ff0
Show file tree

Hide file tree

Showing 2 changed files with 42 additions and 2 deletions.
diff --git a/src/category_theory/limits/shapes/binary_products.lean b/src/category_theory/limits/shapes/binary_products.lean
@@ -147,6 +147,17 @@ by tidy
     (prod.lift prod.fst (prod.snd ≫ prod.fst))
     (prod.snd ≫ prod.snd) }
 
+lemma prod.pentagon (W X Y Z : C) :
+  prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫
+      (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) =
+    (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y⨯Z)).hom :=
+by tidy
+
+lemma prod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
+  prod.map (prod.map f₁ f₂) f₃ ≫ (prod.associator Y₁ Y₂ Y₃).hom =
+    (prod.associator X₁ X₂ X₃).hom ≫ prod.map f₁ (prod.map f₂ f₃) :=
+by tidy
+
 variables [has_terminal.{v} C]
 
 /-- The left unitor isomorphism for binary products with the terminal object. -/
@@ -160,6 +171,12 @@ variables [has_terminal.{v} C]
   (P : C) : P ⨯ ⊤_ C ≅ P :=
 { hom := prod.fst,
   inv := prod.lift (𝟙 _) (terminal.from P) }
+
+lemma prod.triangle (X Y : C) :
+  (prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) ((prod.left_unitor Y).hom) =
+    prod.map ((prod.right_unitor X).hom) (𝟙 Y) :=
+by tidy
+
 end
 
 section
@@ -189,6 +206,17 @@ by tidy
     (coprod.inl ≫ coprod.inl)
     (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr) }
 
+lemma coprod.pentagon (W X Y Z : C) :
+  coprod.map ((coprod.associator W X Y).hom) (𝟙 Z) ≫
+      (coprod.associator W (X⨿Y) Z).hom ≫ coprod.map (𝟙 W) ((coprod.associator X Y Z).hom) =
+    (coprod.associator (W⨿X) Y Z).hom ≫ (coprod.associator W X (Y⨿Z)).hom :=
+by tidy
+
+lemma coprod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
+  coprod.map (coprod.map f₁ f₂) f₃ ≫ (coprod.associator Y₁ Y₂ Y₃).hom =
+    (coprod.associator X₁ X₂ X₃).hom ≫ coprod.map f₁ (coprod.map f₂ f₃) :=
+by tidy
+
 variables [has_initial.{v} C]
 
 /-- The left unitor isomorphism for binary coproducts with the initial object. -/
@@ -202,6 +230,12 @@ variables [has_initial.{v} C]
   (P : C) : P ⨿ ⊥_ C ≅ P :=
 { hom := coprod.desc (𝟙 _) (initial.to P),
   inv := coprod.inl }
+
+lemma coprod.triangle (X Y : C) :
+  (coprod.associator X (⊥_ C) Y).hom ≫ coprod.map (𝟙 X) ((coprod.left_unitor Y).hom) =
+    coprod.map ((coprod.right_unitor X).hom) (𝟙 Y) :=
+by tidy
+
 end
 
 end category_theory.limits
diff --git a/src/category_theory/monoidal/of_has_finite_products.lean b/src/category_theory/monoidal/of_has_finite_products.lean
@@ -38,7 +38,10 @@ def monoidal_of_has_finite_products [has_finite_products.{v} C] : monoidal_categ
   tensor_hom   := λ _ _ _ _ f g, limits.prod.map f g,
   associator   := prod.associator,
   left_unitor  := prod.left_unitor,
-  right_unitor := prod.right_unitor }
+  right_unitor := prod.right_unitor,
+  pentagon'    := prod.pentagon,
+  triangle'    := prod.triangle,
+  associator_naturality' := @prod.associator_naturality _ _ _, }
 
 /-- A category with finite coproducts has a natural monoidal structure. -/
 def monoidal_of_has_finite_coproducts [has_finite_coproducts.{v} C] : monoidal_category C :=
@@ -47,7 +50,10 @@ def monoidal_of_has_finite_coproducts [has_finite_coproducts.{v} C] : monoidal_c
   tensor_hom   := λ _ _ _ _ f g, limits.coprod.map f g,
   associator   := coprod.associator,
   left_unitor  := coprod.left_unitor,
-  right_unitor := coprod.right_unitor }
+  right_unitor := coprod.right_unitor,
+  pentagon'    := coprod.pentagon,
+  triangle'    := coprod.triangle,
+  associator_naturality' := @coprod.associator_naturality _ _ _, }
 
 end