mathlib documentation

category_theory.monoidal.discrete

Monoids as discrete monoidal categories #

The discrete category on a monoid is a monoidal category. Multiplicative morphisms induced monoidal functors.

A multiplicative morphism between monoids gives a monoidal functor between the corresponding discrete monoidal categories.

Equations