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 #

References #


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 appropriate coherences.

theorem category_theory.lax_monoidal_functor.μ_natural_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (c : category_theory.lax_monoidal_functor C D) {X Y X' Y' : C} (f : X Y) (g : X' Y') {X'_1 : D} (f' : c.to_functor.obj (Y Y') X'_1) :
( f g) c.μ Y Y' f' = c.μ X X' (f g) f'
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.


If we have a right adjoint functor G to a monoidal functor F, then G has a lax monoidal structure as well.