Why are the monoid objects in Mon(C) the commutative monoids?

Question

Let $(C, \otimes, 1, \alpha, l, r)$ be a symmetric monoidal category. Can someone explain me why the monoids in the category of monoids Mon(C) are the abelian monoids ?

Thanks for your help.

Answer 1

It is often clarifying to explicitly indicate the variable context of terms and equations between terms. I like to use the notation $x:A,y:B,z:C\vdash s = t$ to indicate that $x$ is a variable of sort $A$, $y$ of sort $B$, and $z$ of sort $C$ and these are the only free variables that may occur in the terms $s$ and $t$. Using this convention, we can write the laws defining monoids as follows: $$x:M,y:M,z:M\vdash x*(y*z) = (x*y)*z$$ $$x:M\vdash x*1 = x \qquad x:M\vdash 1*x=x$$

Because each side of each of these equations uses all of the variables in the variable context exactly once and in the order they are listed, these equations are in the doctrine of monoidal categories. (For contrast, the law for groups $x:G\vdash x*x^{-1}=1$ duplicates the variable on the left and ignores it on the right, and so this equation is not within the doctrine of monoidal categories. This is why we need cartesian products and not just monoidal products to talk about group objects.) In this view $*:M\otimes M\to M$ and $1 : I \to M$. The doctrine of symmetric monoidal categories additionally allows equations that used the variables in any order though still exactly once each.

A term in a given variable context corresponds to an arrow out of a monoidal product. For example, the terms of the monoid associative law corresponds to the arrows $*\circ(id_M\otimes *):M\otimes M\otimes M \to M$ and $*\circ(*\otimes id_M):M\otimes M\otimes M\to M$. These are not actually compatible unless the monoidal structure is strict, but the laws of a (symmetric) monoidal category guarantee that however you do choose to associate $M\otimes M\otimes M$ and insert associators to make these two arrows compatible, it makes no difference.

In the doctrine of symmetric monoidal categories, you can simply take the series of equations as presented, e.g., on Wikipedia and interpret them as above. It's apparent that all of them use the relevant free variables exactly once. If you like, you can translate the element-wise equations into equations between arrows as above which will require inserting associators, unitors, and symmetries. The naturality of these will be important in showing the equalities. And again, how you decide to insert these will not affect the result. Essentially, given two object expressions involving $\otimes$ and $I$ built from the same multi-set of objects, every way of building an arrow between them using the associator, symmetry, unitors, identities, and $\otimes$ produces the same result (which will thus necessarily be an isomorphism) modulo permuting duplicate objects. If we further are given a desired permutation for the duplicate objects, then all the ways of realizing that permutation are equal. For the monoid object in $\mathsf{Mon}(\mathcal C)$ view, the exchange assumption, i.e. that $x:M,y:M,z:M,w:M\vdash(x*y)\star(z*w)=(x\star z)*(y\star w)$, is the statement that $\star$ is a monoid homomorphism with respect to $*$, i.e. $\star$ is an arrow in $\mathsf{Mon}(\mathcal C)$.