A survey of graphical languages for monoidal categories

Peter Selinger

Introduction

There are many kinds of monoidal categories with additional structure — braided, rigid, pivotal, balanced, tortile, ribbon, autonomous, sovereign, spherical, traced, compact closed, *-autonomous, to name a few. Many of them have an associated graphical language of “string diagrams”. The proliferation of different notions is often confusing to non-experts, and occasionally to experts as well. To add to the confusion, one concept often appears in the literature under multiple names (for example, “rigid” is the same as “autonomous”, “sovereign” is the same as “pivotal”, and “ribbon” is the same as “tortile”).

In this survey, I attempt to give a systematic overview of the main notions and their associated graphical languages. My initial intention was to summarize, without proof, only the main definitions and coherence results that appear in the literature. However, it quickly became apparent that, in the interest of being systematic, I had to include some additional notions. This led to the sections on spacial categories, and planar and braided traced categories.

Historically, the terminology was often fixed for special cases before more general cases were considered. As a result, some concepts have a common name (such as “compact closed category”) where another name would have been more systematic (e.g. “symmetric autonomous category”). I have resisted the temptation to make major changes to the established terminology. However, I propose some minor tweaks that will hopefully not be disruptive. For example, I prefer “traced category”, which can be combined with various qualifying adjectives, to the longer and less flexible “traced monoidal category”.

Many of the coherence results are widely known, or at least presumed to be true, but some of them are not explicitly found in the literature. For those that can be attributed, I have attempted to do so, sometimes with a caveat if only special cases have been proved in the literature. For some easy results, I have provided proof sketches. Some unproven results have been included as conjectures.

While the results surveyed here are mathematically rigorous, I have shied away from giving the full technical details of the definitions of the graphical languages and their respective notions of equivalence of diagrams. Instead, I present the graphical languages somewhat informally, but in a way that will be sufficient for most applications. Where appropriate, full mathematical details can be found in the references.

Readers who want a quick overview of the different notions are encouraged to first consult the summary chart at the end of this article.

An updated version of this article will be maintained on the ArXiv, so I encourage readers to contact me with corrections, literature references, and updates.

The use of graphical notations for operator diagrams in physics goes back to Penrose . Initially, such notations applied to multiplications and tensor products of linear operators, but it became gradually understood that they are applicable in more general situations.

To see how graphical languages arise from matrix multiplication, consider the following example. Let M:A→BM:A\rightarrow B, N:B⊗C→DN:B\otimes C\rightarrow D, and P:D→EP:D\rightarrow E be linear maps between finite dimensional vector spaces A,B,C,D,EA,B,C,D,E. These maps can be combined in an obvious way to obtain a linear map F:A⊗C→EF:A\otimes C\rightarrow E. In functional notation, the map FF can be written

The same can be expressed as a summation over matrix indices, relative to some chosen basis of each space. In mathematical notation, suppose M=(mj,i)M=(m_{j,i}), N=(nl,jk)N=(n_{l,jk}), P=(pm,l)P=(p_{m,l}), and F=(fm,ik)F=(f_{m,ik}), where i,j,k,l,mi,j,k,l,m range over basis vectors of the respective spaces. Then

In (1.2) and (1.3), the order of the factors in the multiplication is not relevant, as all the information is contained in the indices. Also note that, while the notation mentions the chosen bases, the result is of course basis independent. This is because indices occur in pairs of opposite variance (if on the same side of the equation) or equal variance (if on opposite sides of the equation). It was Penrose who first pointed out that the notation is valid in many situations where the indices are purely formal symbols, and the maps may not even be between vector spaces.

= \vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 3.01175pt\hbox{{\hbox{\kern-3.01175pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.00565pt\hbox{\xyscale@@{1.0}{1.0}\kern 0.0pt\kern 0.0pt}}}}}}}}}}=\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 2.93901pt\hbox{{\hbox{\kern-2.93901pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-0.00047pt\hbox{\xyscale@@{1.0}{1.0}\kern 0.0pt\kern 0.0pt}}}}}}}}}} (1.4) Finally, since the indices no longer serve any purpose, one may omit them from the notation. Instead, it is more useful to label each wire with the name of the corresponding space.

= \vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 3.01175pt\hbox{{\hbox{\kern-3.01175pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-0.00414pt\hbox{\xyscale@@{1.0}{1.0}\kern 0.0pt\kern 0.0pt}}}}}}}}}}=\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 2.93901pt\hbox{{\hbox{\kern-2.93901pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-0.01405pt\hbox{\xyscale@@{1.0}{1.0}\kern 0.0pt\kern 0.0pt}}}}}}}}}} (1.5) In the notation of monoidal categories, (1.5) can be expressed as a commutative diagram

Thus, we have completed a full circle and arrived back at the notation (1.1) that we started with.

Organization of the paper.

In each of the remaining sections of this paper, we will consider a particular class of categories and its associated graphical language.

Acknowledgments.

I would like to thank Gheorghe Ştefănescu and Ross Street for their help in locating hard-to-obtain references, and for providing some background information. Thanks to Fabio Gadducci, Chris Heunen, and Micah McCurdy for useful comments on an earlier draft.

Categories

We only give the most basic definitions of categories, functors, and natural transformations. For a gentler introduction, with more details and examples, see e.g. Mac Lane .

a class ∣C∣|{\bf C}| of objects, denoted AA, BB, CC, …;

for each pair of objects A,BA,B, a set homC(A,B)\textrm{\rm hom}_{{\bf C}}(A,B) of morphisms, which are denoted f:A→Bf:A\rightarrow B;

identity morphisms idA:A→A\textrm{\rm id}_{A}:A\rightarrow A and the operation of composition: if f:A→Bf:A\rightarrow B and g:B→Cg:B\rightarrow C, then

for all f:A→Bf:A\rightarrow B, g:B→Cg:B\rightarrow C, and h:C→Dh:C\rightarrow D.

The terms “map” or “arrow” are often used interchangeably with “morphism”.

Some examples of categories are: the category Set of sets (with functions as the morphisms); the category Rel of sets (with relations as the morphisms); the category Vect of vector spaces (with linear maps); the category Hilb of Hilbert spaces (with bounded linear maps); the category UHilb of Hilbert spaces (with unitary maps); the category Top of topological spaces (with continuous maps); the category Cob of nn-dimensional oriented manifolds (with oriented cobordisms). Note that in each case, we need to specify not only the objects, but also the morphisms (and technically the composition and identities, although they are often clear from the context).

Categories also arise in other sciences, for example in logic (where the objects are propositions and the morphisms are proofs), and in computing (where the objects are data types and the morphisms are programs).

Many concepts associated with sets and functions, such as inverse, monomorphism (injective map), idempotent, cartesian product, etc., are definable in an arbitrary category.

In the graphical language of categories, objects are represented as wires (also called edges) and morphisms are represented as boxes (also called nodes). An identity morphisms is represented as a continuing wire, and composition is represented by connecting the outgoing wire of one diagram to the incoming wire of another. This is shown in Table 1.

Coherence.

Note that the three defining axioms of categories (e.g., idB∘f=f\textrm{\rm id}_{B}\circ f=f) are automatically satisfied “up isomorphism” in the graphical language. This property is known as soundness. A converse of this statement is also true: every equation that holds in the graphical language is a consequence of the axioms. This property is called completeness. We refer to a soundness and completeness theorem as a coherence theorem.

A well-formed equation between two morphism terms in the language of categories follows from the axioms of categories if and only if it holds in the graphical language up to isomorphism of diagrams.

Hopefully it is obvious what is meant by isomorphism of diagrams: two diagrams are isomorphic if the boxes and wires of the first are in bijective correspondence with the boxes and wires of the second, preserving the connections between boxes and wires.

Admittedly, the above coherence theorem for categories is a triviality, and is not usually stated in this way. However, we have included it for sake of uniformity, and for comparison with the less trivial coherence theorems for monoidal categories in the following sections. The proof is straightforward, since by the associativity and unit axioms, each morphism term is uniquely equivalent to a term of the form ((fn∘…)∘f2)∘f1((f_{n}\circ\ldots)\circ f_{2})\circ f_{1} for n≥0n\geq 0, with corresponding diagram

We have equipped wires with a left-to-right arrow, and boxes with a marking in the upper left corner. These markings are of no use at the moment, but will become important as we extend the language in the following sections.

Technicalities

So far, we have not been very precise about what the wires and boxes of a diagram are labeled with. We have also glossed over what was meant by “a well-formed equation between morphism terms in the language of categories”. We now briefly explain these notions, without giving all the formal details. For a more precise mathematical treatment, see e.g. Joyal and Street .

The wires of a diagram are labeled with object variables, and the boxes are labeled with morphism variables. To understand what this means, consider the familiar language of arithmetic expressions. This language deals with terms, such as (x+y+2)(x+3)(x+y+2)(x+3), which are built up from variables, such as xx and yy, constants, such as 22 and 33, by means of operations, such as addition and multiplication. Variables can be viewed in three different ways: first, they can be viewed as symbols that can be compared (e.g. the variable xx occurs twice in the given term, and is different from the variable yy). They can also be viewed as placeholders for arbitrary numbers, for example x=5x=5 and y=15y=15. Here xx and yy are allowed to represent different numbers or the same number; however, the two occurrences of xx must denote the same number. Finally, variables can be viewed as placeholders for arbitrary terms, such as x=a+bx=a+b and y=z2y=z^{2}.

The formal language of category theory is similar, except that we require two sets of variables: object variables (for labeling wires) and morphism variables (for labeling boxes). We must also equip each morphism variable with a specified domain and codomain. The following definition makes this more precise.

A simple (categorical) signature Σ\Sigma consists of a set Σ0\Sigma_{0} of object variables, a set Σ1\Sigma_{1} of morphism variables, and a pair of functions dom,cod:Σ1→Σ0\mathop{\textrm{\rm dom}}\nolimits,\mathop{\textrm{\rm cod}}\nolimits:\Sigma_{1}\rightarrow\Sigma_{0}. Object variables are usually written A,B,C,…A,B,C,\ldots, morphism variables are usually written f,g,h,…f,g,h,\ldots, and we write f:A→Bf:A\rightarrow B if dom(f)=A\mathop{\textrm{\rm dom}}\nolimits(f)=A and cod(f)=B\mathop{\textrm{\rm cod}}\nolimits(f)=B.

Given a simple signature, we can then build morphism terms, such as f∘(g∘idA)f\circ(g\circ\textrm{\rm id}_{A}), which are built from morphism variables (such as ff and gg) and morphism constants (such as idA\textrm{\rm id}_{A}), via operations (i.e., composition). Each term is recursively equipped with a domain and a codomain, and we must require compositions to respect the domain and codomain information. A term that obeys these rules is called well-formed. Finally, an equation between terms is called a well-formed equation if the left-hand side and right-hand side are well-formed terms that moreover have equal domains and equal codomains.

The graphical language is also relative to a given signature. The wires and boxes are labeled, respectively, with object variables and morphism variables from the signature, and the labeling must respect the domain and codomain information. This means that the wire entering (respectively, exiting) a box labeled ff must be labeled by the domain (respectively, codomain) of ff.

The above remark about the different roles of variables in arithmetic also holds for the diagrammatic language of categories. On the one hand, the labels can be viewed as formal symbols. This is the view used in the coherence theorem, where the formal labels are part of the definition of equivalence (in this case, isomorphism) of diagrams.

The labels can also be viewed as placeholders for specific objects and morphisms in an actual category. Such an assignment of objects and morphisms is called an interpretation of the given signature. More precisely, an interpretation ii of a signature Σ\Sigma in a category C{\bf C} consists of a function i0:Σ0→∣C∣i_{0}:\Sigma_{0}\rightarrow|{\bf C}|, and for any f∈Σ1f\in\Sigma_{1} a morphism i1(f):i0(domf)→i0(codf)i_{1}(f):i_{0}(\mathop{\textrm{\rm dom}}\nolimits f)\rightarrow i_{0}(\mathop{\textrm{\rm cod}}\nolimits f). By a slight abuse of notation, we write i:Σ→Ci:\Sigma\rightarrow{\bf C} for such an interpretation.

Finally, a morphism variable can be viewed as a placeholder for an arbitrary (possibly composite) diagram. We occasionally use this latter view in schematic drawings, such as the schematic representation of t∘st\circ s in Table 1. We then label a box with a morphism term, rather than a formal variable, and understand the box as a short-hand notation for a possibly composite diagram corresponding to that term.

Functors and natural transformations.

Let C{\bf C} and D{\bf D} be categories. A functor F:C→DF:{\bf C}\rightarrow{\bf D} consists of a function F:∣C∣→∣D∣F:|{\bf C}|\rightarrow|{\bf D}|, and for each pair of objects A,B∈∣C∣A,B\in|{\bf C}|, a function F:homC(A,B)→homD(FA,FB)F:\textrm{\rm hom}_{{\bf C}}(A,B)\rightarrow\textrm{\rm hom}_{{\bf D}}(FA,FB), satisfying F(g∘f)=F(g)∘F(f)F(g\circ f)=F(g)\circ F(f) and F(idA)=idFAF(\textrm{\rm id}_{A})=\textrm{\rm id}_{FA}.

Let C{\bf C} and D{\bf D} be categories, and let F,G:C→DF,G:{\bf C}\rightarrow{\bf D} be functors. A natural transformation τ:F→G\tau:F\rightarrow G consists of a family of morphisms τA:FA→GA\tau_{A}:FA\rightarrow GA, one for each object A∈∣C∣A\in|{\bf C}|, such that the following diagram commutes for all f:A→Bf:A\rightarrow B:

Coherence and free categories.

Most coherence theorems are proved by characterizing the free categories of a certain kind.

We say that a category C{\bf C} is free over a signature Σ\Sigma if it is equipped with an interpretation i:Σ→Ci:\Sigma\rightarrow{\bf C}, such that for any category D{\bf D} and interpretation j:Σ→Dj:\Sigma\rightarrow{\bf D}, there exists a unique functor F:C→DF:{\bf C}\rightarrow{\bf D} such that j=F∘ij=F\circ i.

The graphical language of categories over a signature Σ\Sigma, with identities and composition as defined in Table 1, and up to isomorphism of diagrams, forms the free category over Σ\Sigma.

Theorem 2.1 is indeed a consequence of this theorem: by definition of freeness, an equation holds in all categories if and only if it holds in the free category. By the characterization of the free category, an equation holds in the free category if and only if it holds in the graphical language.

Monoidal categories

In this section, we consider various notions of monoidal categories. We sometimes refer to these notions as “progressive”, which means they have graphical languages where all arrows point left-to-right. This serves to distinguish them from “autonomous” notions, which will be discussed in Section 4, and “traced” notions, which will be discussed in Section 5.

A monoidal category (also sometimes called tensor category) is a category with an associative unital tensor product. More specifically:

A monoidal category is a category with the following additional structure:

a new operation A⊗BA\otimes B on objects and a new object constant II;

a new operation on morphisms: if f:A→Cf:A\rightarrow C and g:B→Dg:B\rightarrow D, then

⊗\otimes is a bifunctor, which means idA⊗idB=idA⊗B\textrm{\rm id}_{A}\otimes\textrm{\rm id}_{B}=\textrm{\rm id}_{A\otimes B} and (k⊗h)∘(g⊗f)=(k∘g)⊗(h∘f)(k\otimes h)\circ(g\otimes f)=(k\circ g)\otimes(h\circ f);

α\alpha, λ\lambda, and ρ\rho are natural transformations, i.e., (f⊗(g⊗h))∘αA,B,C=αA′,B′,C′∘((f⊗g)⊗h)(f\otimes(g\otimes h))\circ\alpha_{A,B,C}=\alpha_{A^{\prime},B^{\prime},C^{\prime}}\circ((f\otimes g)\otimes h), f∘λA=λA′∘(idI⊗f)f\circ\lambda_{A}=\lambda_{A^{\prime}}\circ(\textrm{\rm id}_{I}\otimes f), and f∘ρA=ρA′∘(f⊗idI)f\circ\rho_{A}=\rho_{A^{\prime}}\circ(f\otimes\textrm{\rm id}_{I});

plus the following two coherence axioms, called the “pentagon axiom” and the “triangle axiom”:

