English
If M and N are commutative monoid objects, then their tensor product M ⊗ N is also a commutative monoid object.
Русский
Если M и N — коммутативные моноидальные объекты, то их тензорный произведение M ⊗ N также является коммутативным моноидальным объектом.
LaTeX
$$$\text{IsCommMonObj}(M) \wedge \text{IsCommMonObj}(N) \Rightarrow \text{IsCommMonObj}(M \otimes N)$$$
Lean4
instance [IsCommMonObj M] [IsCommMonObj N] : IsCommMonObj (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, MonObj.tensorObj.mul_def, ← whiskerLeft_comp_assoc, -whiskerLeft_comp]
