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.

@[simp]
@[simp]
theorem discrete.add_monoidal_tensor_obj_as (M : Type u) [add_monoid M] (X Y : category_theory.discrete M) :
(X Y).as = X.as + Y.as

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