feat: predicate for a monoid object to be commutative (#22646)

I didn't know where to place these changes within the files, so I placed them at the end.

From Toric

Author: Kiolt

Mathlib/CategoryTheory/Monoidal/CommMon_.lean

@@ -233,3 +233,18 @@ def equivLaxBraidedFunctorPUnit : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C 
   counitIso := counitIso C
 
 end CommMon_
+
+namespace CommMon_
+
+variable {C}
+
+/-- Construct an object of `CommMon_ C` from an object `X : C` a `Mon_Class X` instance
+and a `IsCommMon X` insance. -/
+def mk' (X : C) [Mon_Class X] [IsCommMon X] : CommMon_ C where
+  __ := Mon_.mk' X
+  mul_comm := IsCommMon.mul_comm X
+
+instance (X : CommMon_ C) : IsCommMon X.X where
+  mul_comm' := X.mul_comm
+
+end CommMon_

Mathlib/CategoryTheory/Monoidal/Mon_.lean

@@ -671,6 +671,25 @@ end SymmetricCategory
 
 end Mon_
 
+section
+
+variable {C} [BraidedCategory.{v₁} C]
+
+/-- Predicate for a monoid object to be commutative. -/
+class IsCommMon (X : C) [Mon_Class X] where
+  mul_comm' : (β_ X X).hom ≫ μ = μ := by aesop_cat
+
+open scoped Mon_Class
+
+namespace IsCommMon
+
+@[reassoc (attr := simp)]
+theorem mul_comm (X : C) [Mon_Class X] [IsCommMon X] : (β_ X X).hom ≫ μ = μ := mul_comm'
+
+end IsCommMon
+
+end
+
 /-!
 Projects:
 * Check that `Mon_ MonCat ≌ CommMonCat`, via the Eckmann-Hilton argument.