\scriptstyle{\alpha_{A,B\otimes C,D}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>A</mi><mo>⊗</mo><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>B</mi><mo>⊗</mo><mi>C</mi><mo stretchy="false">)</mo><mo>⊗</mo><mi>D</mi><mo stretchy="false">)</mo><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{A\otimes((B\otimes C)\otimes D)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mopen">((</span><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0715em;">C</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0278em;">D</span><span class="mclose">)</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{A\otimes\alpha_{B,C,D}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mo stretchy="false">(</mo><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>B</mi><mo stretchy="false">)</mo><mo>⊗</mo><mi>C</mi><mo stretchy="false">)</mo><mo>⊗</mo><mi>D</mi><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{((A\otimes B)\otimes C)\otimes D\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mopen">((</span><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0715em;">C</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0278em;">D</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{\alpha_{A,B,C}\otimes D}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><msub><mi>α</mi><mrow><mi>A</mi><mo>⊗</mo><mi>B</mi><mo separator="true">,</mo><mi>C</mi><mo separator="true">,</mo><mi>D</mi></mrow></msub></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{\alpha_{A\otimes B,C,D}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4989em;vertical-align:-0.1975em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0037em;">α</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:-0.0037em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight">A</span><span class="mbin mtight">⊗</span><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight" style="margin-right:0.0715em;">C</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight" style="margin-right:0.0278em;">D</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2822em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{A\otimes(B\otimes(C\otimes D))}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>B</mi><mo stretchy="false">)</mo><mo>⊗</mo><mo stretchy="false">(</mo><mi>C</mi><mo>⊗</mo><mi>D</mi><mo stretchy="false">)</mo><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{(A\otimes B)\otimes(C\otimes D)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mopen">(</span><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.0715em;">C</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0278em;">D</span><span class="mclose">)</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{\alpha_{A,B,C\otimes D}} \textstyle{(A\otimes I)\otimes B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><mrow><msub><mi>ρ</mi><mi>A</mi></msub><mo>⊗</mo><msub><mtext>id</mtext><mi>B</mi></msub></mrow></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{\rho_{A}\otimes\textrm{\rm id}_{B}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6222em;vertical-align:-0.1361em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight">ρ</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight">A</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.1433em;"><span></span></span></span></span></span></span><span class="mbin mtight">⊗</span><span class="mord mtight"><span class="mord text mtight"><span class="mord mtight"><span class="mord mathrm mtight">id</span></span></span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.1433em;"><span></span></span></span></span></span></span></span></span></span></span></span>\scriptstyle{\alpha_{A,I,B}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>A</mi><mo>⊗</mo><mo stretchy="false">(</mo><mi>I</mi><mo>⊗</mo><mi>B</mi><mo stretchy="false">)</mo><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{A\otimes(I\otimes B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.0785em;">I</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mclose">)</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{\textrm{\rm id}_{A}\otimes\lambda_{B}}A⊗B\textstyle{A\otimes B} When we specifically want to emphasize that a monoidal category is not assumed to be braided, symmetric, etc., we sometimes also refer to it as a planar monoidal category.

Examples of monoidal categories include: the category Set (of sets and functions), together with the cartesian product ×\times; the category Set together with the disjoint union operation ++; the category Rel with either ×\times or ++; the category Vect (of vectors spaces and linear functions) with either ⊕\oplus or ⊗\otimes; the category Hilb of Hilbert spaces with either ⊕\oplus or ⊗\otimes; the categories Top and Cob with disjoint union ++. Note that in each case, we need to specify a category and a tensor product (in general there are multiple choices). Technically, we should also specify associativity maps etc., but they are usually clear from the context.

We extend the graphical language of categories as follows. A tensor product of objects is represented by writing the corresponding wires in parallel. The unit object is represented by zero wires. A morphism variable f:A1⊗…⊗An→B1⊗…⊗Bmf:A_{1}\otimes\ldots\otimes A_{n}\rightarrow B_{1}\otimes\ldots\otimes B_{m} is represented as a box with nn input wires and mm output wires. A tensor product of morphisms is represented by stacking the corresponding diagrams. This is shown in Table 2.

Note that it is our convention to write tensor products in the bottom-to-top order. Similar conventions apply to objects as to morphisms: thus, a single wire is labeled by an object variable such as AA, while a more general object such as A⊗BA\otimes B or II is represented by zero or more wires. For more details, see “Monoidal signatures” below.

Coherence.

It is easy to check that the graphical language for monoidal categories is sound, up to deformation of diagrams in the plane. As an example, consider the following law, which is a consequence of bifunctoriality:

Translated into the graphical language, this becomes

which obviously holds up to deformation of diagrams. We have the following coherence theorem:

A well-formed equation between morphism terms in the language of monoidal categories follows from the axioms of monoidal categories if and only if it holds, up to planar isotopy, in the graphical language.

Here, by “planar isotopy”, we mean that two diagrams, drawn in a rectangle in the plane with incoming and outgoing wires attached to the boundaries of the rectangle, are equivalent if it is possible to transform one to the other by continuously moving around boxes in the rectangle, without allowing boxes or wires to cross each other or to be detached from the boundary of the rectangle during the moving. To make these notions mathematically precise, it is usually easier to represent morphism as points, rather than boxes. For precise definitions and a proof of the coherence theorem, see Joyal and Street .

Technically, Joyal and Street’s proof in only applies to planar isotopies where each intermediate diagram during the deformation remains progressive, i.e., with all arrows oriented left-to-right. Joyal and Street call such an isotopy “recumbent”. We conjecture that the result remains true if one allows arbitrary planar deformations. Similar caveats also apply to the coherence theorems for braided and balanced monoidal categories below.

The following is an example of two diagrams that are not isomorphic in the planar embedded sense:

where f:I→A⊗Bf:I\rightarrow A\otimes B, g:A⊗B→Ig:A\otimes B\rightarrow I, and h:I→Ih:I\rightarrow I. And indeed, the corresponding equation g∘((ρA∘(idA⊗h)∘ρA−1)⊗idB)∘f=g∘((λA∘(h⊗idA)∘λA−1)⊗idB)∘fg\circ((\rho_{A}\circ(\textrm{\rm id}_{A}\otimes h)\circ\rho^{-1}_{A})\otimes\textrm{\rm id}_{B})\circ f=g\circ((\lambda_{A}\circ(h\otimes\textrm{\rm id}_{A})\circ\lambda^{-1}_{A})\otimes\textrm{\rm id}_{B})\circ f does not follow from the axioms of monoidal categories. This is an easy consequence of soundness.

Note that because of the coherence theorem, it is not actually necessary to memorize the axioms of monoidal categories: indeed, one could use the coherence theorem as the definition of monoidal category! For practical purposes, reasoning in the graphical language is almost always easier than reasoning from the axioms. On the other hand, the graphical definition is not very useful when one has to check whether a given category is monoidal; in this case, checking finitely many axioms is easier.

Relationship to traditional coherence theorems.

Many category theorists are familiar with coherence theorems of the form “all diagrams of a certain type commute”. Mac Lane’s traditional coherence theorem for monoidal categories is of this form. It states that all diagrams built from only α\alpha, λ\lambda, ρ\rho, id, ∘\circ, and ⊗\otimes commute.

The coherence results in this paper are of a more general form (cf. Kelly [26, p. 107]). Here, the object is to characterize all formal equations that follow from a given set of axioms. We note that the traditional coherence theorem is an easy consequence of the general coherence result of Theorem 3.1: namely, if a given well-formed equation is built only from α\alpha, λ\lambda, ρ\rho, id, ∘\circ, and ⊗\otimes, then both the left-hand side and right-hand side denote identity diagrams in the graphical language. Therefore, by Theorem 3.1, the equation follows from the axioms of monoidal categories. Analogous remarks hold for all the coherence theorems of this article.

Technicalities

To be precise about the labels on diagrams of monoidal categories, and about the meaning of “well-formed equation” in the coherence theorem, we introduce the concept of a monoidal signature. This generalizes the simple signatures introduced in Section 2. Monoidal signatures were introduced under the name tensor schemes by Joyal and Street . We give a non-strict version of the definition.

Given a set Σ0\Sigma_{0} of object variables, let Mon(Σ0)\mathop{\textrm{\rm Mon}}\nolimits(\Sigma_{0}) denote the free (⊗,I)(\otimes,I)-algebra generated by Σ0\Sigma_{0}, i.e., the set of object terms built from object variables and II via the operation ⊗\otimes. For example, if A,B∈Σ0A,B\in\Sigma_{0}, then the term (A⊗B)⊗(I⊗A)(A\otimes B)\otimes(I\otimes A) is an element of Mon(Σ0)\mathop{\textrm{\rm Mon}}\nolimits(\Sigma_{0}).

A monoidal signature consists of a set Σ0\Sigma_{0} of object variables, a set Σ1\Sigma_{1} of morphism variables, and a pair of functions dom,cod:Σ1→Mon(Σ0)\mathop{\textrm{\rm dom}}\nolimits,\mathop{\textrm{\rm cod}}\nolimits:\Sigma_{1}\rightarrow\mathop{\textrm{\rm Mon}}\nolimits(\Sigma_{0}).

The concept of well-formed morphism terms and equations (in the language of monoidal categories) is defined relative to a given monoidal signature. In the graphical language, wires and boxes are labeled by object variables and morphism variables as before. An object term expands to zero or more parallel wires, by the rules of Table 2. As before, the labellings must respect the domain and codomain information, which now involves possibly multiple wires connected to a box. Just as we sometimes label a box by a morphism term in schematic drawings to denote a possibly composite diagram, we sometimes label a wire by an object term, such as SS and TT in Table 2. In this case, it is a short-hand notation for zero or more parallel wires.

Given a monoidal signature Σ\Sigma and a monoidal category C{\bf C}, an interpretation i:Σ→Ci:\Sigma\rightarrow{\bf C} consists of an object function i0:Σ0→∣C∣i_{0}:\Sigma_{0}\rightarrow|{\bf C}|, which then extends in a unique way to i^0:Mon(Σ0)→∣C∣\hat{i}_{0}:\mathop{\textrm{\rm Mon}}\nolimits(\Sigma_{0})\rightarrow|{\bf C}| such that i^0(A⊗B)=i^0(A)⊗i^0(B)\hat{i}_{0}(A\otimes B)=\hat{i}_{0}(A)\otimes\hat{i}_{0}(B) and i^0(I)=I\hat{i}_{0}(I)=I, and for any f∈Σ1f\in\Sigma_{1} a morphism i1(f):i0(domf)→i0(codf)i_{1}(f):i_{0}(\mathop{\textrm{\rm dom}}\nolimits f)\rightarrow i_{0}(\mathop{\textrm{\rm cod}}\nolimits f).

The remaining graphical languages in this Section 3 are all given relative to a monoidal signature.

Monoidal functors and natural transformations.

A strong monoidal functor (also sometimes called a tensor functor) between monoidal categories C{\bf C} and D{\bf D} is a functor F:C→DF:{\bf C}\rightarrow{\bf D}, together with natural isomorphisms ϕ2:FA⊗FB→F(A⊗B)\phi^{2}:FA\otimes FB\rightarrow F(A\otimes B) and ϕ0:I→FI\phi^{0}:I\rightarrow FI, such that the following diagrams commute:

Let C{\bf C} and D{\bf D} be monoidal categories, and let F,G:C→DF,G:{\bf C}\rightarrow{\bf D} be strong monoidal functors. A natural transformation τ:F→G\tau:F\rightarrow G is called monoidal (or a tensor transformation) if the following two diagrams commute for all A,BA,B:

Coherence and free monoidal categories.

Similarly to what we stated for categories, the coherence theorem for monoidal categories is a consequence of a characterization of the free monoidal category. However, due to the extra coherence conditions in the definition of a strong monoidal functor, the definition of freeness is slightly more complicated.

A monoidal category C{\bf C} is a free monoidal category over a monoidal signature Σ\Sigma if it is equipped with an interpretation i:Σ→Ci:\Sigma\rightarrow{\bf C} such that for any monoidal category D{\bf D} and interpretation j:Σ→Dj:\Sigma\rightarrow{\bf D}, there exists a strong monoidal functor F:C→DF:{\bf C}\rightarrow{\bf D} such that j=F∘ij=F\circ i, and FF is unique up to a unique monoidal natural isomorphism.

As before, the coherence theorem can be re-formulated as a freeness theorem.

The graphical language of monoidal categories over a monoidal signature Σ\Sigma, with identities, composition, and tensor as defined in Tables 1 and 2, and up to planar isotopy of diagrams, forms a free monoidal category over Σ\Sigma.

Most of the coherence theorems (and conjectures) of this article can be similarly formulated in terms of freeness. An exception to this are the traced categories without braidings in Sections 5.1–5.4 and 7.5, as explained in Remark 5.4. From now on, we will only mention freeness when it is not entirely automatic, such as in Section 4.1.

2 Spacial monoidal categories

A monoidal category is spacial if it satisfies the additional axiom

In the graphical language, this means that

so in particular, it implies that the two terms in (3.1) are equal. The author does not know whether the concept of a spacial monoidal category appears in the literature, or if it does, under what name.

The graphical language for spacial monoidal categories is the same as that for monoidal categories, except that planarity is dropped from the notion of diagram equivalence, i.e., diagrams are considered up to isomorphism. Obviously the axioms are sound; we conjecture that they are also complete.

A well-formed equation between morphism terms in the language of spacial monoidal categories follows from the axioms of spacial monoidal categories if and only if it holds, up to isomorphism of diagrams, in the graphical language.

Note that, in the case of planar diagrams, the notion of isomorphism of diagrams coincides with ambient isotopy in 3 dimensions. This explains the term “spacial”.

3 Braided monoidal categories

A braiding on a monoidal category is a natural family of isomorphisms cA,B:A⊗B→B⊗Ac_{A,B}:A\otimes B\rightarrow B\otimes A, satisfying the following two “hexagon axioms”:

\scriptstyle{\alpha_{B,A,C}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>B</mi><mo>⊗</mo><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>C</mi><mo stretchy="false">)</mo><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{B\otimes(A\otimes C)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mopen">(</span><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0715em;">C</span><span class="mclose">)</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{\textrm{\rm id}_{B}\otimes c_{A,C}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mo stretchy="false">(</mo><mi>A</mi><mo>⊗</mo><mi>B</mi><mo stretchy="false">)</mo><mo>⊗</mo><mi>C</mi><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{(A\otimes B)\otimes C\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mopen">(</span><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0715em;">C</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{c_{A,B}\otimes\textrm{\rm id}_{C}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><msub><mi>α</mi><mrow><mi>A</mi><mo separator="true">,</mo><mi>B</mi><mo separator="true">,</mo><mi>C</mi></mrow></msub></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{\alpha_{A,B,C}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4989em;vertical-align:-0.1975em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0037em;">α</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:-0.0037em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight">A</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight" style="margin-right:0.0715em;">C</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2822em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{B\otimes(C\otimes A).}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>A</mi><mo>⊗</mo><mo stretchy="false">(</mo><mi>B</mi><mo>⊗</mo><mi>C</mi><mo stretchy="false">)</mo><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{A\otimes(B\otimes C)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0715em;">C</span><span class="mclose">)</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{c_{A,B\otimes C}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mo stretchy="false">(</mo><mi>B</mi><mo>⊗</mo><mi>C</mi><mo stretchy="false">)</mo><mo>⊗</mo><mi>A</mi><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{(B\otimes C)\otimes A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal" style="margin-right:0.0715em;">C</span><span class="mclose">)</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal">A</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{\alpha_{B,C,A}} (B⊗A)⊗C\ignorespaces\ignorespaces\ignorespaces\ignorespaces<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="1"displaystyle="false"><msub><mi>α</mi><mrow><mi>B</mi><moseparator="true">,</mo><mi>A</mi><moseparator="true">,</mo><mi>C</mi></mrow></msub></mstyle></mrow><annotationencoding="application/x−tex">αB,A,C</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.4989em;vertical−align:−0.1975em;"></span><spanclass="mordmtightsizingreset−size6size3"><spanclass="mordmtight"><spanclass="mordmathnormalmtight"style="margin−right:0.0037em;">α</span><spanclass="msupsub"><spanclass="vlist−tvlist−t2"><spanclass="vlist−r"><spanclass="vlist"style="height:0.3448em;"><spanstyle="top:−2.3567em;margin−left:−0.0037em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmathnormalmtight"style="margin−right:0.0502em;">B</span><spanclass="mpunctmtight">,</span><spanclass="mordmathnormalmtight">A</span><spanclass="mpunctmtight">,</span><spanclass="mordmathnormalmtight"style="margin−right:0.0715em;">C</span></span></span></span></span><spanclass="vlist−s">​</span></span><spanclass="vlist−r"><spanclass="vlist"style="height:0.2822em;"><span></span></span></span></span></span></span></span></span></span></span></span>B⊗(A⊗C)\ignorespaces\ignorespaces\ignorespaces\ignorespaces<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="1"displaystyle="false"><mrow><msub><mtext>id</mtext><mi>B</mi></msub><mo>⊗</mo><msubsup><mi>c</mi><mrow><mi>C</mi><moseparator="true">,</mo><mi>A</mi></mrow><mrow><mo>−</mo><mn>1</mn></mrow></msubsup></mrow></mstyle></mrow><annotationencoding="application/x−tex">idB⊗cC,A−1</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.94em;vertical−align:−0.316em;"></span><spanclass="mordmtightsizingreset−size6size3"><spanclass="mordmtight"><spanclass="mordtextmtight"><spanclass="mordmtight"><spanclass="mordmathrmmtight">id</span></span></span><spanclass="msupsub"><spanclass="vlist−tvlist−t2"><spanclass="vlist−r"><spanclass="vlist"style="height:0.3448em;"><spanstyle="top:−2.3567em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmathnormalmtight"style="margin−right:0.0502em;">B</span></span></span></span></span><spanclass="vlist−s">​</span></span><spanclass="vlist−r"><spanclass="vlist"style="height:0.1433em;"><span></span></span></span></span></span></span><spanclass="mbinmtight">⊗</span><spanclass="mordmtight"><spanclass="mordmathnormalmtight">c</span><spanclass="msupsub"><spanclass="vlist−tvlist−t2"><spanclass="vlist−r"><spanclass="vlist"style="height:0.8913em;"><spanstyle="top:−2.1874em;margin−left:0em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmathnormalmtight"style="margin−right:0.0715em;">C</span><spanclass="mpunctmtight">,</span><spanclass="mordmathnormalmtight">A</span></span></span></span><spanstyle="top:−2.931em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmtight">−</span><spanclass="mordmtight">1</span></span></span></span></span><spanclass="vlist−s">​</span></span><spanclass="vlist−r"><spanclass="vlist"style="height:0.4515em;"><span></span></span></span></span></span></span></span></span></span></span></span>(A⊗B)⊗C\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="1"displaystyle="false"><mrow><msubsup><mi>c</mi><mrow><mi>B</mi><moseparator="true">,</mo><mi>A</mi></mrow><mrow><mo>−</mo><mn>1</mn></mrow></msubsup><mo>⊗</mo><msub><mtext>id</mtext><mi>C</mi></msub></mrow></mstyle></mrow><annotationencoding="application/x−tex">cB,A−1⊗idC</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.94em;vertical−align:−0.316em;"></span><spanclass="mordmtightsizingreset−size6size3"><spanclass="mordmtight"><spanclass="mordmathnormalmtight">c</span><spanclass="msupsub"><spanclass="vlist−tvlist−t2"><spanclass="vlist−r"><spanclass="vlist"style="height:0.8913em;"><spanstyle="top:−2.1874em;margin−left:0em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmathnormalmtight"style="margin−right:0.0502em;">B</span><spanclass="mpunctmtight">,</span><spanclass="mordmathnormalmtight">A</span></span></span></span><spanstyle="top:−2.931em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmtight">−</span><spanclass="mordmtight">1</span></span></span></span></span><spanclass="vlist−s">​</span></span><spanclass="vlist−r"><spanclass="vlist"style="height:0.4515em;"><span></span></span></span></span></span></span><spanclass="mbinmtight">⊗</span><spanclass="mordmtight"><spanclass="mordtextmtight"><spanclass="mordmtight"><spanclass="mordmathrmmtight">id</span></span></span><spanclass="msupsub"><spanclass="vlist−tvlist−t2"><spanclass="vlist−r"><spanclass="vlist"style="height:0.3448em;"><spanstyle="top:−2.3567em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmathnormalmtight"style="margin−right:0.0715em;">C</span></span></span></span></span><spanclass="vlist−s">​</span></span><spanclass="vlist−r"><spanclass="vlist"style="height:0.1433em;"><span></span></span></span></span></span></span></span></span></span></span></span>αA,B,C<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="0"displaystyle="false"><mrow><mi>B</mi><mo>⊗</mo><mostretchy="false">(</mo><mi>C</mi><mo>⊗</mo><mi>A</mi><mostretchy="false">)</mo><mimathvariant="normal">.</mi></mrow></mstyle></mrow><annotationencoding="application/x−tex">B⊗(C⊗A).</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:1em;vertical−align:−0.25em;"></span><spanclass="mord"><spanclass="mordmathnormal"style="margin−right:0.0502em;">B</span><spanclass="mspace"style="margin−right:0.2222em;"></span><spanclass="mbin">⊗</span><spanclass="mspace"style="margin−right:0.2222em;"></span><spanclass="mopen">(</span><spanclass="mordmathnormal"style="margin−right:0.0715em;">C</span><spanclass="mspace"style="margin−right:0.2222em;"></span><spanclass="mbin">⊗</span><spanclass="mspace"style="margin−right:0.2222em;"></span><spanclass="mordmathnormal">A</span><spanclass="mclose">)</span><spanclass="mord">.</span></span></span></span></span></span>A⊗(B⊗C)\ignorespaces\ignorespaces\ignorespaces\ignorespaces<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="1"displaystyle="false"><msubsup><mi>c</mi><mrow><mi>B</mi><mo>⊗</mo><mi>C</mi><moseparator="true">,</mo><mi>A</mi></mrow><mrow><mo>−</mo><mn>1</mn></mrow></msubsup></mstyle></mrow><annotationencoding="application/x−tex">cB⊗C,A−1</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.94em;vertical−align:−0.316em;"></span><spanclass="mordmtightsizingreset−size6size3"><spanclass="mordmtight"><spanclass="mordmathnormalmtight">c</span><spanclass="msupsub"><spanclass="vlist−tvlist−t2"><spanclass="vlist−r"><spanclass="vlist"style="height:0.8913em;"><spanstyle="top:−2.1874em;margin−left:0em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmathnormalmtight"style="margin−right:0.0502em;">B</span><spanclass="mbinmtight">⊗</span><spanclass="mordmathnormalmtight"style="margin−right:0.0715em;">C</span><spanclass="mpunctmtight">,</span><spanclass="mordmathnormalmtight">A</span></span></span></span><spanstyle="top:−2.931em;margin−right:0.0714em;"><spanclass="pstrut"style="height:2.5em;"></span><spanclass="sizingreset−size3size1mtight"><spanclass="mordmtight"><spanclass="mordmtight">−</span><spanclass="mordmtight">1</span></span></span></span></span><spanclass="vlist−s">​</span></span><spanclass="vlist−r"><spanclass="vlist"style="height:0.4515em;"><span></span></span></span></span></span></span></span></span></span></span></span>(B⊗C)⊗A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\textstyle{(B\otimes A)\otimes C\ignorespaces\ignorespaces\ignorespaces\ignorespaces}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><msub><mi>α</mi><mrow><mi>B</mi><mo separator="true">,</mo><mi>A</mi><mo separator="true">,</mo><mi>C</mi></mrow></msub></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{\alpha_{B,A,C}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4989em;vertical-align:-0.1975em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0037em;">α</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:-0.0037em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight">A</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight" style="margin-right:0.0715em;">C</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2822em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{B\otimes(A\otimes C)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><mrow><msub><mtext>id</mtext><mi>B</mi></msub><mo>⊗</mo><msubsup><mi>c</mi><mrow><mi>C</mi><mo separator="true">,</mo><mi>A</mi></mrow><mrow><mo>−</mo><mn>1</mn></mrow></msubsup></mrow></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{\textrm{\rm id}_{B}\otimes c^{-1}_{C,A}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.94em;vertical-align:-0.316em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord text mtight"><span class="mord mtight"><span class="mord mathrm mtight">id</span></span></span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.1433em;"><span></span></span></span></span></span></span><span class="mbin mtight">⊗</span><span class="mord mtight"><span class="mord mathnormal mtight">c</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.8913em;"><span style="top:-2.1874em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0715em;">C</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight">A</span></span></span></span><span style="top:-2.931em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mtight">−</span><span class="mord mtight">1</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.4515em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{(A\otimes B)\otimes C\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><mrow><msubsup><mi>c</mi><mrow><mi>B</mi><mo separator="true">,</mo><mi>A</mi></mrow><mrow><mo>−</mo><mn>1</mn></mrow></msubsup><mo>⊗</mo><msub><mtext>id</mtext><mi>C</mi></msub></mrow></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{c^{-1}_{B,A}\otimes\textrm{\rm id}_{C}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.94em;vertical-align:-0.316em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight">c</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.8913em;"><span style="top:-2.1874em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight">A</span></span></span></span><span style="top:-2.931em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mtight">−</span><span class="mord mtight">1</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.4515em;"><span></span></span></span></span></span></span><span class="mbin mtight">⊗</span><span class="mord mtight"><span class="mord text mtight"><span class="mord mtight"><span class="mord mathrm mtight">id</span></span></span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0715em;">C</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.1433em;"><span></span></span></span></span></span></span></span></span></span></span></span>\scriptstyle{\alpha_{A,B,C}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>B</mi><mo>⊗</mo><mo stretchy="false">(</mo><mi>C</mi><mo>⊗</mo><mi>A</mi><mo stretchy="false">)</mo><mi mathvariant="normal">.</mi></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{B\otimes(C\otimes A).}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.0715em;">C</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal">A</span><span class="mclose">)</span><span class="mord">.</span></span></span></span></span></span>\textstyle{A\otimes(B\otimes C)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><msubsup><mi>c</mi><mrow><mi>B</mi><mo>⊗</mo><mi>C</mi><mo separator="true">,</mo><mi>A</mi></mrow><mrow><mo>−</mo><mn>1</mn></mrow></msubsup></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{c^{-1}_{B\otimes C,A}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.94em;vertical-align:-0.316em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight">c</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.8913em;"><span style="top:-2.1874em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span><span class="mbin mtight">⊗</span><span class="mord mathnormal mtight" style="margin-right:0.0715em;">C</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight">A</span></span></span></span><span style="top:-2.931em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mtight">−</span><span class="mord mtight">1</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.4515em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{(B\otimes C)\otimes A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}αB,C,A\scriptstyle{\alpha_{B,C,A}} Note that every braided monoidal category is spacial; this follows from the naturality (in II) of cA,I:A⊗I→I⊗Ac_{A,I}:A\otimes I\rightarrow I\otimes A.

A braided monoidal functor between braided monoidal categories is a monoidal functor that is compatible with the braiding in the following sense:

One extends the graphical language of monoidal categories with the braiding:

In general, if AA and BB are composite object terms, the braiding cA,Bc_{A,B} is represented as the appropriate number of wires crossing each other.

Note that the braiding satisfies cA,B∘cA,B−1=idA⊗Bc_{A,B}\circ c^{-1}_{A,B}=\textrm{\rm id}_{A\otimes B}, but not cA,B∘cB,A=idA⊗Bc_{A,B}\circ c_{B,A}=\textrm{\rm id}_{A\otimes B}. Graphically:

The hexagon axiom translates into the following in the graphical language:

The Yang-Baxter equation is the following equation, which is a consequence of the hexagon axiom and naturality:

A well-formed equation between morphisms in the language of braided monoidal categories follows from the axioms of braided monoidal categories if and only if it holds in the graphical language up to isotopy in 3 dimensions.

Here, by “isotopy in 3 dimensions”, we mean that two diagrams, drawn in a 3-dimensional box with incoming and outgoing wires attached to the boundaries of the box, are isotopic if it is possible to transform one to the other by moving around nodes in the box, without allowing nodes or edges to cross each other or to be detached from the boundary during the moving. Also, the linear order of the edges entering and exiting each node must be respected. This is made more precise in Joyal and Street .

The proof by Joyal and Street is subject to some minor technical assumptions: graphs are assumed to be smooth, and the isotopies are progressive, with continuously changing tangent vectors.

4 Balanced monoidal categories

A twist on a braided monoidal category is a natural family of isomorphisms θA:A→A\theta_{A}:A\rightarrow A, satisfying θI=idI\theta_{I}=\textrm{\rm id}_{I} and such that the following diagram commutes for all A,BA,B:

A balanced monoidal category is a braided monoidal category with twist.

A balanced monoidal functor between balanced monoidal categories is a braided monoidal functor that is also compatible with the twist, i.e., such that F(θA)=θFAF(\theta_{A})=\theta_{FA} for all AA.

The graphical language of balanced monoidal categories is similar to that of braided monoidal categories, except that morphisms are represented by flat ribbons, rather than 1-dimensional wires. A ribbon can be thought of as a pair of parallel wires that are infinitesimally close to each other, or as a wire that is equipped with a framing . For example, the braiding looks like this:

The twist map θA\theta_{A} is represented as a 360-degree twist in a ribbon, or in several ribbons together, if AA is a composite object term. This is easiest seen in the following illustration.

The meaning of (3.3) should then be obvious.

A well-formed equation between morphisms in the language of balanced monoidal categories follows from the axioms of balanced monoidal categories if and only if it holds in the graphical language up to framed isotopy in 3 dimensions.

5 Symmetric monoidal categories

A symmetric monoidal category is a braided monoidal category where the braiding is self-inverse, i.e.:

In this case, the braiding is called a symmetry.

Because of equation (3.3), a symmetric monoidal category can be equivalently defined as a balanced monoidal category in which θA=idA\theta_{A}=\textrm{\rm id}_{A} for all AA.

The previous remark notwithstanding, there exist symmetric monoidal categories that possess a non-trivial twist (in addition to the trivial twist θA=idA\theta_{A}=\textrm{\rm id}_{A}). Thus, in a balanced monoidal category, the symmetry condition cA,B=cB,A−1c_{A,B}=c^{-1}_{B,A} does not in general imply θA=idA\theta_{A}=\textrm{\rm id}_{A}. In other words, a balanced monoidal category that is symmetric as a braided monoidal category is not necessarily symmetric as a balanced monoidal category. An example is the category of finite dimensional vector spaces and linear bijections, with θA(x)=nx\theta_{A}(x)=nx, where n=dim⁡(A)n=\dim(A).

On the monoidal category (Set,×)(\textrm{\bf Set},\times) of sets with cartesian product, a symmetry is given by c(x,y)=(y,x)c(x,y)=(y,x). On the category (Vect,⊗)(\textrm{\bf Vect},\otimes) of vector spaces with tensor product, a symmetry is given by c(x⊗y)=y⊗xc(x\otimes y)=y\otimes x.

The symmetry is graphically represented by a crossing:

A well-formed equation between morphisms in the language of symmetric monoidal categories follows from the axioms of symmetric monoidal categories if and only if it holds, up to isomorphism of diagrams, in the graphical language.

Note that the graphical language for symmetric monoidal categories is up to isomorphism of diagrams, without any reference to 2- or 3-dimensional structure. However, isomorphism of diagrams is equivalent to ambient isotopy in 4 dimensions, so we can still regard it as a geometric notion.

Autonomous categories

Autonomous categories are monoidal categories in which the objects have duals. In terms of graphical language, this means that some wires are allowed to run from right to left.

In a (without loss of generality strict) monoidal category, an exact pairing between two objects AA and BB is given by a pair of morphisms η:I→B⊗A\eta:I\rightarrow B\otimes A and ϵ:A⊗B→I\epsilon:A\otimes B\rightarrow I, such that the following two adjunction triangles commute:

In such an exact pairing, BB is called the right dual of AA and AA is called the left dual of BB.

The maps η\eta and ϵ\epsilon determine each other uniquely, and they are respectively called the unit and the counit of the adjunction. Moreover, the triple (B,η,ϵ)(B,\eta,\epsilon), if it exists, is uniquely determined by AA up to isomorphism. The existence of duals is therefore a property of a monoidal category, rather than an additional structure on it. Moreover, every strong monoidal functor automatically preserves existing duals.

A monoidal category is right autonomous if every object AA has a right dual, which we then denote A∗A^{*}. It is left autonomous if every object AA has a left dual, which we then denote ∗ ⁣A{}^{*}\!A. Finally, the category is autonomous if it is both right and left autonomous.

A [right, left, –] autonomous category is also called [right, left, –] rigid, see e.g. [32, p. 78]. Also, the term “autonomous” is sometimes used in the weaker sense of “monoidal closed”. Although this latter usage is no longer common, it still lives on in the terminology “*-autonomous category” (Barr , see also Section 9).

If we wish to emphasize that an autonomous category is not necessarily symmetric or braided, we sometimes call it a planar autonomous category.

If AA is an object variable, the objects A∗A^{*} and ∗ ⁣A{}^{*}\!A are both represented in the same way: by a wire labeled AA running from right to left. The unit and counit are represented as half turns:

More generally, if AA is a composite object represented by a number of wires, then A∗A^{*} and ∗ ⁣A{}^{*}\!A are represented by the same set of wires running backward (rotated by 180 degrees), and the units and counits are represented as multiple wires turning.

The two diagrams in (4.1), where B=A∗B=A^{*}, translate into the graphical language as follows:

For any morphism f:A→Bf:A\rightarrow B, it is possible to define morphisms f∗:B∗→A∗f^{*}:B^{*}\rightarrow A^{*} and ∗ ⁣f:∗ ⁣B→∗ ⁣A{}^{*}\!f:{}^{*}\!B\rightarrow{}^{*}\!A, called the adjoint mates of ff, as follows:

With these definitions, (−)∗(-)^{*} and ∗ ⁣(−){}^{*}\!(-) become contravariant functors.

A well-formed equation between morphisms in the language of autonomous categories follows from the axioms of autonomous categories if and only if it holds in the graphical language up to planar isotopy.

Here, the notion of planar isotopy is the same as before, except that the wires are of course no longer restricted to being oriented left-to-right during the deformation. However, the ability to turn wires upside down does not extend to boxes: the notion of isotopy for this theorem does not include the ability to rotate boxes. See Joyal and Street for a more precise statement.

The proof by Joyal and Street assumes that the diagrams are piecewise linear.

Note that the same theorem applies to left autonomous, right autonomous, or autonomous categories. Indeed, each individual term in the language of autonomous categories involves only finitely many duals, and thus may be translated into a term of (say) left autonomous categories by replacing each object variable AA by A∗∗∗…∗A^{***\ldots*}, for a sufficiently large, even number of ∗*’s. The resulting term maps to the same diagram.

The same coherence theorem also holds for categories that are only right (or left) autonomous. This is a consequence of the following proposition.

Each right (or left) autonomous category can be fully embedded in an autonomous category.

Let C{\bf C} be a right autonomous category, and consider the strong monoidal functor F:C→CF:{\bf C}\rightarrow{\bf C} given by F(A)=A∗∗F(A)=A^{**}. This functor is full and faithful, and every object in the image of FF has a left dual. Now let C^\hat{\bf C} be the colimit (in the large category of right autonomous categories and strong monoidal functors) of the sequence

Then C^\hat{\bf C} is autonomous, and C{\bf C} is fully and faithfully embedded in C^\hat{\bf C}. The proof for left autonomous categories is analogous. □\Box

A well-formed equation between morphisms in the language of right (left) autonomous categories follows from the axioms of right (left) autonomous categories if and only if it holds in the graphical language up to planar isotopy.

It suffices to show that an equation (in the language of right autonomous categories) holds in all right autonomous categories if and only if it holds in all autonomous categories. The “only if” direction is trivial, since every autonomous category is right autonomous. For the opposite direction, suppose some equation holds in all autonomous categories, and let C{\bf C} be a right autonomous category. Then C{\bf C} can be faithfully embedded in an autonomous category C^\hat{\bf C}. By assumption, the equation holds in C^\hat{\bf C}, and therefore also in C{\bf C}, since the embedding is faithful.□\Box

Technicalities

The diagrams of autonomous categories, and the concept of well-formed equation in the coherence theorem, are defined relative to the notion of an autonomous signature. These were called autonomous tensor schemes by Joyal and Street . We give a non-strict version of the definition.

[21, Def. 2.5] Given a set Σ0\Sigma_{0} of object variables, let Aut(Σ0)\mathop{\textrm{\rm Aut}}\nolimits(\Sigma_{0}) denote the free (⊗,I,∗ ⁣(−),(−)∗)(\otimes,I,{}^{*}\!(-),(-)^{*})-algebra generated by Σ0\Sigma_{0}, i.e., the set of object terms built from object variables and II via the operations ⊗\otimes, ∗ ⁣(−){}^{*}\!(-), and (−)∗)(-)^{*}). For example, if A,B∈Σ0A,B\in\Sigma_{0}, then the term B∗⊗(∗∗I⊗A)∗B^{*}\otimes({}^{**}I\otimes A)^{*} is an element of Aut(Σ0)\mathop{\textrm{\rm Aut}}\nolimits(\Sigma_{0}).

An autonomous signature consists of a set Σ0\Sigma_{0} of object variables, a set Σ1\Sigma_{1} of morphism variables, and a pair of functions dom,cod:Σ1→Aut(Σ0)\mathop{\textrm{\rm dom}}\nolimits,\mathop{\textrm{\rm cod}}\nolimits:\Sigma_{1}\rightarrow\mathop{\textrm{\rm Aut}}\nolimits(\Sigma_{0}).

The concept of a right autonomous signature and left autonomous signature are defined analogously. The remaining graphical languages in this Section 4 are all given relative to an autonomous signature.

Functors and natural transformations of autonomous categories.

Any strong monoidal functor preserves exact pairings: if η:I→B⊗A\eta:I\rightarrow B\otimes A and ϵ:A⊗B→I\epsilon:A\otimes B\rightarrow I define an exact pairing, then so do

In particular, if C{\bf C} and D{\bf D} are autonomous categories and F:C→DF:{\bf C}\rightarrow{\bf D} is a monoidal functor, by uniqueness of duals, there will be a unique induced natural isomorphism F(A∗)≅(FA)∗F(A^{*})\cong(FA)^{*} such that

\scriptstyle{\textrm{\rm id}\otimes{\cong}}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><mrow><mover accent="true"><mi>F</mi><mo>^</mo></mover><msub><mi>ϵ</mi><mi>A</mi></msub></mrow></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{\hat{F}\epsilon_{A}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.763em;vertical-align:-0.1003em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord accent mtight"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.9468em;"><span style="top:-2.7em;"><span class="pstrut" style="height:2.7em;"></span><span class="mord mathnormal mtight" style="margin-right:0.1389em;">F</span></span><span style="top:-2.9523em;"><span class="pstrut" style="height:2.7em;"></span><span class="accent-body" style="left:-0.1667em;"><span class="mord mtight">^</span></span></span></span></span></span></span><span class="mord mtight"><span class="mord mathnormal mtight">ϵ</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight">A</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.1433em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{I,}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>F</mi><mi>A</mi><mo>⊗</mo><mo stretchy="false">(</mo><mi>F</mi><mi>A</mi><msup><mo stretchy="false">)</mo><mo lspace="0em" rspace="0em">∗</mo></msup><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{FA\otimes(FA)^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.1389em;">F</span><span class="mord mathnormal">A</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mopen">(</span><span class="mord mathnormal" style="margin-right:0.1389em;">F</span><span class="mord mathnormal">A</span><span class="mclose"><span class="mclose">)</span><span class="msupsub"><span class="vlist-t"><span class="vlist-r"><span class="vlist" style="height:0.6887em;"><span style="top:-3.063em;margin-right:0.05em;"><span class="pstrut" style="height:2.7em;"></span><span class="sizing reset-size6 size3 mtight"><span class="mord mtight"><span class="mord mtight">∗</span></span></span></span></span></span></span></span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{\epsilon_{FA}} and similarly for F(∗ ⁣A)≅∗ ⁣(FA)F({}^{*}\!A)\cong{}^{*}\!(FA).

For natural transformations, we have the following lemma:

Suppose τ:F→G\tau:F\rightarrow G is a monoidal natural transformation between strong monoidal functors F,G:C→DF,G:{\bf C}\rightarrow{\bf D}. If AA has a right dual A∗A^{*} in C{\bf C}, then τA∗\tau_{A^{*}} and (τA)∗(\tau_{A})^{*} are mutually inverse in D{\bf D} (up to the above canonical isomorphism), or more precisely:

In particular, if C{\bf C} is autonomous, then any such monoidal natural transformation is invertible.

Coherence and free autonomous categories.

The graphical language, as we have defined it above for autonomous categories, is sufficient for the purposes of Theorem 4.5. However, it does not characterize the free autonomous category over an autonomous signature as stated. For example, consider a signature with a single morphism variable f:A→Af:A\rightarrow A. The problem is that there are clearly some diagrams, such as

which are not translations of any well-formed term of autonomous categories. Indeed, for this diagram to correspond to a well-formed term, we would have to have e.g. f:A∗∗→Af:A^{**}\rightarrow A or f:A→∗∗Af:A\rightarrow{}^{**}A.

Joyal and Street characterize the free autonomous category by equipping each edge with a winding number. Effectively, the horizontal segments of edges are labeled with pairs (A,n)(A,n), where AA is an object variables and nn is an integer winding number. Left-to-right segments have even winding numbers, right-to-left segments have odd winding numbers, and winding numbers increase by one on counterclockwise turns, and decrease by one on clockwise turns. The winding numbers on the input and output of each box, and on the global inputs and outputs, are restricted to be consistent with the domain and codomain information, where e.g. A∗∗A^{**} corresponds to (A,2)(A,2), and ∗∗∗B{}^{***}B to (B,−3)(B,-3). See for precise details. Here is an example of a well-formed diagram of type I→B∗∗⊗AI\rightarrow B^{**}\otimes A, where g:I→A⊗Bg:I\rightarrow A\otimes B:

The graphical language (with winding numbers) of autonomous categories over an autonomous signature Σ\Sigma, up to planar isotopy of diagrams, forms a free autonomous category over Σ\Sigma.

We remark that if a diagram of planar autonomous categories can be labeled with winding numbers, then this labeling is necessarily unique. In particular, for the purposes of Theorem 4.5, there is no harm in dropping the winding numbers, because by hypothesis, the theorem only considers diagrams that are the translation of well-formed terms, whose winding numbers can therefore uniquely reconstructed.

2 (Planar) pivotal categories

A pivotal category is an autonomous category with a suitable isomorphism A≅A∗∗A\cong A^{**}.

A pivotal category is a right autonomous category equipped with a monoidal natural isomorphism iA:A→A∗∗i_{A}:A\rightarrow A^{**}.

Note that any pivotal category is immediately left autonomous, therefore autonomous. The requirement that iAi_{A} is a monoidal natural transformation here means that iIi_{I} is the canonical isomorphism I≅I∗∗I\cong I^{**}, and that the following diagram commutes, where the horizontal arrow is the canonical isomorphism derived from the autonomous structure:

The following property, which is sometimes taken as part of the definition of pivotal categories [19, Def. 3.1.1], is a direct consequence of Saavedra Rivano’s Lemma (Lemma 4.9).

In any pivotal category, the following diagram commutes:

One can equivalently define a pivotal category as an autonomous category equipped with a monoidal natural isomorphism (of contravariant monoidal functors) ϕ:A∗→≅∗ ⁣A\phi:A^{*}\xrightarrow{\cong}{}^{*}\!A. This was done by Freyd and Yetter . Condition (S) of [16, Def. 4.1] is also a consequence of Saavedra Rivano’s Lemma, and is therefore redundant.

Freyd and Yetter also introduced the term sovereign category for a pivotal category.

A pivotal functor between pivotal categories is a monoidal functor that also satisfies

The graphical language for pivotal categories is the same as that for autonomous categories, where the isomorphism iA:A→A∗∗i_{A}:A\rightarrow A^{**} is represented like an identity map. Of course, there are now additional diagrams that are the translation of well-formed terms. For example, when f:A→Af:A\rightarrow A, then (4.2) is a well-formed diagram of pivotal categories, but not of autonomous categories. Indeed, in the case of pivotal categories, the problem of winding numbers (discussed before Theorem 4.10) disappears, as winding numbers are taken modulo 2, and hence add nothing beyond orientation.

A well-formed equation between morphisms in the language of pivotal categories follows from the axioms of pivotal categories if and only if it holds in the graphical language up to planar isotopy, including rotation of boxes.

Only special cases of this theorem have been proved in the literature. Freyd and Yetter [16, Thm. 4.4] considered the case of the free pivotal category generated by a category. In our terminology, this means that they only considered diagrams for pivotal categories over simple signatures, rather than over autonomous signatures. In other words, they only considered boxes of the form

with exactly one input and one output. Joyal and Street’s draft report claims the general result but contains no proof.

The notion of planar isotopy for pivotal categories includes the ability to rotate boxes in the plane of the diagram. For example, the following two diagrams are isotopic in this sense:

This also explains why we have marked a corner of each box. With the ability to rotate boxes, we need to keep track of their “natural” orientation, so that the diagrams from (4.4) can also be represented like this:

f\textstyle{f} More generally, the adjoint mate of f:A→Bf:A\rightarrow B can be represented by a rotated box:

Also note that is ff is a composite diagram, then the whole diagram may be rotated to obtain f∗f^{*}.

3 Spherical pivotal categories

A pivotal category is spherical if for all objects AA and morphisms f:A→Af:A\rightarrow A,

The intuition behind the “spherical” axioms is that diagrams should be embedded in a 2-sphere, rather than the plane. It is then obvious that the left-hand side of (4.6) can be continuously transformed into the right-hand side, namely by moving the loop across the back of the 2-sphere.

The spherical axiom is not sound for the graphical language of diagrams embedded in the 2-sphere. The problem is that the notion of “diagram embedded in the 2-sphere” is not compatible with composition or tensor. The following is a consequence of the spherical axiom, but does not hold up to isotopy in the 2-sphere.

Note that this counterexample is similar to the spacial axiom (3.2), but does not quite imply it. If one adds the spacial axiom, as we are about to do, then any notion of isotopy is lost and equivalence of diagrams collapses to isomorphism.

4 Spacial pivotal categories

A pivotal category is spacial if it satisfies the spacial axiom (3.2) and the spherical axiom (4.6).

The graphical language for spacial pivotal categories is the same as that for planar pivotal categories, except that equivalence of diagrams is now taken up to isomorphism. Clearly, the axioms are sound for the graphical language. We conjecture that they are also complete.

A well-formed equation between morphisms in the language of spacial pivotal categories follows from the axioms of spacial pivotal categories if and only if it holds in the graphical language up to isomorphism.

5 Braided autonomous categories

An braided autonomous category is an autonomous category that is also braided (as a monoidal category). The notion of braided autonomous categories is not extremely natural, as the graphical language is only sound for a restricted form of isotopy called regular isotopy. Nevertheless, it is useful to collect some facts about braided autonomous categories.

A braided monoidal category is autonomous if and only if it is right autonomous.

If η:I→B⊗A\eta:I\rightarrow B\otimes A and ϵ:A⊗B→I\epsilon:A\otimes B\rightarrow I form an exact pairing, then so do cA,B−1∘η:I→A⊗Bc^{-1}_{A,B}\circ\eta:I\rightarrow A\otimes B and ϵ∘cB,A:B⊗A→I\epsilon\circ c_{B,A}:B\otimes A\rightarrow I. Therefore any right dual of AA is also a left dual of AA. □\Box

In any braided autonomous category C{\bf C}, we can define a natural isomorphism bA:A∗∗→Ab_{A}:A^{**}\rightarrow A. This follows from the proof of Lemma 4.17, using the fact that both AA and A∗∗A^{**} are right duals of A∗A^{*}. More concretely, bAb_{A} and its inverse are defined by:

Here we have written, without loss of generality, as if C{\bf C} were strict monoidal. Graphically, bAb_{A} and its inverse look like this:

The graphical language braided autonomous categories is obtained simply by adding braids to the graphical language of autonomous categories. However, the correct notion of equivalence of diagrams is neither planar isotopy (like for autonomous categories), nor 3-dimensional isotopy (like for braided monoidal categories), but an in-between notion called regular isotopy .

It is well-known that 3-dimensional isotopy of links and tangles is equivalent to planar isotopy of their (non-degenerate) projections onto a 2-dimensional plane, plus the three Reidemeister moves shown as (R1)–(R3) in Figure 3. To extend this to diagrams with nodes, one also has to add the moves (Λ\Lambda1) and (Λ\Lambda2).

Regular isotopy is defined to be the equivalence obtained by dropping Reidemeister move (R1). Note that regular isotopy is an equivalence on 2-dimensional representation of 3-dimensional diagrams (and not of 3-dimensional diagrams themselves).

A well-formed equation between morphisms in the language of braided autonomous categories follows from the axioms of braided autonomous categories if and only if it holds in the graphical language up to regular isotopy.

Only special cases of this theorem have been proved in the literature. Freyd and Yetter [16, Thm. 3.8] proved this only for diagrams over a simple signature.

6 Braided pivotal categories

Let C{\bf C} be a braided autonomous category. Then giving a twist θA:A→A\theta_{A}:A\rightarrow A on C{\bf C} (making C{\bf C} into a balanced category) is equivalent to giving a pivotal structure iA:A→A∗∗i_{A}:A\rightarrow A^{**} (making C{\bf C} into a pivotal category).

The lemma is remarkable because the concept of a braided autonomous category does not include any assumption relating the braided structure to the autonomous structure. Moreover, the axioms for a twist depend only on the braided structure, whereas the axioms for a pivotal structure depend only on the autonomous structure. Yet, they are equivalent if C{\bf C} is braided autonomous.

Proof of Lemma 4.20: Recall the natural isomorphism bA:A∗∗→Ab_{A}:A^{**}\rightarrow A that was defined in Section 4.5 for any braided autonomous category. Given a twist θA:A→A\theta_{A}:A\rightarrow A, we define a pivotal structure by

Conversely, given a pivotal structure iA:A→A∗∗i_{A}:A\rightarrow A^{**}, we define a twist by

The two constructions are clearly each other’s inverse. To verify their properties, it is obvious that iAi_{A} is a natural isomorphism if and only if θA\theta_{A} is a natural isomorphism. Moreover, θI=id\theta_{I}=\textrm{\rm id} iff iI=bI−1i_{I}=b^{-1}_{I}, and bI−1b^{-1}_{I} is the canonical isomorphism I≅I∗∗I\cong I^{**}. What remains to be shown is that θ\theta satisfies equation (3.3) if and only if ii satisfies equation (4.3). However, this is a direct consequence of the following fact about bb, which is easily verified:

\scriptstyle{\cong}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><msub><mi>c</mi><mrow><mi>A</mi><mo separator="true">,</mo><mi>B</mi></mrow></msub></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{c_{A,B}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4989em;vertical-align:-0.1975em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight">c</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight">A</span><span class="mpunct mtight">,</span><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2822em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{B^{**}\otimes A^{**}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><mrow><msub><mi>b</mi><mi>B</mi></msub><mo>⊗</mo><msub><mi>b</mi><mi>A</mi></msub></mrow></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{b_{B}\otimes b_{A}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.5864em;vertical-align:-0.1003em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight">b</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.1433em;"><span></span></span></span></span></span></span><span class="mbin mtight">⊗</span><span class="mord mtight"><span class="mord mathnormal mtight">b</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight">A</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.1433em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{(A\otimes B)^{**}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><msub><mi>b</mi><mrow><mi>A</mi><mo>⊗</mo><mi>B</mi></mrow></msub></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{b_{A\otimes B}}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6281em;vertical-align:-0.142em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mtight"><span class="mord mathnormal mtight">b</span><span class="msupsub"><span class="vlist-t vlist-t2"><span class="vlist-r"><span class="vlist" style="height:0.3448em;"><span style="top:-2.3567em;margin-left:0em;margin-right:0.0714em;"><span class="pstrut" style="height:2.5em;"></span><span class="sizing reset-size3 size1 mtight"><span class="mord mtight"><span class="mord mathnormal mtight">A</span><span class="mbin mtight">⊗</span><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span></span></span></span></span><span class="vlist-s">​</span></span><span class="vlist-r"><span class="vlist" style="height:0.2028em;"><span></span></span></span></span></span></span></span></span></span></span></span>\textstyle{A\otimes B}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mrow><mi>B</mi><mo>⊗</mo><mi>A</mi><mi mathvariant="normal">.</mi><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle><mstyle mathcolor="#cc0000"><mtext>\ignorespaces</mtext></mstyle></mrow></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{B\otimes A.\ignorespaces\ignorespaces\ignorespaces\ignorespaces}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:1em;vertical-align:-0.25em;"></span><span class="mord"><span class="mord mathnormal" style="margin-right:0.0502em;">B</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mbin">⊗</span><span class="mspace" style="margin-right:0.2222em;"></span><span class="mord mathnormal">A</span><span class="mord">.</span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span><span class="mord text" style="color:#cc0000;"><span class="mord" style="color:#cc0000;">\ignorespaces</span></span></span></span></span></span></span>\scriptstyle{c_{B,A}} □\Box

A braided pivotal category is the same thing as a balanced autonomous category. □\Box

While Lemma 4.20 establishes a one-to-one correspondence between twists and pivotal structures, the correspondence is not canonical. Indeed, instead of (4.7) and (4.8), we could have equally well used

In fact, there are a countable number of such similar one-to-one correspondences, all induced by the existence of a monoidal natural transformation bA′−1∘iA∘bA∘iA:A→Ab^{\prime}_{A}{}^{-1}\circ i_{A}\circ b_{A}\circ i_{A}:A\rightarrow A. They all coincide if and only if the category is tortile, as discussed in the next section.

The graphical language for braided pivotal categories is the same as the graphical language for pivotal categories, with the addition of braids. Equivalence of diagrams is up to regular isotopy, just as for braided autonomous categories (see Section 4.5).

A well-formed equation between morphisms in the language of braided pivotal categories follows from the axioms of braided pivotal categories if and only if it holds in the graphical language up to regular isotopy.

Only special cases of this theorem have been proved in the literature. Freyd and Yetter [16, Thm. 4.4] proved this only for diagrams over a simple signature.

holds up to regular isotopy, as it can be proved using only the Reidemeister moves (R2) and (R3). It is therefore valid in braided pivotal categories (or even braided autonomous categories). On the other hand, the equation

holds up to isotopy, but not up to regular isotopy (because regular isotopy preserves total curvature, as pointed out by Freyd and Yetter [15, p. 169]). It is therefore not valid in braided pivotal categories. The use of regular isotopy does not seem natural, and this is precisely the reason why Joyal and Street introduced tortile categories, which we discuss in the next section.

A braided pivotal category is not in general spherical (and therefore also not spacial). Indeed, instead of the spherical axiom (4.6), only the following holds up to regular isotopy:

Along with Remark 4.22, this is further evidence that braided pivotal categories (and braided autonomous categories) are not “natural” notions.

7 Tortile categories

Consider a braided pivotal category, which is equivalently balanced autonomous via (4.7) and (4.8). For any object AA the following are equivalent:

(ϵA∗⊗idA)∘(idA∗⊗cA∗∗,A−1)∘(ηA⊗idA∗∗)∘iA∘(ϵA∗⊗idA)∘(idA∗⊗cA,A∗∗)∘(ηA⊗idA∗∗)∘iA=idA,(\epsilon_{A^{*}}\otimes\textrm{\rm id}_{A})\circ(\textrm{\rm id}_{A^{*}}\otimes c^{-1}_{A^{**},A})\circ(\eta_{A}\otimes\textrm{\rm id}_{A^{**}})\circ i_{A}\circ(\epsilon_{A^{*}}\otimes\textrm{\rm id}_{A})\circ(\textrm{\rm id}_{A^{*}}\otimes c_{A,A^{**}})\circ(\eta_{A}\otimes\textrm{\rm id}_{A^{**}})\circ i_{A}=\textrm{\rm id}_{A}, or graphically:

The proof is a straightforward calculation, but it is best explained by the fact that the following hold in the graphical language:

Therefore, the equation (b) is equivalent to

The condition in Lemma 4.27(a) holds if and only if the two definitions of θA\theta_{A} from (4.8) and (4.10) coincide.

A tortile category is a braided pivotal category satisfying the condition of Lemma 4.27(a). Equivalently, a tortile category is a balanced autonomous category satisfying the condition of Lemma 4.27(b).

A tortile category is also sometimes called a ribbon category, see e.g. .

The graphical language for tortile categories is like the graphical language for braided pivotal categories, except that morphisms are represented by ribbons, rather than wires. These ribbons are just like the ones for balanced categories from Section 3.4. Units and counits are represented in the obvious way, for example

The twist map θA:A→A\theta_{A}:A\rightarrow A can be represented in several equivalent ways:

Note that these diagrams are equivalent up to framed 3-dimensional isotopy, and define the same morphism in a tortile category. (On the other hand, in a mere braided pivotal category, the latter two diagrams are not equal). Also note that the map bAb_{A} from Section 4.5 is also represented in the graphical language as

but this is of type bA:A∗∗→Ab_{A}:A^{**}\rightarrow A, whereas θA:A→A\theta_{A}:A\rightarrow A. They differ, of course, only by an invisible pivotal map iA:A→A∗∗i_{A}:A\rightarrow A^{**}.

A well-formed equation between morphisms in the language of tortile categories follows from the axioms of tortile categories if and only if it holds in the graphical language up to framed 3-dimensional isotopy.

Only special cases of this theorem have been proved in the literature. Shum [34, Thm. 6.1] proved it for the case of the free tortile category generated by a category, i.e., for diagrams over a simple signature only.

8 Compact closed categories

A compact closed category is a tortile category that is symmetric (as a balanced monoidal category) in the sense of Section 3.5. Equivalently, because of Remark 3.10, a compact closed category is a tortile category in which θA=idA\theta_{A}=\textrm{\rm id}_{A} for all AA.

The definition can be simplified. Notice that a right autonomous symmetric monoidal category is automatically autonomous (by Lemma 4.17), balanced (with θA=idA\theta_{A}=\textrm{\rm id}_{A}) and therefore pivotal (by Lemma 4.20). Moreover, it is tortile (because θA∗=(θA)∗=idA∗\theta_{A^{*}}=(\theta_{A})^{*}=\textrm{\rm id}_{A^{*}}). We can therefore define:

A compact closed category is a right autonomous symmetric monoidal category.

By analogy with Remark 3.11, it is possible for a compact closed category to possess a non-trivial twist (with the associated non-trivial pivotal structure), in addition to the trivial twist θA=idA\theta_{A}=\textrm{\rm id}_{A}, making it into a tortile category. In other words, for a given tortile category, the symmetry condition cA,B=cB,A−1c_{A,B}=c^{-1}_{B,A} does not in general imply θA=idA\theta_{A}=\textrm{\rm id}_{A}. However, it does imply θA2=idA\theta_{A}^{2}=\textrm{\rm id}_{A}, as the following argument shows:

To construct an example where θ≠id\theta\neq\textrm{\rm id}, consider the category C{\bf C} of finite-dimensional real vector spaces and linear functions. Define an equivalence relation on objects by A∼BA\sim B iff dim⁡(A⊗B)\dim(A\otimes B) is a square. Then define a subcategory C∼{\bf C}_{\sim} by

where pip_{i} is the iith prime number. Finally, define the twist map θA\theta_{A} as multiplication by the scalar ϕ(dim⁡(A))\phi(\dim(A)), or as idA\textrm{\rm id}_{A} if AA is 0-dimensional. With this twist, C∼{\bf C}_{\sim} is tortile. In fact, this shows that there exists a continuum of possible twists on C∼{\bf C}_{\sim}.

The monoidal category (Rel,×)(\textrm{\bf Rel},\times) is compact closed with A∗=AA^{*}=A. The category (FdVect,⊗)(\textrm{\bf FdVect},\otimes) of finite dimensional vectors spaces is compact closed with A∗A^{*} the dual space of AA, and similarly for the category of finite dimensional Hilbert spaces (FdHilb,⊗)(\textrm{\bf FdHilb},\otimes). The corresponding categories of possibly infinite dimensional spaces are not autonomous. (Cob,+)(\textrm{\bf Cob},+) is compact closed with A∗A^{*} equal to AA with reversed orientation.

The graphical language for compact closed categories is like that of tortile categories, except that we remove the framing and twist maps, and use symmetries instead of braidings.

A well-formed equation between morphisms in the language of compact closed categories follows from the axioms of compact closed categories if and only if it holds, up to isomorphism of diagrams, in the graphical language.

The special case of diagrams over a simple signature was proven by Kelly and Laplaza [27, Thm. 8.2]. The general case does not appear in the literature.

Traced categories

The graphical languages considered in Section 3 were progressive, which means that all wires were oriented left-to-right. By contrast, the graphical languages of autonomous categories in Section 4 allow wires to be oriented left-to-right or right-to-left. We now turn out attention to an intermediate notion, namely traced categories.

Like autonomous graphical languages, traced graphical languages permit loops, but with a restriction: all wires must be directed left-to-right at their endpoints. In other words, traced diagrams are like autonomous diagrams, but are taken relative to a monoidal signature (see Section 3.1), rather than an autonomous signature (see Section 4.1). Table 4 shows a typical example of a traced diagram, and a typical example of an autonomous diagram that is not a traced diagram.

Logically, we should have considered traced categories before pivotal categories, because traced categories have less structure than pivotal categories (i.e., every pivotal category is traced, and not the other way around). However, many of the coherence theorems of this section are consequences of the corresponding theorems for pivotal categories, and therefore it made sense to present the pivotal notions first.

Symmetric traced categories and their graphical language (in the strict monoidal case, and with one additional axiom) were first introduced in the 1980’s by Ştefănescu and Căzănescu under the name “biflow” . Joyal, Street, and Verity later rediscovered this notion independently, generalized it to balanced monoidal categories, and proved the fundamental embedding theorem relating balanced traced categories to tortile categories .

Joyal, Street, and Verity use the term traced monoidal category. However, I prefer traced category, usually prefixed by an adjective such as planar, spacial, balanced, symmetric. The word “monoidal” is redundant, because one cannot have a traced structure without a monoidal structure. Also, by putting the adjective before the word “traced”, rather than after it, we make it clear that the traced structure, and not just the underlying monoidal structure, if being modified.

A right trace on a monoidal category is a family of operations

satisfying the following four axioms. For notational convenience, we assume without loss of generality that the monoidal structure is strict.

Tightening (naturality in A,BA,B): TrRX((g⊗idX)∘f∘(h⊗idX))=g∘(TrRXf)∘h\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}((g\otimes\textrm{\rm id}_{X})\circ f\circ(h\otimes\textrm{\rm id}_{X}))=g\circ(\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}f)\circ h;

Sliding (dinaturality in XX): TrRY(f∘(idA⊗g))=TrRX((idB⊗g)∘f)\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{Y}(f\circ(\textrm{\rm id}_{A}\otimes g))=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}((\textrm{\rm id}_{B}\otimes g)\circ f), where f:A⊗X→B⊗Yf:A\otimes X\rightarrow B\otimes Y and g:Y→Xg:Y\rightarrow X;

Vanishing: TrRIf=f\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{I}f=f and TrRX⊗Yf=TrRX(TrRY(f))\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X\otimes Y}f=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}(\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{Y}(f));

Strength. TrRX(g⊗f)=g⊗TrRXf\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}(g\otimes f)=g\otimes\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}f.

A (planar) right traced category is a monoidal category equipped with a right trace.

These axioms are similar to those of Joyal, Street, and Verity , except that we have omitted the yanking axioms which does not apply in the planar case, and we have replaced the non-planar “superposing” axiom by the planar “strength” axiom. I do not know whether this set of planar axioms appears in the literature.

The right trace of a diagram f:A⊗X→B⊗Xf:A\otimes X\rightarrow B\otimes X is graphically represented by drawing a loop from the output XX to the input XX, as follows:

Note that in the graphical language of right traced categories, parts of wires can be oriented right-to-left, but each wire must be oriented left-to-right near the endpoints. The four axioms of right traced categories are illustrated in the graphical language in Table 5.

The axioms of right traced categories are obviously sound for the graphical language, up to planar isotopy. We conjecture that they are also complete.

A well-formed equation between morphism terms in the language of right traced categories follows from the axioms of right traced categories if and only if it holds in the graphical language up planar isotopy.

This is a weak conjecture, in the sense that there is not much empirical evidence to support it, nor is there an obvious strategy for a proof. If this conjecture turns out to be false, the axioms for right traced categories should be amended until it becomes true.

The concept of a left trace is defined similarly as a family of operations

satisfying symmetric axioms. A left trace is graphically depicted as follows:

We say that a monoidal functor FF preserves right traces if F(TrRXf)=TrRFX((ϕ2)−1∘Ff∘ϕ2)F(\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}f)=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{FX}((\phi^{2})^{-1}\circ Ff\circ\phi^{2}), and similarly for left traces.

2 Planar traced categories

A planar traced category is a monoidal category equipped with a right trace and a left trace, such that the two traces satisfy three additional axioms:

Interchange: TrRX(TrLYf)=TrLY(TrRXf)\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}(\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm L}}^{Y}f)=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm L}}^{Y}(\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}f), for all f:Y⊗A⊗X→Y⊗B⊗Xf:Y\otimes A\otimes X\rightarrow Y\otimes B\otimes X;

Left pivoting: TrRB(idB⊗f)=TrLA(f⊗idA)\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{B}(\textrm{\rm id}_{B}\otimes f)=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm L}}^{A}(f\otimes\textrm{\rm id}_{A}), for all f:I→A⊗Bf:I\rightarrow A\otimes B;

