# mathlibdocumentation

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]
.as = 0
@[simp]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
def category_theory.discrete.monoidal (M : Type u) [monoid M] :
Equations
@[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
def category_theory.discrete.monoidal_functor {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) :

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

Equations
@[simp]
theorem discrete.add_monoidal_functor_to_lax_monoidal_functor_ε {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) :
@[simp]
@[simp]
theorem discrete.add_monoidal_functor_to_lax_monoidal_functor_μ {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) (X Y : category_theory.discrete M) :
@[simp]
theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_ε {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) :
def discrete.add_monoidal_functor {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) :

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

Equations
@[simp]
theorem discrete.add_monoidal_functor_to_lax_monoidal_functor_to_functor_map {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] (F : M →+ N) (X Y : category_theory.discrete M) (f : X Y) :
@[simp]
theorem category_theory.discrete.monoidal_functor_to_lax_monoidal_functor_to_functor_map {M : Type u} [monoid M] {N : Type u} [monoid N] (F : M →* N) (X Y : category_theory.discrete M) (f : X Y) :
def discrete.add_monoidal_functor_comp {M : Type u} [add_monoid M] {N : Type u} [add_monoid N] {K : Type u} [add_monoid K] (F : M →+ N) (G : N →+ K) :

The monoidal natural isomorphism corresponding to composing two additive morphisms.

Equations
def category_theory.discrete.monoidal_functor_comp {M : Type u} [monoid M] {N : Type u} [monoid N] {K : Type u} [monoid K] (F : M →* N) (G : N →* K) :

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

Equations