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.

@[protected, instance]
Equations

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

Equations

An additive morphism between add_monoids gives a monoidal functor between the corresponding discrete monoidal categories.

Equations