feat: tensor product of group objects (#29134)

... and similarly for commutative monoid objects.

From Toric

Author: YaelDillies

Mathlib/CategoryTheory/Monoidal/Grp_.lean

@@ -252,11 +252,17 @@ lemma toMon_Class_injective {X : C} :
   exacts [congr(($e.symm).mul), congr(($e.symm).one)]
 
 @[ext]
-lemma _root_.Grp_Class.ext {X : C} (h₁ h₂ : Grp_Class X)
-    (H : h₁.toMon_Class = h₂.toMon_Class) : h₁ = h₂ :=
+lemma ext {X : C} (h₁ h₂ : Grp_Class X) (H : h₁.toMon_Class = h₂.toMon_Class) : h₁ = h₂ :=
   Grp_Class.toMon_Class_injective H
 
-end Grp_Class
+namespace tensorObj
+variable [BraidedCategory C] {G H : C} [Grp_Class G] [Grp_Class H]
+
+@[simps inv]
+instance : Grp_Class (G ⊗ H) where
+  inv := ι ⊗ₘ ι
+
+end Grp_Class.tensorObj
 
 namespace Grp_
 

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -942,6 +942,18 @@ lemma Mon_Class.mul_mul_mul_comm' [IsCommMon M] :
 
 end
 
+section SymmetricCategory
+variable [SymmetricCategory C] {M N W X Y Z : C} [Mon_Class M] [Mon_Class N]
+
+instance [IsCommMon M] [IsCommMon N] : IsCommMon (M ⊗ N) where
+  mul_comm := by
+    simp [← IsIso.inv_comp_eq, tensorμ, ← associator_inv_naturality_left_assoc,
+      ← associator_naturality_right_assoc, SymmetricCategory.braiding_swap_eq_inv_braiding M N,
+      ← tensorHom_def_assoc, -whiskerRight_tensor, -tensor_whiskerLeft, ← tensor_comp,
+      Mon_Class.tensorObj.mul_def, ← whiskerLeft_comp_assoc, -whiskerLeft_comp]
+
+end SymmetricCategory
+
 /-!
 Projects:
 * Check that `Mon_ MonCat ≌ CommMonCat`, via the Eckmann-Hilton argument.