Right pivoting: TrRB(idB⊗f)=TrLA(f⊗idA)\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{B}(\textrm{\rm id}_{B}\otimes f)=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm L}}^{A}(f\otimes\textrm{\rm id}_{A}), for all f:A⊗B→If:A\otimes B\rightarrow I.

The graphical language of planar traced categories consists of diagrams using the left and right trace together, modulo planar isotopy. The axioms of interchange, left pivoting, and right pivoting are shown graphically in Table 6. Compare also equation (4.4) on page 4.4.

The axioms are clearly sound; we conjecture that they are also complete:

A well-formed equation between morphism terms in the language of planar traced categories follows from the axioms of planar traced categories if and only if it holds in the graphical language up planar isotopy.

As for right traced categories, this conjecture is weak. If it turns out to be false, then one should amend the axioms of planar traced categories accordingly.

Even if the conjecture is true, the graphical language does not in itself give an easy description of the free planar traced category. This is because there are diagrams, such as the following, that “look” planar traced, but are not actually the diagram of any planar traced term (not even up to planar isotopy).

It is not obvious how to characterize the “planar traced” diagrams intrinsically, or how to extend the notion of planar traced categories to encompass all such diagrams.

An autonomous category is not necessarily traced. However, every pivotal category is planar traced with the obvious definitions of left and right trace:

