mathlib documentation


(Lax) monoidal functors

A lax monoidal functor F between monoidal categories C and D is a functor between the underlying categories equipped with morphisms

A monoidal functor is a lax monoidal functor for which ε and μ are isomorphisms.

We show that the composition of (lax) monoidal functors gives a (lax) monoidal functor.

See also category_theory.monoidal.functorial for a typeclass decorating an object-level function with the additional data of a monoidal functor. This is useful when stating that a pre-existing functor is monoidal.

See category_theory.monoidal.natural_transformation for monoidal natural transformations.

We show in category_theory.monoidal.Mon_ that lax monoidal functors take monoid objects to monoid objects.

Future work



A lax monoidal functor is a functor F : C ⥤ D between monoidal categories, equipped with morphisms ε : 𝟙 _D ⟶ F.obj (𝟙_ C) and μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y), satisfying the the appropriate coherences.

structure category_theory.monoidal_functor (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (D : Type u₂) [category_theory.category D] [category_theory.monoidal_category D] :
Type (max u₁ u₂ v₁ v₂)

A monoidal functor is a lax monoidal functor for which the tensorator and unitor as isomorphisms.


The identity lax monoidal functor.


The identity monoidal functor.