mathlib3 documentation

category_theory.monoidal.discrete

Monoids as discrete monoidal categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[simp]

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