In the graphical language, this looks just like the diagrams (5.1) and (5.2). As a consequence, each diagram of planar traced categories can be regarded as a diagram of planar pivotal categories, but not the other way around.

3 Spherical traced categories

The concept of a spherical traced category is analogous to that of spherical pivotal categories from Section 4.3.

A planar traced category satisfies the spherical axiom if for all f:A→Af:A\rightarrow A,

or equivalently, in the graphical language:

A spherical traced category is a planar traced category satisfying the spherical axiom.

Every spherical pivotal category is spherical traced.

Just like for spherical pivotal categories, the graphical language of spherical traced categories is not coherent for any geometrically useful notion of equivalence of diagrams.

4 Spacial traced categories

A spacial traced category is a planar traced category if it satisfies the spacial axiom (3.2) and the spherical axiom (5.3).

The graphical language for spacial traced categories is the same as that for planar traced categories, except that equivalence of diagrams is now taken up to isomorphism.

A well-formed equation between morphism terms in the language of spacial traced categories follows from the axioms of spacial traced categories if and only if it holds, up to isomorphism of diagrams, in the graphical language.

Every spacial pivotal category is clearly spacial traced. I do not know whether conversely every spacial traced category can be faithfully embedded in a spacial pivotal category. If this is true, then Conjecture 5.6 follows from Conjecture 4.16.

