Documentation

Mathlib.CategoryTheory.Monoidal.NaturalTransformation

Monoidal natural transformations #

Natural transformations between (lax) monoidal functors must satisfy an additional compatibility relation with the tensorators: F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y.

(Lax) monoidal functors between a fixed pair of monoidal categories themselves form a category.

A monoidal natural transformation is a natural transformation between (lax) monoidal functors additionally satisfying: F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y

Instances For

    Construct a monoidal natural isomorphism from object level isomorphisms, and the monoidal naturality in the forward direction.

    Instances For

      The unit of a monoidal equivalence can be upgraded to a monoidal natural transformation.

      Instances For

        The counit of a monoidal equivalence can be upgraded to a monoidal natural transformation.

        Instances For