GitHub

Monoidal Categories

A monoidal category is a quintuplet $(\mathcal C, \otimes, \mathbb 1, a, \iota)$ where

  • $\mathcal C$ is a category
  • $\otimes\colon \mathcal C \times \mathcal C \to \mathcal C$is a bifunctor
  • $a_{X,Y,Z} \colon (X \otimes Y) \otimes Z \to X \otimes (Y \otimes Z)$ is a natural transformation
  • $\iota \colon \mathbb 1 \otimes \mathbb 1 \to \mathbb 1$ is an isomorphism

such that

\begin{tikzcd} & {((W \otimes X) \otimes Y)\otimes Z} \\ {(W \otimes (X \otimes Y)) \otimes Z} && {(W \otimes X) \otimes (Y\otimes Z)} \\ {W \otimes ((X\otimes Y) \otimes Z)} && {W \otimes (X \otimes (Y\otimes Z))} \arrow["{a_{W,X,Y} \otimes \mathrm{id}_Z}"'{pos=1}, shorten <=4pt, from=1-2, to=2-1] \arrow["{a_{W,X\otimes Y,Z}}"', shift right=5, draw=none, from=2-1, to=3-1] \arrow[from=2-1, to=3-1] \arrow["{\mathrm{id}\otimes a_{X,Y,Z}}"', from=3-1, to=3-3] \arrow["{a_{W\otimes X, Y,Z}}"{pos=0.8}, from=1-2, to=2-3] \arrow["{a_{W,X,Y\otimes Z}}", shift left=5, draw=none, from=2-3, to=3-3] \arrow[from=2-3, to=3-3] \end{tikzcd}

commutes for all objects $W,X,Y,Z$ in $\mathcal C$ and

\[\begin{align*} L_{\mathbb 1} \colon & X \to \mathbb 1 \otimes X \\ R_{\mathbb 1} \colon & X \to X \otimes \mathbb 1 \end{align*}\]

are autoequivalences.

Conventions and Restrictions

At the current state all monoidal categories are assumed to satisfy $X \otimes \mathbb 1 \cong X \cong \mathbb 1 \otimes X$ and $\iota = \mathrm{id}_{\mathbb 1}$.

But building non-strict monoidal categories is explicitly encouraged, as this support is a strength of our Package.

Monoidal Categories

Following the definition we need the following methods.

  • tensor_product(X::YourObject...)::YourObject returning the monoidal product. You can access your method by invoking the infix operate ⊗.
  • tensor_product(f::YourMorphism...)::YourMorphism returning the the monoidal product of morphisms. You can access your method by invoking the infix operate ⊗.
  • one(C::YourCategory)::YourObject returning the monoidal unit.
  • associator(X::YourObject, Y::YourObject, Z::YourObject).

Rigidity

Whenever there are objects which admit duals it is feasible to acces them.

  • left_dual(X::YourObject)::YourObject return the left dual $X^\ast$.
  • right_dual(X::YourObject)::YourObject return the right dual ${}^\ast X$.
  • ev(X::YourObject)::YourMorphism return the evaluation morphism $\mathrm{ev}_X\colon X^\ast \otimes X \to \mathbb 1$.
  • coev(X::YourObject)::YourMorphism return the coevaluation morphism $\mathrm{coev}_X\colon \mathbb 1 \to X\otimes X^\ast$.

This allows to generically compute

Note that dual will always call left_dual.