5 Braided traced categories

Braided traced categories, like braided pivotal categories, are a somewhat unnatural notion, because coherence is only satisfied up to regular isotopy. (If one considers full isotopy, one obtains the more natural notion of balanced traced categories, which we will consider in the next section). Nevertheless, we include this section on braided traced categories, not least because it is the first traced notion for which we can actually prove a coherence theorem (modulo Caveat 4.24).

A braided traced category is a planar traced category with a braiding (as a monoidal category), such that

The axiom (5.4) does not follow from the remaining axioms.

In the presence of the remaining axioms, (5.4) is equivalent to

In the presence of the remaining axioms of braided traced categories, the left and right pivoting axioms are redundant.

(a) To see this, consider morphism terms in the language of braided traced categories with one object generator and no morphism generators. Define the degree of a term to the be tensor product of all traced-out objects, i.e., deg⁡(id)=I\deg(\textrm{\rm id})=I, deg⁡(f∘g)=deg⁡(f)⊗deg⁡(g)\deg(f\circ g)=\deg(f)\otimes\deg(g), deg⁡(TrRXf)=X⊗deg⁡(f)\deg(\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{X}f)=X\otimes\deg(f), etc. This is well-defined up to isomorphism. All the axioms of planar traced categories and braided categories respect degree; the only axioms where the left-hand side and right-hand side could potentially have different degree are sliding in Table 5 and pivoting in Table 6. However, in the absence of morphism generators, it is easy to show that all morphism terms are of the form f:A→Bf:A\rightarrow B where A≅BA\cong B. Therefore, neither sliding nor pivoting change the degree (the latter because it is vacuous). Therefore degree is an invariant. On the other hand, (5.4) is not degree-preserving; therefore it cannot follow from the other axioms.

