feat(category_theory/monoidal): prove that in a braided monoidal cate…

…gory unitors and associators are monoidal natural transformations (#13121)

This PR contains proofs of lemmas that are used in the stacked PR to define a monoidal structure on the category of monoids in a braided monoidal category.  The lemmas can be summarised by saying that in a braided monoidal category unitors and associators are monoidal natural transformations.

Note that for these statements to make sense we would need to define monoidal functors that are sources and targets of these monoidal natural transformations.  For example, the morphisms `(α_ X Y Z).hom` are the components of a monoidal natural transformation
```
(tensor.prod (𝟭 C)) ⊗⋙ tensor  ⟶ Α_ ⊗⋙ ((𝟭 C).prod tensor) ⊗⋙ tensor
```
where `Α_ : monoidal_functor ((C × C) × C) (C × (C × C))` is the associator functor given by `λ X, (X.1.1, (X.1.2, X.2))` on objects.  I didn't define the functor `Α_`.  (The easiest way would be to build it up using `prod'` we have already defined from `fst` and `snd`, which we would need to define as monoidal functors.)  Instead, I stated and proved the commutative diagram that expresses the monoidality of the above transformation.  Ditto for unitors.  Please let me know if you'd like me to define all the required functors and monoidal natural transformations.  The monoidal natural transformations themselves are not used in the proof that the category of monoids in a braided monoidal category is monoidal and only provide meaningful names to the lemmas that are used in the proof.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>

src/category_theory/monoidal/braided.lean

@@ -530,6 +530,177 @@ def tensor_monoidal : monoidal_functor (C × C) C :=
   μ_is_iso := by { dsimp [tensor_μ], apply_instance },
   .. tensor C }
 
+lemma left_unitor_monoidal (X₁ X₂ : C) :
+    (λ_ X₁).hom ⊗ (λ_ X₂).hom
+  = tensor_μ C (𝟙_ C, X₁) (𝟙_ C, X₂) ≫
+    ((λ_ (𝟙_ C)).hom ⊗ 𝟙 (X₁ ⊗ X₂)) ≫
+    (λ_ (X₁ ⊗ X₂)).hom :=
+begin
+  dsimp [tensor_μ],
+  have :
+      (λ_ X₁).hom ⊗ (λ_ X₂).hom
+    = (α_ (𝟙_ C) X₁ (𝟙_ C ⊗ X₂)).hom ≫
+      (𝟙 (𝟙_ C) ⊗ (α_ X₁ (𝟙_ C) X₂).inv) ≫
+      (λ_ ((X₁ ⊗ (𝟙_ C)) ⊗ X₂)).hom ≫
+      ((ρ_ X₁).hom ⊗ (𝟙 X₂)) := by pure_coherence,
+  rw this, clear this,
+  rw ←braiding_left_unitor,
+  slice_lhs 3 4 { rw [←id_comp (𝟙 X₂), tensor_comp] },
+  slice_lhs 3 4 { rw [←left_unitor_naturality] },
+  coherence,
+end
+
+lemma right_unitor_monoidal (X₁ X₂ : C) :
+    (ρ_ X₁).hom ⊗ (ρ_ X₂).hom
+  = tensor_μ C (X₁, 𝟙_ C) (X₂, 𝟙_ C) ≫
+    (𝟙 (X₁ ⊗ X₂) ⊗ (λ_ (𝟙_ C)).hom) ≫
+    (ρ_ (X₁ ⊗ X₂)).hom :=
+begin
+  dsimp [tensor_μ],
+  have :
+      (ρ_ X₁).hom ⊗ (ρ_ X₂).hom
+    = (α_ X₁ (𝟙_ C) (X₂ ⊗ (𝟙_ C))).hom ≫
+      (𝟙 X₁ ⊗ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv) ≫
+      (𝟙 X₁ ⊗ (ρ_ (𝟙_ C ⊗ X₂)).hom) ≫
+      (𝟙 X₁ ⊗ (λ_ X₂).hom) := by pure_coherence,
+  rw this, clear this,
+  rw ←braiding_right_unitor,
+  slice_lhs 3 4 { rw [←id_comp (𝟙 X₁), tensor_comp, id_comp] },
+  slice_lhs 3 4 { rw [←tensor_comp,
+                      ←right_unitor_naturality,
+                      tensor_comp] },
+  coherence,
+end
+
+lemma associator_monoidal_aux (W X Y Z : C) :
+    (𝟙 W ⊗ (β_ X (Y ⊗ Z)).hom) ≫
+    (𝟙 W ⊗ (α_ Y Z X).hom) ≫
+    (α_ W Y (Z ⊗ X)).inv ≫
+    ((β_ W Y).hom ⊗ 𝟙 (Z ⊗ X))
+  = (α_ W X (Y ⊗ Z)).inv ≫
+    (α_ (W ⊗ X) Y Z).inv ≫
+    ((β_ (W ⊗ X) Y).hom ⊗ 𝟙 Z) ≫
+    ((α_ Y W X).inv ⊗ 𝟙 Z) ≫
+    (α_ (Y ⊗ W) X Z).hom ≫
+    (𝟙 (Y ⊗ W) ⊗ (β_ X Z).hom) :=
+begin
+  slice_rhs 1 2 { rw ←pentagon_inv },
+  slice_rhs 3 5 { rw [←tensor_comp, ←tensor_comp,
+                      hexagon_reverse,
+                      tensor_comp, tensor_comp] },
+  slice_rhs 5 6 { rw associator_naturality },
+  slice_rhs 6 7 { rw [tensor_id,
+                      tensor_id_comp_id_tensor,
+                      ←id_tensor_comp_tensor_id] },
+  slice_rhs 2 3 { rw ←associator_inv_naturality },
+  slice_rhs 3 5 { rw pentagon_inv_inv_hom },
+  slice_rhs 4 5 { rw [←tensor_id,
+                      ←associator_inv_naturality] },
+  slice_rhs 2 4 { rw [←tensor_comp, ←tensor_comp,
+                      ←hexagon_forward,
+                      tensor_comp, tensor_comp] },
+  simp,
+end
+
+lemma associator_monoidal (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
+    tensor_μ C (X₁ ⊗ X₂, X₃) (Y₁ ⊗ Y₂, Y₃) ≫
+    (tensor_μ C (X₁, X₂) (Y₁, Y₂) ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
+    (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom
+  = ((α_ X₁ X₂ X₃).hom ⊗ (α_ Y₁ Y₂ Y₃).hom) ≫
+    tensor_μ C (X₁, X₂ ⊗ X₃) (Y₁, Y₂ ⊗ Y₃) ≫
+    (𝟙 (X₁ ⊗ Y₁) ⊗ tensor_μ C (X₂, X₃) (Y₂, Y₃)) :=
+begin
+  have :
+      (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom
+    = ((α_ X₁ Y₁ (X₂ ⊗ Y₂)).hom ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
+      ((𝟙 X₁ ⊗ (α_ Y₁ X₂ Y₂).inv) ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
+      (α_ (X₁ ⊗ ((Y₁ ⊗ X₂) ⊗ Y₂)) X₃ Y₃).inv ≫
+      ((α_ X₁ ((Y₁ ⊗ X₂) ⊗ Y₂) X₃).hom ⊗ 𝟙 Y₃) ≫
+      ((𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) Y₂ X₃).hom) ⊗ 𝟙 Y₃) ≫
+      (α_ X₁ ((Y₁ ⊗ X₂) ⊗ (Y₂ ⊗ X₃)) Y₃).hom ≫
+      (𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) (Y₂ ⊗ X₃) Y₃).hom) ≫
+      (𝟙 X₁ ⊗ (α_ Y₁ X₂ ((Y₂ ⊗ X₃) ⊗ Y₃)).hom) ≫
+      (α_ X₁ Y₁ (X₂ ⊗ ((Y₂ ⊗ X₃) ⊗ Y₃))).inv ≫
+      (𝟙 (X₁ ⊗ Y₁) ⊗ (𝟙 X₂ ⊗ (α_ Y₂ X₃ Y₃).hom)) ≫
+      (𝟙 (X₁ ⊗ Y₁) ⊗ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv) := by pure_coherence,
+  rw this, clear this,
+  slice_lhs 2 4 { rw [←tensor_comp, ←tensor_comp,
+                      tensor_μ_def₁,
+                      tensor_comp, tensor_comp] },
+  slice_lhs 4 5 { rw [←tensor_id,
+                      associator_inv_naturality] },
+  slice_lhs 5 6 { rw [←tensor_comp,
+                      associator_naturality,
+                      tensor_comp] },
+  slice_lhs 6 7 { rw [←tensor_comp, ←tensor_comp,
+                      associator_naturality,
+                      tensor_comp, tensor_comp] },
+  have :
+      ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
+      ((𝟙 X₁ ⊗ (α_ X₂ Y₁ Y₂).inv) ⊗ 𝟙 (X₃ ⊗ Y₃)) ≫
+      (α_ (X₁ ⊗ ((X₂ ⊗ Y₁) ⊗ Y₂)) X₃ Y₃).inv ≫
+      ((α_ X₁ ((X₂ ⊗ Y₁) ⊗ Y₂) X₃).hom ⊗ 𝟙 Y₃) ≫
+      ((𝟙 X₁ ⊗ (α_ (X₂ ⊗ Y₁) Y₂ X₃).hom) ⊗ 𝟙 Y₃)
+    = (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (X₃ ⊗ Y₃)).hom ≫
+      (𝟙 (X₁ ⊗ X₂) ⊗ (α_ (Y₁ ⊗ Y₂) X₃ Y₃).inv) ≫
+      (α_ X₁ X₂ (((Y₁ ⊗ Y₂) ⊗ X₃) ⊗ Y₃)).hom ≫
+      (𝟙 X₁ ⊗ (α_ X₂ ((Y₁ ⊗ Y₂) ⊗ X₃) Y₃).inv) ≫
+      (α_ X₁ (X₂ ⊗ ((Y₁ ⊗ Y₂) ⊗ X₃)) Y₃).inv ≫
+      ((𝟙 X₁ ⊗ (𝟙 X₂ ⊗ (α_ Y₁ Y₂ X₃).hom)) ⊗ 𝟙 Y₃) ≫
+      ((𝟙 X₁ ⊗ (α_ X₂ Y₁ (Y₂ ⊗ X₃)).inv) ⊗ 𝟙 Y₃) := by pure_coherence,
+  slice_lhs 2 6 { rw this }, clear this,
+  slice_lhs 1 3 { rw tensor_μ_def₁ },
+  slice_lhs 3 4 { rw [←tensor_id,
+                      associator_naturality] },
+  slice_lhs 4 5 { rw [←tensor_comp,
+                      associator_inv_naturality,
+                      tensor_comp] },
+  slice_lhs 5 6 { rw associator_inv_naturality },
+  slice_lhs 6 9 { rw [←tensor_comp, ←tensor_comp, ←tensor_comp,
+                      ←tensor_comp, ←tensor_comp, ←tensor_comp,
+                      tensor_id,
+                      associator_monoidal_aux,
+                      ←id_comp (𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁),
+                      ←id_comp (𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁ ≫ 𝟙 X₁),
+                      ←id_comp (𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃),
+                      ←id_comp (𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃ ≫ 𝟙 Y₃),
+                      tensor_comp, tensor_comp, tensor_comp, tensor_comp, tensor_comp,
+                      tensor_comp, tensor_comp, tensor_comp, tensor_comp, tensor_comp] },
+  slice_lhs 11 12 { rw associator_naturality },
+  slice_lhs 12 13 { rw [←tensor_comp,
+                        associator_naturality,
+                        tensor_comp] },
+  slice_lhs 13 14 { rw [←tensor_comp, ←tensor_id,
+                        associator_naturality,
+                        tensor_comp] },
+  slice_lhs 14 15 { rw associator_inv_naturality },
+  slice_lhs 15 17 { rw [tensor_id, ←tensor_comp, ←tensor_comp,
+                        ←tensor_μ_def₂,
+                        tensor_comp, tensor_comp] },
+  have :
+      ((𝟙 X₁ ⊗ ((α_ Y₁ X₂ X₃).inv ⊗ 𝟙 Y₂)) ⊗ 𝟙 Y₃) ≫
+      ((𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) X₃ Y₂).hom) ⊗ 𝟙 Y₃) ≫
+      (α_ X₁ ((Y₁ ⊗ X₂) ⊗ (X₃ ⊗ Y₂)) Y₃).hom ≫
+      (𝟙 X₁ ⊗ (α_ (Y₁ ⊗ X₂) (X₃ ⊗ Y₂) Y₃).hom) ≫
+      (𝟙 X₁ ⊗ (α_ Y₁ X₂ ((X₃ ⊗ Y₂) ⊗ Y₃)).hom) ≫
+      (α_ X₁ Y₁ (X₂ ⊗ ((X₃ ⊗ Y₂) ⊗ Y₃))).inv ≫
+      (𝟙 (X₁ ⊗ Y₁) ⊗ (𝟙 X₂ ⊗ (α_ X₃ Y₂ Y₃).hom)) ≫
+      (𝟙 (X₁ ⊗ Y₁) ⊗ (α_ X₂ X₃ (Y₂ ⊗ Y₃)).inv)
+    = (α_ X₁ ((Y₁ ⊗ (X₂ ⊗ X₃)) ⊗ Y₂) Y₃).hom ≫
+      (𝟙 X₁ ⊗ (α_ (Y₁ ⊗ (X₂ ⊗ X₃)) Y₂ Y₃).hom) ≫
+      (𝟙 X₁ ⊗ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom) ≫
+      (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ (Y₂ ⊗ Y₃))).inv := by pure_coherence,
+  slice_lhs 9 16 { rw this }, clear this,
+  slice_lhs 8 9 { rw associator_naturality },
+  slice_lhs 9 10 { rw [←tensor_comp,
+                       associator_naturality,
+                       tensor_comp] },
+  slice_lhs 10 12 { rw [tensor_id,
+                        ←tensor_μ_def₂] },
+  dsimp,
+  coherence,
+end
+
 end tensor
 
 end category_theory