Monoid object

Category of monoid objects

The category of monoids in , denoted , is a category where an object is a Monoid object in and a morphism is a Monoid morphism. #m/def/cat In particular, is the same as .

As the cocartesian completion of a symmetric monoidal category

If is a symmetric monoidal category then the tensor product of two monoids in naturally carries the structure of a monoid with the unit and multiplication

c c

With the product defined as such, is in fact a cocartesian category. #m/thm/cat

Proof

Suppose are monoids in . We define monoid morphisms

c c c

and claim these satisfy the universal property of the coproduct. Namely, if and are monoid morphisms in , then we claim is the unique monoid morphism such that

c

commutes. Suppose that can replace in the commutative diagram. Then

so as required.

#state/tidy | #lang/en | #SemBr