(b) The following graphical proof sketch can be turned into an algebraic proof:

(c) Here is a proof sketch for the left pivoting axiom. Notably, the second to last step uses dinaturality (sliding).

Each braided traced category possesses a balanced structure (as a braided monoidal category) given by θA=TrLAcA,A−1\theta_{A}=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm L}}^{A}c^{-1}_{A,A}, with inverse θA−1=TrRAcA,A\theta^{-1}_{A}=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{A}c_{A,A} (cf. (5.4)). However, this twist is not canonical; for example, another twist can be defined by θA′=TrRAcA,A\theta^{\prime}_{A}=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm R}}^{A}c_{A,A} with inverse θA′−1=TrLAcA,A−1\theta^{\prime}_{A}{}^{-1}=\mathop{\textrm{\rm Tr}}\nolimits_{\textrm{\rm L}}^{A}c^{-1}_{A,A} (cf. (5.5)). In fact, there are countably many other possible twists. This is entirely analogous to Remark 4.22. The various twists coincide if and only if the yanking equation (5.6) holds, yielding a balanced traced category as discussed in Section 5.6 below.

We note that every braided pivotal category is braided traced, with the traced structure as given in Remark 5.5. Moreover, there is an embedding theorem giving a partial converse:

Every braided traced category C{\bf C} can by fully and faithfully embedded into a braided pivotal category Int(C)\mathop{\textrm{\rm Int}}({\bf C}), via a braided traced functor.

The proof exactly mimics the Int-construction of Joyal, Street, and Verity , except that we must replace the twist by , and be careful only to use the braided traced axioms. We omit the details, which are both lengthy and tedious.□\Box

A braided traced category is not necessarily spherical (and therefore not spacial). This is analogous to Remark 4.26.

The graphical language for braided traced categories is obtained by adding braids to the graphical language of planar traced categories. Equivalence of diagrams is up to regular isotopy (see Section 4.5).

A well-formed equation between morphisms in the language of braided traced categories follows from the axioms of braided traced categories if and only if it holds in the graphical language up to regular isotopy.

Soundness is easy to check by inspection of the axioms. Completeness is a consequence of Theorems 4.23 and 5.10. Namely, consider an equation in the language of braided traced categories that holds in the graphical language up to regular isotopy. The diagrams corresponding to the left-hand side and right-hand side of the equation can also be regarded as diagrams of braided pivotal categories, and since they are regularly isotopic, the equation holds in all braided pivotal categories by Theorem 4.23. Since any braided traced category C{\bf C} can be faithfully embedded in a braided pivotal category Int(C)\mathop{\textrm{\rm Int}}({\bf C}) by Theorem 5.10, an equation that holds in Int(C)\mathop{\textrm{\rm Int}}({\bf C}) must also hold in C{\bf C}. It follows that the equation in question holds in all braided traced categories C{\bf C}, and therefore, it is a consequence of the axioms.□\Box

Because of the dependence on Theorem 4.23, Caveat 4.24 also applies here.

6 Balanced traced categories

A balanced traced category is a balanced monoidal category equipped with a right trace Tr\mathop{\textrm{\rm Tr}}\nolimits, and satisfying the following yanking axioms:

The graphical language of balanced traced categories combines the ribbons and twists of balanced categories with the loops of traced categories. The trace is represented as expected:

Note that there is no need to postulate a left trace, because a left trace is definable from the right trace and braidings as follows:

The defined left trace automatically satisfies interchange and the pivoting axioms (Table 6), as well as the spherical axiom (5.3) and the braided traced axiom (5.4). The spacial axiom (3.2) is satisfied by any braided monoidal category. Therefore, any balanced traced category is spacial traced and braided traced.

The graphical validity of the yanking axiom is easily verified using a shoe string:

Every tortile category is balanced traced, with the traced structure as given in Remark 5.5. Moreover, there is an embedding theorem:

Every balanced traced category can be fully and faithfully embedded into a tortile category, via a balanced traced functor.

A well-formed equation between morphisms in the language of balanced traced categories follows from the axioms of balanced traced categories if and only if it holds in the graphical language up to framed isotopy in 3 dimensions.

This follows from Theorems 4.30 and 5.15, by the exact same argument that was used in the proof of Theorem 5.12.□\Box

Because of the dependence on Theorem 4.30, Caveat 4.31 also applies here.

In any braided monoidal category with a right trace, the twist and its inverse are definable by equation (5.6). These maps are automatically natural and satisfy θI=idI\theta_{I}=\textrm{\rm id}_{I} and (3.3). However, they are not automatically inverse to each other. Therefore, a balanced traced category could be equivalently defined as a braided monoidal category with a right trace, satisfying

7 Symmetric traced categories

A symmetric traced category is a symmetric monoidal category with a right trace Tr\mathop{\textrm{\rm Tr}}\nolimits, satisfying the symmetric yanking axiom:

Because of Remark 3.10, a symmetric traced category can be equivalently defined as a balanced traced category in which θA=idA\theta_{A}=\textrm{\rm id}_{A} for all AA.

Obviously every compact closed category is symmetric traced with the structure from Remark 5.5. Here, too, we have an embedding theorem:

Every symmetric traced category can be fully and faithfully embedded into a compact closed category, via a symmetric traced functor.

Consider the category Rel of sets and relations, with biproducts given by disjoint union A+BA+B. Given a relation R:A+X→B+XR:A+X\rightarrow B+X, define its trace TrX(R):A→B\mathop{\textrm{\rm Tr}}\nolimits^{X}(R):A\rightarrow B by (a,b)∈TrX(R)(a,b)\in\mathop{\textrm{\rm Tr}}\nolimits^{X}(R) iff there exists n≥0n\geq 0 and x1,…,xn∈Xx_{1},\ldots,x_{n}\in X such that a R x1 R x2 R … R xn R ba\,R\,x_{1}\,R\,x_{2}\,R\,\ldots\,R\,x_{n}\,R\,b. This defines a symmetric traced category which is not compact closed.

The graphical language is like that of planar traced categories, combined with the symmetry. A typical diagram looks like this:

The notion of equivalence of diagrams is isomorphism.

A well-formed equation between morphisms in the language of symmetric traced categories follows from the axioms of symmetric traced categories if and only if it holds in the graphical language up to isomorphism of diagrams.

A consequence of Theorems 4.33 and 5.20, as in Theorems 5.12 and 5.16.

Because of the dependence on Theorem 4.33, Caveat 4.34 also applies here.

Strict symmetric traced categories, with the additional axiom

first appear in the work of Ştefănescu under the name “biflow”. A precursor of the definition appears in , and the axioms were given their modern form by Căzănescu and Ştefănescu . The paper also contains a detailed proof sketch of coherence, namely, that the graphical language, modulo isomorphism and the equation (5.7), forms the free biflow over a monoidal signature. This proof sketch remains valid with respect to the modern definition, provided that one assumes coherence for symmetric monoidal categories.

Products, coproducts, and biproducts

In this section, we consider graphical languages for monoidal categories where the monoidal structure is given by a categorical product, coproduct, or biproduct. The main difference with the graphical languages of “purely” monoidal categories from Sections 3–5 is that equivalence of diagrams must now be defined up to diagrammatic equations.

In a category, a product of objects AA and BB is given by an object A×BA\times B, together with morphisms π1:A×B→A\pi_{1}:A\times B\rightarrow A and π2:A×B→B\pi_{2}:A\times B\rightarrow B, such that for all objects CC and pairs of morphisms f:C→Af:C\rightarrow A and g:C→Bg:C\rightarrow B, there exists a unique morphism h:C→A⊗Bh:C\rightarrow A\otimes B such that the following diagram commutes:

The unique morphism hh is often written as h=⟨f,g⟩h=\langle f,g\rangle. An object II is terminal if for all objects CC, there exists a unique morphism h:C→Ih:C\rightarrow I. A finite product category (or cartesian category) is a category with a chosen terminal object, and a chosen product for each pair of objects.

Equivalently, a finite product category can be described as a symmetric monoidal category, together with natural families of copy and erase maps

subject to a number of axioms, shown in Table 7.

We extend the graphical language of symmetric monoidal categories by adding the following representations of the copy and erase maps.

A<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="0"displaystyle="false"><molspace="0em"rspace="0em">∙</mo></mstyle></mrow><annotationencoding="application/x−tex">∙</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.4445em;"></span><spanclass="mord"><spanclass="mord">∙</span></span></span></span></span></span>A\textstyle{A}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mo lspace="0em" rspace="0em">∙</mo></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{\bullet}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4445em;"></span><span class="mord"><span class="mord">∙</span></span></span></span></span></span>\textstyle{A}A\textstyle{A} Erase ◊A:A→I\Diamond_{A}:A\rightarrow I A\textstyle{A}∙\textstyle{\bullet} As usual, if AA is a composite object term, a wire labeled AA should be replaced by multiple parallel wires. Table 8 contains graphical representations of some of the axioms for finite product categories.

Note that the projections π1:A×B→A\pi_{1}:A\times B\rightarrow A and π2:A×B→B\pi_{2}:A\times B\rightarrow B, and the pairing h:C→A⊗Bh:C\rightarrow A\otimes B of f:C→Af:C\rightarrow A and g:C→Bg:C\rightarrow B, are represented graphically as follows:

Coherence.

As the equivalences in Table 8 demonstrate, coherence in the graphical language of finite product categories does not hold up to isomorphism or isotopy of diagrams. Rather, is holds up to manipulations of diagrams. So unlike the graphical languages considered in Sections 2–5, we now have to consider axioms on diagrams.

A well-formed equation between morphism terms in the language of finite product categories follows from the axioms of finite product categories if and only if it holds in the graphical language, up to isomorphism of diagrams and the diagrammatic manipulations shown in Table 8.

This theorem is a simple consequence of coherence for symmetric monoidal categories (Theorem 3.12), together with the fact that all the axioms of finite product categories, except those shown in Table 8, hold up to isomorphism of diagrams.

2 Coproducts

The definition of coproducts and initial objects is dual to that of products and terminal objects, i.e., it is obtained by reversing all the arrows in Section 6.1. Explicitly, an object is initial if for all objects CC, there exists a unique morphism h:0→Ch:0\rightarrow C. A coproduct of objects A,BA,B is given by an object A+BA+B, together with morphisms ι1:A→A+B\iota_{1}:A\rightarrow A+B and ι2:B→A+B\iota_{2}:B\rightarrow A+B, such that for all objects CC and pairs of morphisms f:A→Cf:A\rightarrow C and g:B→Cg:B\rightarrow C, there exists a unique morphism h:A+B→Ch:A+B\rightarrow C such that h∘ι1=fh\circ\iota_{1}=f and h∘ι2=gh\circ\iota_{2}=g. One often writes h=[f,g]h=[f,g]. A category with finite coproducts is also called a co-cartesian category.

Dualizing the presentation of Section 6.1, one can equivalently define a finite coproduct category as a symmetric monoidal category with natural families of merge and initial maps

satisfying the duals of the axioms in Table 7.

The graphical language of finite coproduct categories is obtained by dualizing that of finite product categories, with the duals of the axioms from Table 8.

3 Biproducts

An object is called a zero object if it is initial and terminal. If 0{\bf 0} is a zero object, then there is a distinguished map A→0→BA\rightarrow{\bf 0}\rightarrow B between any two objects, denoted 0A,B0_{A,B}. A biproduct of objects A1A_{1} and A2A_{2} is given by an object A1⊕A2A_{1}\oplus A_{2}, together with morphisms ιi:Ai→A1⊕A2\iota_{i}:A_{i}\rightarrow A_{1}\oplus A_{2} and πi:A1⊕A2→Ai\pi_{i}:A_{1}\oplus A_{2}\rightarrow A_{i}, for i=1,2i=1,2, such that A⊕BA\oplus B is a product with π1,π2\pi_{1},\pi_{2}, a coproduct with ι1,ι2\iota_{1},\iota_{2} and such that πi∘ιj=δij\pi_{i}\circ\iota_{j}=\delta_{ij}. Here δii=idAi\delta_{ii}=\textrm{\rm id}_{A_{i}} and δij=0Aj,Ai\delta_{ij}=0_{A_{j},A_{i}} when i≠ji\neq j. We say that C{\bf C} is a biproduct category if it has a chosen zero object 0{\bf 0} and a chosen biproduct for any pair of objects.

The axiom πi∘ιj=δij\pi_{i}\circ\iota_{j}=\delta_{ij} is equivalent to the assertion that the symmetric monoidal structure defined by ⊕\oplus “as a product” coincides with the symmetric monoidal structure defined by ⊕\oplus “as a coproduct”. Therefore, a biproduct category is symmetric monoidal in a canonical way.

Equivalently, a biproduct category can be defined as a symmetric monoidal category, together with natural families of morphisms

satisfying the axioms in Table 7, as well as their duals.

The graphical language of biproducts is obtained by combining the graphical languages for products and coproducts. In this case, one has the equalities in Table 9, which are consequences of the naturality axioms in Table 8. Note that the axiom πi∘ιj=δij\pi_{i}\circ\iota_{j}=\delta_{ij} holds automatically in the graphical language.

A well-formed equation between morphism terms in the language of biproduct categories follows from the axioms of biproduct categories if and only if it holds in the graphical language, up to isomorphism of diagrams, the diagrammatic manipulations shown in Table 8, and their duals.

This theorem is a simple consequence of coherence for symmetric monoidal categories, together with the fact that the axioms in Table 8 (and their duals) are exactly the graphical representations of the axioms in Table 7 (and their duals) that do not already hold up to graphical isomorphism.

4 Traced product, coproduct, and biproduct categories

It potentially makes sense to revisit each of the notions of Sections 3–5 and consider the case where the monoidal structure is given by a product, coproduct, or biproduct. Since products, coproducts, and biproducts are automatically symmetric, we do not need to consider the weaker notions (such as balanced, braided, etc).

