traced monoidal category

In category theory, a traced monoidal category is a category with some extra structure which gives a reasonable notion of feedback.

A traced symmetric monoidal category is a symmetric monoidal category C together with a family of functions

:$\backslash mathrm\{Tr\}^U\_\{X,Y\}:\backslash mathbf\{C\}(X\backslash otimes\; U,Y\backslash otimes\; U)\backslash to\backslash mathbf\{C\}(X,Y)$

called a trace, satisfying the following conditions:

• naturality in $X$: for every $f:X\backslash otimes\; U\backslash to\; Y\backslash otimes\; U$ and $g:X\text{'}\backslash to\; X$,

::$\backslash mathrm\{Tr\}^U\_\{X\text{'},Y\}(f\; \backslash circ\; (g\backslash otimes\; \backslash mathrm\{id\}\_U))\; =\; \backslash mathrm\{Tr\}^U\_\{X,Y\}(f)\; \backslash circ\; g$

Image:Trace diagram naturality 1.svg

• naturality in $Y$: for every $f:X\backslash otimes\; U\backslash to\; Y\backslash otimes\; U$ and $g:Y\backslash to\; Y\text{'}$,

::$\backslash mathrm\{Tr\}^U\_\{X,Y\text{'}\}((g\backslash otimes\; \backslash mathrm\{id\}\_U)\; \backslash circ\; f)\; =\; g\; \backslash circ\; \backslash mathrm\{Tr\}^U\_\{X,Y\}(f)$

Image:Trace diagram naturality 2.svg

• dinaturality in $U$: for every $f:X\backslash otimes\; U\backslash to\; Y\backslash otimes\; U\text{'}$ and $g:U\text{'}\backslash to\; U$

::$\backslash mathrm\{Tr\}^U\_\{X,Y\}((\backslash mathrm\{id\}\_Y\backslash otimes\; g)\; \backslash circ\; f)=\backslash mathrm\{Tr\}^\{U\text{'}\}\_\{X,Y\}(f\; \backslash circ\; (\backslash mathrm\{id\}\_X\backslash otimes\; g))$

Image:Trace diagram dinaturality.svg

• vanishing I: for every $f:X\; \backslash otimes\; I\; \backslash to\; Y\; \backslash otimes\; I$, (with $\backslash rho\_X\; \backslash colon\; X\backslash otimes\; I\backslash cong\; X$ being the right unitor),

::$\backslash mathrm\{Tr\}^I\_\{X,Y\}(f)=\backslash rho\_Y\; \backslash circ\; f\; \backslash circ\; \backslash rho\_X^\{-1\}$

Image:Trace diagram vanishing.svg

• vanishing II: for every $f:X\backslash otimes\; U\backslash otimes\; V\backslash to\; Y\backslash otimes\; U\backslash otimes\; V$

::$\backslash mathrm\{Tr\}^U\_\{X,Y\}(\backslash mathrm\{Tr\}^V\_\{X\backslash otimes\; U,Y\backslash otimes\; U\}(f))\; =\; \backslash mathrm\{Tr\}^\{U\backslash otimes\; V\}\_\{X,Y\}(f)$

Image:Trace diagram associativity.svg

• superposing: for every $f:X\backslash otimes\; U\backslash to\; Y\backslash otimes\; U$ and $g:W\backslash to\; Z$,

::$g\backslash otimes\; \backslash mathrm\{Tr\}^U\_\{X,Y\}(f)=\backslash mathrm\{Tr\}^U\_\{W\backslash otimes\; X,Z\backslash otimes\; Y\}(g\backslash otimes\; f)$

Image:Trace diagram superposition.svg

• yanking:

::$\backslash mathrm\{Tr\}^X\_\{X,X\}(\backslash gamma\_\{X,X\})=\backslash mathrm\{id\}\_X$

(where $\backslash gamma$ is the symmetry of the monoidal category).

Image:Trace diagram yanking.svg