mathlib documentation

category_theory.monoidal.functor

(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

See https://stacks.math.columbia.edu/tag/0FFL.

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.

@[simp]
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) :
(c.to_functor.map f c.to_functor.map g) c.μ Y Y' f' = c.μ X X' c.to_functor.map (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.

See https://stacks.math.columbia.edu/tag/0FFL.

The identity lax monoidal functor.

Equations

The identity monoidal functor.

Equations