Moreover, we do not need to consider any autonomous cases, because an autonomous category where the tensor is given by a product (or coproduct) is trivial. Indeed, for any objects A,BA,B, the morphisms f:A→Bf:A\rightarrow B are in one-to-one correspondence with morphism A⊗B∗→IA\otimes B^{*}\rightarrow I. Since II is terminal, there is exactly one such morphism, and therefore there is a unique morphism between any two objects. Such a category is equivalent to the one-object one-morphism category.

Therefore, the only new notion from Sections 3–5 that admits non-trivial examples in the context of products, coproducts, or biproducts is that of a symmetric traced category.

A traced product [coproduct, biproduct] category is a symmetric traced category where the tensor is given by a categorical product [coproduct, biproduct].

The symmetric traced category (Rel,+)(\textrm{\bf Rel},+) from Example 5.21 is a traced biproduct category.

Consider the category Set⊥\textrm{\bf Set}_{\bot} whose objects are sets, and whose morphisms are partial functions, regarded as a subcategory of Rel from Example 6.4. In this category, the empty set is a zero object, and the disjoint union operation A+BA+B defines a coproduct (but not a product). Trace is given as in Example 6.4. With these definitions, Set⊥\textrm{\bf Set}_{\bot} is a traced coproduct category.

As expected, the graphical language of traced product [coproduct, biproduct] categories is given by adding a trace (as in Section 5) to the graphical language of finite product [finite coproduct, biproduct] categories.

A well-formed equation between morphism terms in the language of traced product [coproduct, biproduct] categories follows from the respective axioms if and only if it holds in the graphical language, up to isomorphism of diagrams, and the diagrammatic manipulations shown in Table 8 and/or their duals (as appropriate).

In computer science, traces arise naturally in the context of data flow (as fixed points), and in the context of control flow (as iteration). The two situations correspond to traced product categories and traced coproduct categories, respectively. The duality between data flow and control flow was first described by Bainbridge . The following are typical examples of a data flow diagram (on the left) and a control flow diagram (on the right). The data flow diagram represents the fixed point expression y=(3+x)(x+y)y=(3+x)(x+y), parametric on an input xx. The control flow diagram represents a generic “while loop”. Note that data flow diagrams have a notion of “copying” data, whereas control flow diagrams have a dual notion of “merging” control paths.

In a category with finite coproducts, giving a trace is equivalent to giving an iteration operator. Here, an iteration operator is a family of operations

natural in AA and dinatural in XX, satisfying

Iteration: iter(f)=[idA,iter(f)]∘f\mathop{\textrm{\rm iter}}\nolimits(f)=[\textrm{\rm id}_{A},\mathop{\textrm{\rm iter}}\nolimits(f)]\circ f, for all f:X→A+Xf:X\rightarrow A+X;

Diagonal property: iter(iter(f))=iter((idA+[idX,idX])∘f)\mathop{\textrm{\rm iter}}\nolimits(\mathop{\textrm{\rm iter}}\nolimits(f))=\mathop{\textrm{\rm iter}}\nolimits((\textrm{\rm id}_{A}+[\textrm{\rm id}_{X},\textrm{\rm id}_{X}])\circ f), for all f:X→A+X+Xf:X\rightarrow A+X+X.

Dually, on a finite product category, giving a trace is equivalent to a fixed point operator fixX:hom(A×X,X)→hom(A,X)\mathop{\textrm{\rm fix}}\nolimits^{X}:\textrm{\rm hom}(A\times X,X)\rightarrow\textrm{\rm hom}(A,X).

This makes precise the intuitive idea that in the presence of coproducts, the while loop in Remark 6.7 is sufficient for constructing arbitrary traces.

In the presence of the other axioms, the diagonal property is equivalent to the so-called Bekič Lemma:

for all f:X→A+X+Yf:X\rightarrow A+X+Y and g:Y→A+X+Yg:Y\rightarrow A+X+Y [36, Prop. B.1].

Iteration operators in the sense of Proposition 6.8 were first defined, using different but equivalent axioms, by Căzănescu and Ungureanu , under the name “algebraic theory with iterate”.

In a category with finite biproducts, giving a trace is equivalent to giving a repetition operation, i.e., a family of operators

Here, f+gf+g denotes the morphism ∇A∘(f⊕g)∘ΔA:A→A\nabla_{A}\circ(f\oplus g)\circ\Delta_{A}:A\rightarrow A, for f,g:A→Af,g:A\rightarrow A.

5 Uniformity and regular trees

Suppose we are given a traced category with a distinguished subclass of morphisms called the strict morphisms. Then the trace is called uniform if for all f:A⊗X→B⊗Xf:A\otimes X\rightarrow B\otimes X, g:A⊗Y→B⊗Yg:A\otimes Y\rightarrow B\otimes Y, and strict h:X→Yh:X\rightarrow Y, the following implication holds:

whenever hh is strict. Note that uniformity is not an equational property.

A traced coproduct category is uniformly traced if and only if for all f:X→A+Xf:X\rightarrow A+X, g:Y→A+Yg:Y\rightarrow A+Y, and strict h:X→Yh:X\rightarrow Y,

Moreover, a traced biproduct category is uniformly traced if and only if for all f:X→Xf:X\rightarrow X, g:Y→Yg:Y\rightarrow Y, and strict h:X→Yh:X\rightarrow Y,

In the particular case where the class of strict morphisms is taken to be the smallest co-cartesian subcategory containing all objects, Ştefănescu proved that the free uniformly traced coproduct category over a monoidal signature is given by the graphical language of traced coproduct categories, modulo a suitable notion of simulation equivalence on diagrams. This simulation equivalence is easiest to describe in the case where all morphism variables are of input arity 1. In this case, two diagrams are simulation equivalent if and only if they have the same infinite tree unwinding. There is also an analogous result for biproducts. We refer the reader to for full details.

The following is an example of an equation that holds up to infinite tree unwinding, but fails in general traced coproduct categories:

Ésik’s “iteration theories” are a direct equational axiomatization of such infinite tree unwindings. They include an iteration operator as in Proposition 6.8, but with an infinite family of additional properties, such as (6.1).

6 Cartesian center

Sometimes it is useful to consider notions that are weaker than product categories, yet still have copy and erase maps ΔA:A→A⊗A\Delta_{A}:A\rightarrow A\otimes A and ◊A:A→I\Diamond_{A}:A\rightarrow I. For example, it is common to drop the naturality axioms, while retaining the commutative comonoid and coherence axioms (see Tables 7 and 8). An equivalent way to describe such a category is as a symmetric monoidal category with (faithful) cartesian center , i.e., a symmetric monoidal category with a symmetric monoidal subcategory that contains all the objects and is cartesian. Similar ideas have occurred, with varying degrees of explicitness, in the literature on flowcharts, see e.g. .

Similarly, if one omits naturality from the axioms for coproducts, one obtains categories with a co-cartesian center. A weakened version of biproducts is obtained by combining the axioms of cartesian center and co-cartesian center. In this case, one requires the operations Δ\Delta, ◊\Diamond, ∇\nabla, □\Box to be natural with respect to one another, yielding the properties from Table 9. More generally, one may require any subset of the operations Δ\Delta, ◊\Diamond, ∇\nabla, □\Box to exist, and a further subset to be natural transformations. As the reader may imagine, this leads to a nearly endless number of categorical notions and corresponding graphical languages; see e.g. .

Dagger categories

The concept of a dagger category (also called involutive category or *-category in the literature) is motivated by the category of Hilbert spaces, where each morphism f:A→Bf:A\rightarrow B has an adjoint f†:B→Af^{\dagger}:B\rightarrow A.

A dagger category is a category C{\bf C} together with an involutive, identity-on-objects, contravariant functor †:C→C\dagger:{\bf C}\rightarrow{\bf C}.

Concretely, this means that to every morphism f:A→Bf:A\rightarrow B, one associates a morphism f†:B→Af^{\dagger}:B\rightarrow A, called the adjoint of ff, such that for all f:A→Bf:A\rightarrow B and g:B→Cg:B\rightarrow C:

The category Hilb of Hilbert spaces and bounded linear maps is a dagger category, where f†:B→Af^{\dagger}:B\rightarrow A is given by the usual adjointness property of linear algebra, i.e., ⟨f†x∣y⟩=⟨x∣fy⟩\langle f^{\dagger}x\mathrel{|}y\rangle=\langle x\mathrel{|}fy\rangle for all x∈Bx\in B and y∈Ay\in A.

(Unitary map, self-adjoint map) In a dagger category, a morphism f:A→Bf:A\rightarrow B is called unitary if it is an isomorphism and f−1=f†f^{-1}=f^{\dagger}. A morphism f:A→Af:A\rightarrow A is called self-adjoint or hermitian if f=f†f=f^{\dagger}.

A dagger functor between dagger categories is a functor that satisfies F(f†)=(Ff)†F(f^{\dagger})=(Ff)^{\dagger} for all ff.

The graphical language of dagger categories extends that of categories. The adjoint of a morphism variable f:A→Bf:A\rightarrow B is represented diagrammatically as follows:

More generally, the adjoint of any diagram is its mirror image. Note that the mirror image of a box is visually distinguishable because we have marked the upper left corner of each box representing a morphism variable. Also note that, while we have taken the mirror image of each box, we have reversed the location, but not the direction, of the wires. Contrast this with (4.5).

A well-formed equation between two morphism terms in the language of dagger categories follows from the axioms of dagger categories if and only if it holds in the graphical language up to isomorphism of diagrams.

This is a consequence of coherence for categories, from Theorem 2.1. As usual, soundness is easy to check. For completeness, notice that any morphism term tt of dagger categories can be transformed, via the axioms (g∘f)†=f†∘g†(g\circ f)^{\dagger}=f^{\dagger}\circ g^{\dagger}, id†=id\textrm{\rm id}^{\dagger}=\textrm{\rm id}, and f††=ff^{\dagger\dagger}=f, into an equivalent term t′t^{\prime} with the property that †\dagger is only applied to morphism variables in t′t^{\prime}. Such a term can be regarded as a term in the language of categories, over the extended set of morphism variables {f,f†,…}\{f,f^{\dagger},\ldots\}. Now if tt and ss are two terms that have isomorphic diagrams, then by soundness, t′t^{\prime} and s′s^{\prime} have isomorphic diagrams. By Theorem 2.1, t′t^{\prime} and s′s^{\prime} are provably equal from the axioms of categories. Therefore tt and ss are provably equal from the axioms of dagger categories.□\Box

We now consider “dagger notions” for the various monoidal categories from Sections 3–5.

1 Dagger monoidal categories

A dagger monoidal category is a monoidal category that is a dagger category, such that the dagger structure is compatible with the monoidal structure in the following sense:

(f⊗g)†=f†⊗g†(f\otimes g)^{\dagger}=f^{\dagger}\otimes g^{\dagger}, for all f,gf,g;

the canonical isomorphisms of the monoidal structure, αA,B,C:(A⊗B)⊗C→A⊗(B⊗C)\alpha_{A,B,C}:(A\otimes B)\otimes C\rightarrow A\otimes(B\otimes C), λA:I⊗A→A\lambda_{A}:I\otimes A\rightarrow A, and ρA:A⊗I→A\rho_{A}:A\otimes I\rightarrow A, are unitary.

The graphical language of dagger monoidal categories is like the graphical language of monoidal categories, with the adjoint of a diagram given by its mirror image. For example,

A well-formed equation between morphism terms in the language of dagger monoidal categories follows from the axioms of dagger monoidal categories if and only if it holds, up to planar isotopy, in the graphical language.

This is a consequence of coherence for planar monoidal categories, from Theorem 3.1. The proof is analogous to that of Theorem 7.2. Note that the axioms of dagger monoidal categories are precisely what is needed to ensure that all occurrences of †\dagger can be removed from a morphism term, except where applied directly to a morphism variable.□\Box

2 Other progressive dagger monoidal notions

We can now “daggerize” the other progressive monoidal notions from Section 3:

A dagger monoidal category is spacial if it is spacial as a monoidal category.

A dagger braided monoidal category is a dagger monoidal category with a unitary braiding cA,B:A⊗B→B⊗Ac_{A,B}:A\otimes B\rightarrow B\otimes A.

A dagger balanced monoidal category is a dagger braided monoidal category with a unitary twist θA:A→A\theta_{A}:A\rightarrow A.

A dagger symmetric monoidal category is a dagger braided monoidal category such that the unitary braiding is a symmetry.

In each case, the graphical language extends the corresponding language from Section 3, with the dagger of a diagram taken to be its mirror image. Each notion has a coherence theorem, proved by the same method as Theorems 7.2 and 7.3. The requirements that the braiding and twist are unitary ensures that the dagger can be removed from the corresponding terms. The respective caveats from Section 3 also apply to the dagger cases.

The category Hilb of Hilbert spaces is dagger symmetric monoidal, with the usual tensor product and symmetry.

3 Dagger pivotal categories

In defining dagger variants of the notions of Section 4, we find that the notion of a dagger autonomous category and a dagger pivotal category coincide. This is because the presence of a dagger structure on an autonomous category already induces a canonical isomorphism A≅A∗∗A\cong A^{**}, which automatically satisfies the pivotal axioms under mild assumptions.

To be more precise, consider a dagger monoidal category that is also right autonomous (as a monoidal category). Because ηA:I→A∗⊗A\eta_{A}:I\rightarrow A^{*}\otimes A has an adjoint ηA†:A∗⊗A→I\eta^{\dagger}_{A}:A^{*}\otimes A\rightarrow I, we can define a family of isomorphisms

We can represent this schematically as follows (but bearing in mind that we do not yet have a formal graphical language to work with):

The following are equivalent in a right autonomous, dagger monoidal category:

the family of isomorphisms iA:A→A∗∗i_{A}:A\rightarrow A^{**}, as defined above, determines a pivotal structure;

for all A,BA,B, the canonical isomorphisms (A⊗B)∗≅B∗⊗A∗(A\otimes B)^{*}\cong B^{*}\otimes A^{*} and I∗≅II^{*}\cong I (determined by the right autonomous structure) are unitary, and for all f:A→Bf:A\rightarrow B, the equation f∗†=f†∗f^{*\dagger}=f^{\dagger*} holds.

By a direct calculation from the definitions, one can check three separate and independent facts:

For any given f:A→Bf:A\rightarrow B, the diagram

commutes if and only if f∗†=f†∗f^{*\dagger}=f^{\dagger*}. In particular, the family iAi_{A} is a natural transformation if and only if this condition holds for all ff.

commutes if and only if the canonical isomorphism (A⊗B)∗≅B∗⊗A∗(A\otimes B)^{*}\cong B^{*}\otimes A^{*} is unitary.

The morphism iI:I→I∗∗i_{I}:I\rightarrow I^{**} is equal to the canonical isomorphism (from the right autonomous structure) if and only if the canonical isomorphism I→I∗I\rightarrow I^{*} is unitary.

Since the three conditions are the defining conditions for a pivotal structure, the lemma follows. □\Box

Under the equivalent conditions of Lemma 7.5, the following hold:

iA=A→≅A⊗I→idA⊗ϵA∗†A⊗A∗⊗A∗∗→ϵA⊗idA∗∗I⊗A∗∗→≅A∗∗i_{A}=A\xrightarrow{\cong}A\otimes I\xrightarrow{\textrm{\rm id}_{A}\otimes\epsilon^{\dagger}_{A^{*}}}A\otimes A^{*}\otimes A^{**}\xrightarrow{\epsilon_{A}\otimes\textrm{\rm id}_{A^{**}}}I\otimes A^{**}\xrightarrow{\cong}A^{**}:

ηA†=ϵA∗∘(idA∗⊗iA)\eta^{\dagger}_{A}=\epsilon_{A^{*}}\circ(\textrm{\rm id}_{A^{*}}\otimes i_{A}):

ϵA†=(iA−1⊗idA∗)∘ηA∗\epsilon^{\dagger}_{A}=(i^{-1}_{A}\otimes\textrm{\rm id}_{A^{*}})\circ\eta_{A^{*}}:

But this is just the definition of iA∗i_{A^{*}}, therefore (iA)†∗=iA∗(i_{A})^{\dagger*}=i_{A^{*}}. By definition, iAi_{A} is unitary iff (iA)†=iA−1(i_{A})^{\dagger}=i_{A}^{-1}, iff (iA)†∗=(iA−1)∗(i_{A})^{\dagger*}=(i_{A}^{-1})^{*}, iff iA∗=(iA−1)∗=(iA∗)−1i_{A^{*}}=(i_{A}^{-1})^{*}=(i_{A}^{*})^{-1}. Since ii is a monoidal natural transformation, this holds by Saavedra Rivano’s Lemma (Lemma 4.9).

To prove (b), note that the right-hand side is the inverse of (iA)†(i_{A})^{\dagger}. Therefore, (b) is equivalent to (a).

