feat(Category/Theory/Monoidal): monoids in a symmetric category form a symmetric category (#13058)

Author: kim-em

Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

@@ -332,6 +332,12 @@ theorem braiding_rightUnitor (X : C) : (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (
 theorem braiding_tensorUnit_left (X : C) : (β_ (𝟙_ C) X).hom = (λ_ X).hom ≫ (ρ_ X).inv := by
   simp [← braiding_rightUnitor]
 
+@[reassoc, simp]
+theorem braiding_inv_tensorUnit_left (X : C) : (β_ (𝟙_ C) X).inv = (ρ_ X).hom ≫ (λ_ X).inv := by
+  rw [Iso.inv_ext]
+  rw [braiding_tensorUnit_left]
+  coherence
+
 @[reassoc]
 theorem leftUnitor_inv_braiding (X : C) : (λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv := by
   simp
@@ -347,6 +353,12 @@ theorem rightUnitor_inv_braiding (X : C) : (ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom
 theorem braiding_tensorUnit_right (X : C) : (β_ X (𝟙_ C)).hom = (ρ_ X).hom ≫ (λ_ X).inv := by
   simp [← rightUnitor_inv_braiding]
 
+@[reassoc, simp]
+theorem braiding_inv_tensorUnit_right (X : C) : (β_ X (𝟙_ C)).inv = (λ_ X).hom ≫ (ρ_ X).inv := by
+  rw [Iso.inv_ext]
+  rw [braiding_tensorUnit_right]
+  coherence
+
 end
 
 /--

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -392,6 +392,8 @@ theorem one_rightUnitor {M : Mon_ C} :
   simp [← unitors_equal]
 #align Mon_.one_right_unitor Mon_.one_rightUnitor
 
+section BraidedCategory
+
 variable [BraidedCategory C]
 
 theorem Mon_tensor_one_mul (M N : Mon_ C) :
@@ -526,10 +528,69 @@ theorem associator_hom_hom (X Y Z : Mon_ C) : (α_ X Y Z).hom.hom = (α_ X.X Y.X
 @[simp]
 theorem associator_inv_hom (X Y Z : Mon_ C) : (α_ X Y Z).inv.hom = (α_ X.X Y.X Z.X).inv := rfl
 
+@[simp]
+theorem tensor_one (M N : Mon_ C) : (M ⊗ N).one = (λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one) := rfl
+
+@[simp]
+theorem tensor_mul (M N : Mon_ C) : (M ⊗ N).mul =
+    tensor_μ C (M.X, N.X) (M.X, N.X) ≫ (M.mul ⊗ N.mul) := rfl
+
 instance monMonoidal : MonoidalCategory (Mon_ C) where
   tensorHom_def := by intros; ext; simp [tensorHom_def]
 #align Mon_.Mon_monoidal Mon_.monMonoidal
 
+theorem one_braiding {X Y : Mon_ C} : (X ⊗ Y).one ≫ (β_ X.X Y.X).hom = (Y ⊗ X).one := by
+  simp only [monMonoidalStruct_tensorObj_X, tensor_one, Category.assoc,
+    BraidedCategory.braiding_naturality, braiding_tensorUnit_right, Iso.cancel_iso_inv_left]
+  coherence
+
+end BraidedCategory
+
+/-!
+We next show that if `C` is symmetric, then `Mon_ C` is braided, and indeed symmetric.
+
+Note that `Mon_ C` is *not* braided in general when `C` is only braided.
+
+The more interesting construction is the 2-category of monoids in `C`,
+bimodules between the monoids, and intertwiners between the bimodules.
+
+When `C` is braided, that is a monoidal 2-category.
+-/
+section SymmetricCategory
+
+variable [SymmetricCategory C]
+
+theorem mul_braiding {X Y : Mon_ C} :
+    (X ⊗ Y).mul ≫ (β_ X.X Y.X).hom = ((β_ X.X Y.X).hom ⊗ (β_ X.X Y.X).hom) ≫ (Y ⊗ X).mul := by
+  simp only [monMonoidalStruct_tensorObj_X, tensor_mul, tensor_μ, Category.assoc,
+    BraidedCategory.braiding_naturality, BraidedCategory.braiding_tensor_right,
+    BraidedCategory.braiding_tensor_left, comp_whiskerRight, whisker_assoc,
+    MonoidalCategory.whiskerLeft_comp, pentagon_assoc, pentagon_inv_hom_hom_hom_inv_assoc,
+    Iso.inv_hom_id_assoc, whiskerLeft_hom_inv_assoc]
+  slice_lhs 3 4 =>
+    -- We use symmetry here:
+    rw [← MonoidalCategory.whiskerLeft_comp, ← comp_whiskerRight, SymmetricCategory.symmetry]
+  simp only [id_whiskerRight, MonoidalCategory.whiskerLeft_id, Category.id_comp, Category.assoc,
+    pentagon_inv_assoc, Iso.hom_inv_id_assoc]
+  slice_lhs 1 2 =>
+    rw [← associator_inv_naturality_left]
+  slice_lhs 2 3 =>
+    rw [Iso.inv_hom_id]
+  rw [Category.id_comp]
+  slice_lhs 2 3 =>
+    rw [← associator_naturality_right]
+  slice_lhs 1 2 =>
+    rw [← tensorHom_def]
+  simp only [Category.assoc]
+
+instance : SymmetricCategory (Mon_ C) where
+  braiding := fun X Y => isoOfIso (β_ X.X Y.X) one_braiding mul_braiding
+  symmetry := fun X Y => by
+    ext
+    simp [← SymmetricCategory.braiding_swap_eq_inv_braiding]
+
+end SymmetricCategory
+
 end Mon_
 
 /-!