Documentation

Mathlib.CategoryTheory.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 CategoryTheory.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 CategoryTheory.Monoidal.NaturalTransformation for monoidal natural transformations.

We show in CategoryTheory.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 appropriate coherences.

Instances For

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

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

    Instances For

      The tensorator of a (strong) monoidal functor as an isomorphism.

      Instances For

        The composition of two lax monoidal functors is again lax monoidal.

        Instances For

          The composition of two monoidal functors is again monoidal.

          Instances For

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

            Instances For

              If a monoidal functor F is an equivalence of categories then its inverse is also monoidal.

              Instances For