Finally, equations (c) and (d) are restatements of the definition of iAi_{A} from (7.1). □\Box

The equivalence between (a) and (b) in Lemma 7.6 holds only if iAi_{A} is defined as in (7.1). It does not hold for an arbitrary pivotal structure on a right autonomous dagger monoidal category.

Armed with these results, we finally state the two equivalent definitions of a dagger pivotal category:

A dagger pivotal category is defined in one of the following equivalent ways:

as a dagger monoidal, right autonomous category such that the natural isomorphisms (A⊗B)∗≅B∗⊗A∗(A\otimes B)^{*}\cong B^{*}\otimes A^{*} and I∗≅II^{*}\cong I (from the right autonomous structure) are unitary, and such that f∗†=f†∗f^{*\dagger}=f^{\dagger*} holds for all morphisms ff; or

as a pivotal, dagger monoidal category satisfying the condition in Lemma 7.6(c) (or equivalently, (d)).

The first form of this definition is much easier to check in practice. The second form is more suitable for the proof of the coherence theorem below.

In a dagger pivotal category, the operation (−)∗(-)^{*} arises from an adjunction (in the categorical sense) of objects, with associated unit, counit, and adjoint mates. On the other hand, the operation (−)†(-)^{\dagger} arises from an adjunction (in the linear algebra sense) of morphisms. The two concepts should not be confused with each other.

The graphical language of dagger pivotal categories is like that of pivotal categories, where the adjoint of a diagram is given, as usual, by its mirror image. For example:

Note that in the graphical language, adjoint mates f∗:B∗→A∗f^{*}:B^{*}\rightarrow A^{*} are represented by rotation and adjoints f†:B→Af^{\dagger}:B\rightarrow A by mirror image. Therefore, each morphism variable f:A→Bf:A\rightarrow B induces four kinds of boxes:

Also note that, unlike the informal notation used above, the graphical language does not explicitly display the isomorphism iA:A→A∗∗i_{A}:A\rightarrow A^{**}, and it does not explicitly distinguish ηA:I→A∗⊗A\eta_{A}:I\rightarrow A^{*}\otimes A from ϵA∗†:I→A∗⊗A∗∗\epsilon^{\dagger}_{A^{*}}:I\rightarrow A^{*}\otimes A^{**}. This is justified by the following coherence theorem.

A well-formed equation between morphisms in the language of dagger pivotal categories follows from the axioms of dagger pivotal categories if and only if it holds in the graphical language up to planar isotopy, including rotation of boxes (by multiples of 180 degrees).

This follows from coherence of pivotal categories (Theorem 4.14), by the same argument used in the proof of Theorem 7.3. The equations from Lemma 7.6(c) and (d), and the fact that iAi_{A} is unitary, can be used to replace ηA†\eta^{\dagger}_{A}, ϵA†\epsilon^{\dagger}_{A}, and iA†i^{\dagger}_{A} by equivalent terms not containing †\dagger.□\Box

4 Other dagger pivotal notions

It is possible to define dagger variants of the remaining pivotal notions from Section 4:

A dagger pivotal category is spherical (respectively spacial) if it is spherical (respectively spacial) as a pivotal category.

A dagger braided pivotal category is a dagger pivotal category with a unitary braiding cA,B:A⊗B→B⊗Ac_{A,B}:A\otimes B\rightarrow B\otimes A.

Like any braided pivotal category, a dagger braided pivotal category is balanced by Lemma 4.20. However, in general the resulting twist θA:A→A\theta_{A}:A\rightarrow A is not unitary. In fact, θA\theta_{A} is unitary in this situation if and only if θA∗=(θA)∗\theta_{A^{*}}=(\theta_{A})^{*}, i.e., if and only if the category is tortile.

A dagger tortile category is defined in one of the following equivalent ways:

as a dagger braided pivotal category in which the canonical twist θA\theta_{A}, defined as in Lemma 4.20, is unitary;

as a tortile, dagger monoidal category such that the braiding is unitary, and such that ϵA\epsilon_{A} and ηA\eta_{A} satisfy the (equivalent) conditions of Lemma 7.6(c) and (d); or

as a dagger balanced monoidal category that is right autonomous and satisfies

A dagger compact closed category is a dagger tortile category such that θA=idA\theta_{A}=\textrm{\rm id}_{A} for all AA. Equivalently, it is a dagger symmetric monoidal category that is right autonomous and satisfies

The equivalence of the two definition is immediate from the third form of the definition of dagger tortile categories. Note that (7.2) is equivalent to (7.3) in the symmetric case. Further, these conditions are equivalent to the condition in Lemma 7.6(d).

The category FdHilb of finite dimensional Hilbert spaces is dagger compact closed, with A∗A^{*} the usual dual space of linear functions from AA to II, and with f†f^{\dagger} the usual linear algebra adjoint.

Each of the notions defined in this section (except the spherical notion) has a graphical language, extending the corresponding graphical language from Section 4, with the dagger of a diagram taken to be its mirror image. Each notion has a coherence theorem, proved by the same method as Theorems 7.2 and 7.3. As expected, equivalence of diagrams is up to isomorphism (for spacial dagger pivotal categories); up to regular isotopy (for dagger braided pivotal categories); up to framed 3-dimensional isotopy (for dagger tortile categories); and up to isomorphism (for dagger compact closed categories).

5 Dagger traced categories

There is no difficulty in defining dagger variants of each of the traced notions of Section 5. A (left or right) trace on a dagger monoidal category is called a dagger trace if it satisfies

For example: a dagger right traced category is a right traced dagger monoidal category satisfying (7.4). A balanced traced category is dagger balanced traced if it is dagger balanced and satisfies (7.4). And similarly for the other notions. The representation theorems of Section 5 extend to these dagger variants:

Every dagger braided [balanced, symmetric] traced category can be fully and faithfully embedded in a dagger braided pivotal [dagger tortile, dagger compact closed] category, via a dagger braided [balanced, symmetric] traced functor.□\Box

The proof, in each case, is by Joyal, Street, and Verity’s Int-construction , which respects the dagger structure.

The graphical language of each class of traced categories extends to the corresponding dagger traced categories, in a way suggested by equation (7.4). As usual, the dagger of a diagram is its mirror image, thus for example

The coherence theorems of Section 5 extend to this setting.

6 Dagger biproducts

In a dagger category, if A⊕BA\oplus B is a categorical product (with projections π1:A⊕B→A\pi_{1}:A\oplus B\rightarrow A and π2:A⊕B→B\pi_{2}:A\oplus B\rightarrow B), then it is automatically a coproduct (with injections π1†:A→A⊕B\pi^{\dagger}_{1}:A\rightarrow A\oplus B and π2†:B→A⊕B\pi^{\dagger}_{2}:B\rightarrow A\oplus B). It therefore makes sense to define a notion of dagger biproduct.

A dagger biproduct category is a biproduct category carrying a dagger structure, such that πi†=ιi:Ai→A1⊕A2\pi^{\dagger}_{i}=\iota_{i}:A_{i}\rightarrow A_{1}\oplus A_{2} for i=1,2i=1,2.

As in Section 6.3, we can equivalently define a dagger biproduct category as a dagger symmetric monoidal category, together with natural families of morphisms

such that ΔA†=∇A\Delta^{\dagger}_{A}=\nabla_{A} and ◊A†=□A\Diamond^{\dagger}_{A}=\Box_{A}, satisfying the axioms in Table 7.

The graphical language of dagger biproduct categories is like that of biproduct categories, where the dagger of a diagram is taken to be its mirror image. For example,

A well-formed equation between morphism terms in the language of dagger biproduct categories follows from the axioms of dagger biproduct categories if and only if it holds in the graphical language, up to isomorphism of diagrams, the diagrammatic manipulations shown in Table 8, and their duals.

By reduction to biproduct categories, as in the proofs of Theorems 7.2 and 7.3. The axioms ΔA†=∇A\Delta^{\dagger}_{A}=\nabla_{A} and ◊A†=□A\Diamond^{\dagger}_{A}=\Box_{A} allow †\dagger to be removed from anywhere but a morphism variable.□\Box

Finally, there is an obvious notion of dagger traced biproduct category (which is really a dagger traced dagger biproduct category), with graphical language derived from traced biproduct categories.

Bicategories

A bicategory is a generalization of a monoidal category. In addition to objects A,B,…A,B,\ldots and morphisms f,g,…f,g,\ldots, one now also considers 0-cells α,β,…\alpha,\beta,\ldots, which we can visualize as colors. For example, consider the following diagram. It is a standard diagram for monoidal categories, except that the areas between the wires have been colored.

As usual, we have objects A,B,C,D,E,FA,B,C,D,E,F and morphisms f:A→C⊗Df:A\rightarrow C\otimes D and g:B⊗C→F⊗Eg:B\otimes C\rightarrow F\otimes E. But now there are also 0-cells called green, red, yellow, and blue. In such diagrams, each object has a source, which is the 0-cell just above it, and a target, which is the 0-cell just below it. For example, we have A:\mboxgreen→\mboxyellowA:\mbox{green}\rightarrow\mbox{yellow}, B:\mboxyellow→\mboxblueB:\mbox{yellow}\rightarrow\mbox{blue}, and so on. It is now clear that, to be consistently colored, such diagrams have to satisfy some coloring constraints. The constraints are:

The tensor B⊗AB\otimes A of two objects may only be formed if the target of AA is equal to the source of BB. In symbols, for any 0-cells α,β,γ\alpha,\beta,\gamma, if A:α→βA:\alpha\rightarrow\beta and B:β→γB:\beta\rightarrow\gamma, then B⊗A:α→γB\otimes A:\alpha\rightarrow\gamma.

If f:A→Bf:A\rightarrow B is a morphism, then AA and BB must have a common source and a common target. In symbols, if f:A→Bf:A\rightarrow B and A:α→βA:\alpha\rightarrow\beta, then B:α→βB:\alpha\rightarrow\beta.

One also requires a unit object Iα:α→αI_{\alpha}:\alpha\rightarrow\alpha for every color α\alpha.

As an illustration of the second property, consider f:A→C⊗Df:A\rightarrow C\otimes D in the above example, where A:\mboxgreen→\mboxyellowA:\mbox{green}\rightarrow\mbox{yellow} and C⊗D:\mboxgreen→\mboxyellowC\otimes D:\mbox{green}\rightarrow\mbox{yellow}. Subject to the above coloring constraints, a bicategory is then required to satisfy exactly the same axioms as a monoidal category. Notice, for example, that if f:A→Bf:A\rightarrow B and g:B→Cg:B\rightarrow C and f,gf,g are well-colored, then so is g∘f:A→Cg\circ f:A\rightarrow C. Also, the identity maps idA:A→A\textrm{\rm id}_{A}:A\rightarrow A, the associativity map αA,B,C:(A⊗B)⊗C→≅A⊗(B⊗C)\alpha_{A,B,C}:(A\otimes B)\otimes C\xrightarrow{\cong}A\otimes(B\otimes C), and the other structural maps are well-colored. In particular, a monoidal category is the same thing as a one-object bicategory.

To give a detailed account of bicategories and their graphical languages is beyond the scope of this paper. We have already discussed over 30 different flavors of monoidal categories, and the reader can well imagine how many possible variations of bicategories there are, with 2-, 3-, and 4-dimensional graphical languages, once one considers bicategorical versions of braids, twists, adjoints, and traces. There are even more variations if one considers tricategories and beyond. We refer the reader to for the definition and basic properties of bicategories, and to , [2, Sec. 7] for a taste of their graphical languages.

Beyond a single tensor product

All the categorical notions that we have considered in this paper have just a single tensor product, which we represented as juxtaposition in the graphical languages. For notions of categories with more than one tensor product, the graphical languages get much more complicated. The details are beyond the scope of this paper, so we just outline the basics and give some references.

Examples of categories with more than one tensor are linearly distributive categories and *-autonomous categories . Both of these notions are models of multiplicative linear logic . These categories have two tensors, often called “tensor” and “par”, and written

The two tensors are related by some morphisms, such as A⊗(B\llampC)→(A⊗B)\llampCA\otimes(B\llamp C)\rightarrow(A\otimes B)\llamp C, while other similar morphisms, such as (A⊗B)\llampC→A⊗(B\llampC)(A\otimes B)\llamp C\rightarrow A\otimes(B\llamp C), are not present.

To make a graphical language for more than one tensor product, one must label the wires by morphism terms, rather than morphism variables. One must also introduce special tensor and par nodes as shown here:

A⊗B<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="0"displaystyle="false"><molspace="0em"rspace="0em">⊗</mo></mstyle></mrow><annotationencoding="application/x−tex">⊗</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.6667em;vertical−align:−0.0833em;"></span><spanclass="mord"><spanclass="mord">⊗</span></span></span></span></span></span>B<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="1"displaystyle="false"><mi>A</mi></mstyle></mrow><annotationencoding="application/x−tex">A</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.4783em;"></span><spanclass="mordmtightsizingreset−size6size3"><spanclass="mordmathnormalmtight">A</span></span></span></span></span></span>⊗\scriptstyle{A\otimes B}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mo lspace="0em" rspace="0em">⊗</mo></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{\otimes}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6667em;vertical-align:-0.0833em;"></span><span class="mord"><span class="mord">⊗</span></span></span></span></span></span>\scriptstyle{B}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><mi>A</mi></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{A}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4783em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mathnormal mtight">A</span></span></span></span></span></span>\textstyle{\otimes}A⊗B\scriptstyle{A\otimes B} A\llampB<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="1"displaystyle="false"><mi>B</mi></mstyle></mrow><annotationencoding="application/x−tex">B</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.4783em;"></span><spanclass="mordmtightsizingreset−size6size3"><spanclass="mordmathnormalmtight"style="margin−right:0.0502em;">B</span></span></span></span></span></span>A<spanclass="katex−display"><spanclass="katex"><spanclass="katex−mathml"><mathxmlns="http://www.w3.org/1998/Math/MathML"display="block"><semantics><mrow><mstylescriptlevel="0"displaystyle="false"><molspace="0em"rspace="0em">⊗</mo></mstyle></mrow><annotationencoding="application/x−tex">⊗</annotation></semantics></math></span><spanclass="katex−html"aria−hidden="true"><spanclass="base"><spanclass="strut"style="height:0.6667em;vertical−align:−0.0833em;"></span><spanclass="mord"><spanclass="mord">⊗</span></span></span></span></span></span>A⊗B\scriptstyle{A\llamp B}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="1" displaystyle="false"><mi>B</mi></mstyle></mrow><annotation encoding="application/x-tex">\scriptstyle{B}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.4783em;"></span><span class="mord mtight sizing reset-size6 size3"><span class="mord mathnormal mtight" style="margin-right:0.0502em;">B</span></span></span></span></span></span>\scriptstyle{A}<span class="katex-display"><span class="katex"><span class="katex-mathml"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block"><semantics><mrow><mstyle scriptlevel="0" displaystyle="false"><mo lspace="0em" rspace="0em">⊗</mo></mstyle></mrow><annotation encoding="application/x-tex">\textstyle{\otimes}</annotation></semantics></math></span><span class="katex-html" aria-hidden="true"><span class="base"><span class="strut" style="height:0.6667em;vertical-align:-0.0833em;"></span><span class="mord"><span class="mord">⊗</span></span></span></span></span></span>\scriptstyle{A\otimes B} The resulting theory is called the theory of proof nets, and was first given by Girard for unit-free multiplicative linear logic . It was later extended to include the tensor units by Blute et al. .

Summary

Table 10 summarizes the graphical languages from Sections 2–6. The name of each class of categories is shown along with a typical diagram or equation. The arrows indicate forgetful functors. We have omitted spherical categories, because they do not possess a graphical language modulo a natural notion of isotopy.

The letter dd indicates the dimension of the diagrams, and the letter ii indicates the dimension of the ambient space for isotopy. If i>di>d, then isotopy coincides with isomorphism of diagrams. Special cases are “3f” for framed diagrams and framed isotopy in 3 dimensions; “2+” for two-dimensional diagram with crossings (i.e., isotopy is taken on 2-dimensional projections, rather than on 3-dimensional diagrams); “reg” for regular isotopy; and “rot” to indicate that isotopy includes rotation of boxes. Finally, “eqn” indicates that equivalence of diagrams is taken modulo equational axioms.

The letter cc indicates the status of a coherence theorem. This is usually a reference to a proof of the theorem, or “conj” if the result is conjectured. A checkmark “√\surd” indicates a result that is folklore or whose proof is trivial. “int” indicates that the coherence theorem follows from a version of Joyal, Street, and Verity’s Int-construction, and the corresponding coherence theorem for pivotal categories. An asterisk “∗*” indicates that the result has only been proved for simple signatures.

Dagger variants can be defined of all of the notions shown in Table 10, except the planar autonomous and braided autonomous notions. Finally, bicategories require their own (presumably much larger) table and are not included here.

References