Abstract Scalars, Loops, and Free Traced and Strongly Compact Closed Categories

Introduction

In this preliminary section, we will discuss the background and motivation for the technical results in the main body of the paper, in a fairly wide-ranging fashion. The technical material itself should be essentially self-contained, from the level of a basic familiarity with monoidal categories (for which see e.g. ).

In recent work , the present author and Bob Coecke have developed a categorical axiomatics for Quantum Mechanics, as a foundation for high-level approaches to quantum informatics: type systems, logics, and languages for quantum programming and quantum protocol specification. The central notion in our axiomatic framework is that of strongly compact closed category. It turns out that this rather simple and elegant structure suffices to capture most of the key notions for quantum informatics: compound systems, unitary operations, projectors, preparations of entangled states, Dirac bra-ket notation, traces, scalars, the Born rule. This axiomatic framework admits a range of models, including of course the Hilbert space formulation of quantum mechanics.

Additional evidence for the scope of the framework is provided by recent work of Selinger . He shows that the framework of completely positive maps acting on generalized states represented by density operators, used in his previous work on the semantics of quantum programming languages , fits perfectly into the framework of strongly compact closed categories. Selinger prefers to use the term ‘dagger compact closed category’, since the notion of adjoint which is formalized by the dagger operation $()^{\dagger}$ is a separate structure which is meaningful in a more general setting. He also showed that a simple construction (independently found and studied in some depth by Coecke ), which can be carried out completely generally at the level of strongly compact closed categories, corresponds to passing to the category of completely positive maps (and specializes exactly to this in the case of Hilbert spaces).

2 Multiplicatives and Additives

We briefly mention a wider context for these ideas. To capture the branching structure of measurements, and the flow of (classical) information from the result of a measurement to the future evolution of the quantum system, an additional additive level of structure is required, based on a functor $\oplus$, as well as the multiplicative level of the compact closed structure based around the tensor product (monoidal structure) $\otimes$. This delineation of additive and multiplicative levels of Quantum Mechanics is one of the conceptually interesting outcomes of our categorical axiomatics. (The terminology is based on that of Linear Logic — of which our structures can be seen as ‘collapsed models’). In terms of ordinary algebra, the multiplicative level corresponds to the multilinear-algebraic aspect of Quantum Mechanics, and the additive level to the linear-algebraic. But this distinction is usually lost in the sea of matrices; in particular, it is a real surprise how much can be done purely with the multiplicative structure.

It should be mentioned that we fully expect an exponential level to become important, in the passage to the multi-particle, infinite dimensional, relativistic, and eventually field-theoretic levels of quantum theory.

We shall not discuss the additive level further in this paper. For most purposes, the additive structure can be regarded as freely generated, subject to arithmetic requirements on the scalars (see ).

3 Explicit constructions of free structured categories

Our main aim in the present paper is to give explicit characterizations of free constructions for various kinds of categories-with-structure, most notably, for traced symmetric monoidal and strongly compact closed categories. We aim to give a synthetic account, including some basic cases which are well known from the existing literature . We will progressively build up structure through the following levels:

Of these, those cases which have not, to the best of our knowledge,, appeared previously are (3), (5) and (6). But in any event, we hope that our account will serve as a clear, accessible and useful reference.

It should be emphasized that constructions (1)–(4) are free over categories, (5) over categories with involutions, and (6) over a comma category of categories with involution with a specified evaluation of scalars. We note that Dusko Pavlovic has give a free construction of traced categories over monoidal categories . His construction is elegant, but abstract and less combinatorial/geometric than ours: perhaps necessarily so, since in our situation the monoidal structure, which itself has some spatial content, is added freely. Another reference is by Katis, Sabadini and Walters . They construct a free ‘feedback category’, which is a trace minus the Yanking axiom — which is very important for the dynamics of the trace — over a monoidal category, and then formally quotient it to get a traced category. A treatment in the same style as the present paper of free traced, compact closed and strongly compact closed categories over a monoidal category remains a topic for future investigation.

Furthermore, we will work entirely with the strict versions of the categories-with-structure we will study. Since in each case, every such category is monoidally equivalent to a strict one, this does not really lose any generality; while by greatly simplifying the description of the free constructions, it makes their essential content, especially the geometry that begins to emerge as we add traces and compact closure (paths and loops), much more apparent.

4 Diagrammatics

Our free constructions have immediate diagrammatic interpretations, which make their geometric content quite clear and vivid. Diagrammatic notation for tensor categories has been extensively developed with a view to applications in categorical formulations of topological invariants, quantum groups, and topological quantum field theories . Within the purely categorical literature, a forerunner of these developments is the early work of Kelly on coherence ; while the are also several precursors in the non-categorical literature, notably Penrose’s diagrammatic notation for abstract tensors .

Diagrammatic notation has played an important role in our own work with Coecke on applying our categorical axiomatics to quantum informatics, e.g. to quantum protocols . For example, the essence of the verification of the teleportation protocol is the diagrammatic equality shown in Figure 1. For details, see .

5 Categorical Quantum Logic

The diagrammatics of our constructions leads in turn to the idea of a logical formulation, in which the diagrammatic representation of a morphism in the free category is thought of as a proof-net, in the same general sense as in Linear Logic .

More precisely, morphisms in the free category will correspond to proof nets in normal form, and the definition of composition in the category gives a direct construction for normalizing a cut between two such proof nets. One advantage of the logical formulation is that we get an explicit syntactic description of these objects, and we can decompose the normalization process into cut-reduction steps, so that the computation of the normal form can be captured by a rewriting system. This provides an explicit computational basis for deciding equality of proofs, which corresponds in the categorical context to verifying the commutativity of a diagram.

In the categorical approach to quantum informatics , verifying the correctness of various quantum protocols is formulated as showing the commutativity of certain diagrams; so a computational theory of the above kind is directly applicable to such verifications.

In a joint paper with Ross Duncan , we have developed a system of Categorical Quantum Logic along these lines, incorporating additive as well as multiplicative features. This kind of logic, and its connection with Quantum Mechanics, is very different to the traditional notion of ‘Quantum Logic’ . Duncan is continuing to develop this approach in his forthcoming thesis.

6 Overview

The further structure of the paper is as follows. In Section 2 we explore the abstract notion of scalar which exists in any monoidal category. As we will see, scalars play an important role in determining the structure of free traced and strongly compact closed categories, as they correspond to the values of loops. In Section 3, we review the notions of compact closed and strongly compact closed categories. The need for the notion of strong compact closure, to capture the structure of the complex spaces arising in Quantum Mechanics, is explained. In Section 4, we turn to the free constructions themselves.

Given $\lambda:[n]\rightarrow X$, $\mu:[m]\rightarrow X$, we define $[\lambda,\mu]:[n+m]\rightarrow X$ by

We write $\mathcal{M}(X)$ for the free commutative monoid generated by a set $X$. Concretely, these are the finite multisets over $X$, with the addition given by multiset union, which we write as $S\uplus T$.

Scalars in monoidal categories

The concept of a scalar as a basis for quantitative measurements is fundamental in Physics. In particular, in Quantum Mechanics complex numbers $\alpha$ play the role of probability amplitudes, with corresponding probabilities $\alpha\bar{\alpha}=|\alpha|^{2}$.

A key step in the development of the categorical axiomatics for Quantum Mechanics in was the recognition that the notion of scalar is meaningful in great generality --- in fact, in any monoidal (not necessarily symmetric) category. Susbsequently, I became aware through Martin Hyland of the mathematical literature on Tannakian categories , stemming ultimately from Grothendiek. Tannakian categories embody much stronger assumptions than ours, in particular that the categories are abelian as well as compact closed, although the idea of strong compact closure is absent. But they certainly exhibit a consonant development of a large part of multilinear algebra in an abstract setting.

We remark that in the non-strict case, where we have unit isomorphisms

We write $s\bullet f$ for $f\circ s_{A}=s_{B}\circ f$. Note that

which exactly generalizes the multiplicative part of the usual properties of scalar multiplication. Thus scalars act globally on the whole category.

Strongly Compact Closed Categories

A compact closed category is a symmetric monoidal category in which to each object $A$ a dual $A^{*}$, a unit $\eta_{A}:{\rm I}\to A^{*}\otimes A$ and a counit $\epsilon_{A}:A\otimes A^{*}\to{\rm I}$ are assigned in such a way that the following ‘triangular identities’ hold:

Viewing monoidal categories as bicategories with a single 0-cell, this amounts to the axiom:

We can also view compact closed categories as *-autonomous categories for which ${\otimes}={\bindnasrepma}$, and hence as ‘collapsed’ models of Linear Logic .

$({\bf Rel},\times)$: Sets, relations, and cartesian product. Here $\eta_{X}\subseteq\{*\}\times(X\times X)$ and we have

where $n$ is the dimension of $V$, $\{e_{i}\}_{i=1}^{i=n}$ is a basis for $V$ and $\bar{e}_{i}$ is the linear functional in $V^{*}$ determined by $\bar{e}_{j}(e_{i})=\delta_{ij}$.

2 Duality, Names and Conames

For each morphism $f:A\to B$ in a compact closed category we can construct a dual $f^{*}:B^{*}\rightarrow A^{*}$:

The assignment $f\mapsto f^{*}$ extends $A\mapsto A^{*}$ into a contravariant endofunctor with $A\simeq A^{**}$. In any compact closed category, we have

3 Why compact closure does not suffice

In inner-product spaces we have the adjoint:

This is not the same as the dual — the types are different. In “degenerate” CCC’s in which $A^{*}=A$, e.g. $\mathbf{Rel}$ or real inner-product spaces, we have $f^{*}=f^{\dagger}$. In complex inner-product spaces such as Hilbert spaces, the inner product is sesquilinear

and the isomorphism $A\simeq A^{*}$ is not linear, but conjugate linear:

and hence does not live in the category $\mathbf{Hilb}$ at all!

4 Solution: Strong Compact Closure

We define the conjugate space of a Hilbert space ${\cal H}$: this has the same additive group of vectors as ${\cal H}$, while the scalar multiplication and inner product are “twisted” by complex conjugation:

We can define ${\cal H}^{*}=\bar{{\cal H}}$, since ${\cal H}$, $\bar{{\cal H}}$ have the same orthornormal bases, and we can define the counit by

which is indeed (bi)linear rather than sesquilinear!

The crucial observation is this: $()^{*}$ has a covariant functorial extension $f\mapsto f_{*}$, which is essentially identity on morphisms; and then we can define

5 Axiomatization of Strong Compact Closure

A strict monoidal involutive assignment $A\mapsto A^{*}$ on objects.

An identity-on-objects, contravariant, strict monoidal, involutive functor $f\mapsto f^{\dagger}$.

commutes, where $\tau_{A,A}:A\otimes A\simeq A\otimes A$ is the twist map.

Given such a functor $()^{\dagger}$, we define an isomorphism $\alpha$ to be unitary if $\alpha^{-1}=\alpha^{\dagger}$. We additionally require that the canonical natural isomorphism for symmetry given as part of the symmetric monoidal structure on $\mathcal{C}$ is (componentwise) unitary in this sense.

While diagram (5) is the analogue to (3) with $\eta_{A}^{\dagger}\circ\tau_{A,A^{*}}$ playing the role of the counit, diagram (6) expresses Yanking with respect to the canonical trace of the compact closed structure. In fact, we have used the ‘left trace’ here rather than the more customary ‘right trace’ which we shall use in our subsequent discussion of traced monoidal categories. In the symmetric context, the two are equivalent; we chose the left trace here because, given our other notational conventions, it requires less use of symmetries in stating the axiom. We only need one commuting diagram as compared to (3) and (3) in the definition of compact closure, since due to the strictness assumption (i.e. $A\mapsto A^{*}$ being involutive) we were able to replace the second diagram by $\eta_{A^{*}}=\tau_{A^{*}\!,A}\circ\eta_{A}$.

Yanking diagrammatically

Free Constructions

We will now give detailed descriptions of free constructions for a number of types of category-with-structure. We shall consider the following cases:

For cases (1)–(4), we shall consider adjunctions of the form

where $S$ ranges over the various kinds of structure. Specifically, we shall give explicit descriptions in each case of $F_{S}(\mathcal{C})$ for a category $\mathcal{C}$. This explicit description — not algebraically by generators and relations, but giving direct combinatorial definitions of the normal forms and how they compose, thus solving the word problem over these categories — is the strongest form of coherence theorem available for notions such as compact closure and traces. In these cases, cyclic structures arise, violating the compatibility requirements for stronger forms of coherence developed in . This point is discussed in the concluding section of .

where $\mathbf{InvCat}$ is the category of categories with a specified involution, (what Selinger calls ‘dagger categories’ in ), and functors which preserve the involution. Finally, in (6) we consider an adjunction with respect to a comma category, which allows us to describe the free strongly compact slosed category generated by a category $\mathcal{C}$, together with a prescribed multiplicative monoid of scalars.

Our treatment will be incremental, reflecting the fact that in our sequence (1)–(6), each term arises by adding structure to the previous one. Each form of structure is reflected conceptually by a new feature arising in the corresponding free construction:

We will also begin to see a primitive graph-theoretic geometry of points, lines and paths begin to emerge as we progress through the levels of structure. There is in fact more substantial geometry lurking here than might be apparent: the elaboration of these connections must be left to future work.

Finally, we mention a recurring theme. To form a ‘pure’ picture of each construction, it is useful to consider the case $F_{S}(\mathbf{1})$ explicitly, where $\mathbf{1}$ is the category with (one object and) one morphism (i.e. one generator, no relations).

An arrow from one list of objects to another is simply a list of arrows of $\mathcal{C}$ of the appropriate types. Note that there can only be an arrow between lists of the same length. Composition is performed pointwise in the obvious fashion.

A morphism $\lambda:(n,A)\rightarrow(m,B)$ can only exist if $n=m$, and is specified by a map $\lambda:[n]\rightarrow\mathsf{Mor}\,\mathcal{C}$, satisfying

Arrows in $F_{\mathsf{M}}(\mathcal{C})$ are thus simply those expressible in the form

Unicity of the monoidal functor to a monoidal category $\mathcal{M}$ extending a given functor $F:\mathcal{C}\rightarrow U_{\mathsf{M}}\mathcal{M}$ is then immediate.

2 Symmetric Monoidal Categories

The objects of $F_{\mathsf{SM}}(\mathcal{C})$ are the same as in the monoidal case.

An arrow $(n,A)\longrightarrow(n,B)$ is given by $(\pi,\lambda)$, where $\pi\in S(n)$ is a permutation, and $\lambda_{i}:A_{i}\rightarrow B_{\pi(i)}$, $1\leq i\leq n$. {diagram}

Composition in $F_{\mathsf{SM}}(\mathcal{C})$ is described as follows. Form paths of length 2, and compose the arrows from $\mathcal{C}$ labelling these paths.

Note that $F_{\mathsf{SM}}(\mathbf{1})=\coprod_{n}S(n)$ (coproduct of categories). Thus the free monoidal category on the trivial generating category comprises (the disjoint union of) all the finite symmetric groups. At this point, a possible step towards geometry presents itself. If we considered free braided monoidal categories, we would find a similar connection to the braid groups . However, we shall not pursue that here.

Let $\mathcal{M}$ be a symmetric monoidal category, and consider a tensor product $A_{1}\otimes\cdots\otimes A_{n}$. Each element $\pi\in S(n)$ of the symmetric group $S(n)$ induces an isomorphism, which by abuse of notation we also write as $\pi$:

Now note that under the above concrete description of $F_{\mathsf{SM}}(\mathcal{C})$, arrows

Again, the freeness property follows directly. The main observation to be made is that such arrows are closed under composition:

where if $\pi\in S(n)$, $\sigma\in S(m)$, $\pi\otimes\sigma\in S(n+m)$ is the evident concatenation of the two permutations, as defined in the Introduction.

The above closed form expression for composition requires the ‘naturality square’:

3 Traced Symmetric Monoidal Categories

We now come to a key case, that of traced symmetric monoidal categories. Much of the structure of strongly compact closed categories in fact appears already at the traced level. This is revealed rather clearly by our incremental development of the free constructions.

for objects $A$, $B$, $U$ of $\mathcal{C}$, satisfying the following axioms:

where $f:A\otimes U\to B\otimes U$, $g:A^{\prime}\to A$,

where $f:A\otimes U\to B\otimes U$, $g:B\to B^{\prime}$,

where $f:A\otimes U\to B\otimes U^{\prime}$, $g:U^{\prime}\to U$,

where $f:A\otimes I\to B\otimes I$ and $g:A\otimes U\otimes V\to B\otimes U\otimes V$.

where $f:A\otimes U\to B\otimes U$ and $g:W\to Z$ .

Diagrammatically, we depict the trace as feedback:

It corresponds to contracting indices in traditional tensor calculus.

We now consider the free symmetric monoidal category generated by $\mathcal{C}$, $F_{\mathsf{SM}}(\mathcal{C})$, as described in the previous section. Recall that morphisms in $F_{\mathsf{SM}}(\mathcal{C})$ can be written as

Our first observation is that this category is already canonically traced. Understanding why this is so, and why $F_{\mathsf{SM}}(\mathcal{C})$ is not the free traced category, will lay bare the essential features of the free construction we are seeking.

Note firstly that, if there is an arrow $f:(n,A)\otimes(p,U)\rightarrow(m,B)\otimes(p,U)$ in $F_{\mathsf{SM}}(\mathcal{C})$, then we must have $n+p=m+p$, and hence $n=m$. Thus we can indeed hope to form an arrow $A\rightarrow B$ in $F_{\mathsf{SM}}(\mathcal{C})$. Now we consider the ‘geometry’ arising from the permutation $\pi$, together with the diagrammatic feedback interpretation of the trace. We illustrate this with the following example.

Consider the arrow $f=\pi^{-1}\circ\bigotimes_{i=1}^{4}f_{i}$, where $\pi=(2,4,3,1)$, and $f_{i}:A_{i}\rightarrow B_{\pi(i)}$. Suppose that $A_{i}=U_{i}=B_{i}$, $2\leq i\leq 4$, and write $U=\bigotimes_{i=2}^{4}U_{i}$. We wish to compute $\mathsf{Tr}_{A_{1},B_{1}}^{U}(f)$. The geometry is made clear by the following figure.

We simply follow the path leading from $A_{1}$ to $B_{1}$:

composing the arrows which label the arcs in the path: thus

in this case. A similar procedure can always be followed for arrows in the form (7), which as we have seen is general for $F_{\mathsf{SM}}(\mathcal{C})$. (It is perhaps not immediately obvious that a path from an input will always emerge from the feedback zone into an output. See the following Proposition 1). Moreover, this assignment does lead to a well-defined trace on $F_{\mathsf{SM}}(\mathcal{C})$. However, this is not the free traced structure generated by $\mathcal{C}$.

We now turn to a more formal account, culminating in the construction of $F_{\mathsf{Tr}}(\mathcal{C})$.

Geometry of permutations

We begin with a more detailed analysis of permutations $\pi\in S(n+m)$, with the decomposition $n+m$ reflecting our distinction between the visible (input-output) part of the type, and the hidden (feedback) part, arising from the application of the trace.

We define an $n$-path (or if $n$ is understood, an input-output path) of $\pi$ to be a sequence

where $1\leq i,j\leq n$, and for all $0<p<k$, $\pi^{p}(i)>n$. We write $P_{\pi}(i)$ for the $n$-path starting from $i$, which is clearly unique if it exists, and also $p_{\pi}(i)=j$. We write $P_{\pi}^{0}(i)$ for the set of elements of $\{n+1,\dots,n+m\}$ appearing in the sequence. A loop of $\pi$ is defined to be a cycle

where $n<j\leq n+m$. We write $\mathcal{L}(\pi)$ for the set of all loops of $\pi$.

The following holds for any permutation $\pi\in S(n+m)$:

For each $i$, $1\leq i\leq n$, $P_{\pi}(i)$ is well-defined.

form a partition of $\{n+1,\ldots,n+m\}$.

Either we reach $\pi^{k+1}=j\leq n$, or there must be a least $l$ such that

(Note that the fact that $i\leq n$ allows us to write the left hand term as $\pi^{k+1}(i)$). But then, applying $\pi^{-1}$, we conclude that $\pi^{k}(i)=\pi^{l}(i)$, a contradiction.

If $p_{\pi}(i)=p_{\pi}(j)$, then $\pi^{k+1}(i)=\pi^{l+1}(j)$, where say $k\leq l$. Applying $(\pi^{-1})^{k+1}$, we obtain $i=\pi^{l-k}(j)\leq n$, whence $l=k$ and $i=j$.

It is standard that distinct cycles are disjoint. We can reason similarly to part (2) to show that if $P_{\pi}^{0}(i)$ meets $P_{\pi}^{0}(j)$, then $i=j$. Similar reasoning to (1) shows that $P_{\pi}^{0}(i)\cap L=\varnothing$, for $L\in\mathcal{L}(\pi)$. Finally, iterating $\pi^{-1}$ on $j>n$ either forms a cycle, or reaches $i\leq n$; in the latter case, $j\in P_{\pi}^{0}(i)$.

We now give a more algebraic description of the permutation $p_{\pi}$. Firstly, we extend our notation by defining $[n{:}m]:=\{n+1,\ldots,m\}$. Now we can write $[n{+}m]=[n]\sqcup[n{:}n{+}m]$, where $\sqcup$ is disjoint union. We can use this decomposition to express $\pi\in S(n{+}m)$ as the disjoint union of the following four maps:

We can view these maps as binary relations on $[n{+}m]$ (they are in fact injective partial functions), and use relational algebra (union $R\cup S$, relational composition $R;S$ and reflexive transitive closure $R^{\ast}$) to express $p_{\pi}$ in terms of the $\pi_{ij}$:

We can also characterize the elements of $\mathcal{L}(\pi)$:

Loops

We follow Kelly and Laplaza in making the following basic definitions. The loops of a category $\mathcal{C}$, written $\mathcal{L}[\mathcal{C}]$, are the endomorphisms of $\mathcal{C}$ quotiented by the following equivalence relation: a composition {diagram} is equated with all its cyclic permutations. A trace function on $\mathcal{C}$ is a map on the endomorphisms of $\mathcal{C}$ which respects this equivalence. We note in particular the following standard result :

If $\mathcal{C}$ is traced, then the trace applied to endomorphisms:

Traces of decomposable morphisms

We now turn to a general proposition about traced categories, from which the structure of the free category will be readily apparent. It shows that whenever a morphism is decomposable into a tensor product followed by a permutation (as all morphisms in $F_{\mathsf{SM}}(\mathcal{C})$ are), then the trace can be calculated explictly by composing over paths.

Let $\mathcal{C}$ be a traced symmetric monoidal category, and consider a morphism of the form

where $C=\bigotimes_{i=1}^{n}A_{i}\otimes\bigotimes_{j=n+1}^{n+m}U_{j}$, $D=\bigotimes_{i=1}^{n}B_{i}\otimes\bigotimes_{j=n+1}^{n+m}U_{j}$, $\pi\in S(n+m)$, and $f_{i}:C_{i}\rightarrow D_{\pi(i)}$. Then

where for each $1\leq i\leq n$, with $n$-path

Taken together with the following instance of Superposing:

this Proposition yields a closed form description of the trace on expressions of the form:

We approach the proof of this Proposition via a number of lemmas.

Firstly, a simple consequence of Feedback Dinaturality:

Let $U=\bigotimes_{i=1}^{n}U_{i}$, and $\sigma\in S(n)$. Let $\sigma U=\bigotimes_{i=1}^{n}U_{\sigma(i)}$. Then

We now show how the trace is evaluated along cyclic paths of any length. We write $\sigma_{k+1}=\begin{pmatrix}1&2&\cdots&k&k+1\\ 2&3&\cdots&k+1&1\end{pmatrix}$, the cyclic permutation of length $k+1$. Note the useful recursion formula:

The proof is relegated to the Appendix. This lemma simultaneously generalizes Vanishing I ($k=0$) and Yanking ($k=1$, $A_{1}=A_{2}=A_{3}$, $f_{1}=f_{2}=1_{A_{1}}$), and also the Generalized Yanking of . The geometry of the situation is made clear by the following diagram.

Note that for $k=0$, this is just Vanishing I. Up to conjugation by some permutation $\sigma$, we can express $\pi$ as the tensor product of its $n$-paths and loops:

Using Lemmas 3 and 2, we can express the trace of $f$ in terms of the traces of the morphisms corresponding to the $n$-paths and loops of $\pi$. The trace of each $n$-path is given by Lemma 4. ∎

Description of F𝖳𝗋​(𝒞)F_{\mathsf{Tr}}(\mathcal{C})

The objects are as for $F_{\mathsf{SM}}(\mathcal{C})$. A morphism now has the form $(S,\pi,\lambda)$, where $(\pi,\lambda)$ are as in $F_{\mathsf{SM}}(\mathcal{C})$, and $S$ is a multiset of loops in $\mathcal{L}[\mathcal{C}]$, i.e. an element of $\mathcal{M}(\mathcal{L}[\mathcal{C}])$, the free commutative monoid generated by $\mathcal{L}[\mathcal{C}]$.

in the language of traced symmetric monoidal categories. This will be our closed-form description of morphisms in the free traced category. It follows from Proposition 3, together with equations (1)–(4), (8), (9), (10), that this is indeed closed under the traced monoidal operations.

We define the main operations on morphisms.

Composition

Tensor product

Trace

That is, the objects in this free category are the natural numbers; a morphism is a pair $(\pi,n)$, where $\pi$ is a permutation, and $n$ is a natural number counting the number of loops.

4 Compact Closed Categories

The free construction for compact closed categories was characterized in the pioneering paper by Kelly and Laplaza . Their construction is rather complex. Even when simplified to the strict monoidal case, several aspects of the construction are bundled in together, and it can be hard to spot what is going one. (For example, the path construction we gave for the trace in the previous section is implicit in their paper — but not easy to spot!). We are now in a good position to disentangle and clarify their construction. Indeed, we have already explictly constructed $F_{\mathsf{Tr}}(\mathcal{C})$, and there is the $\mathcal{G}$ or Int construction of Joyal, Street and Verity Prefigured in , and also in some unpublished lectures of Martin Hyland ., which is developed in the symmetric monoidal context with connections to Computer Science issues and the Geometry of Interaction in . This construction gives the free compact closed category generated by a traced monoidal category. Thus we can recover the Kelly-Laplaza construction as the composition of these two adjunctions:

Adjoints compose, so $F_{\mathsf{CC}}(\mathcal{C})=\mathcal{G}\circ F_{\mathsf{Tr}}(\mathcal{C})$. This factorization allows us to ‘rationally reconstruct’ the Kelly-Laplaza construction.

The main notion which has to be added to those already present in $F_{\mathsf{Tr}}(\mathcal{C})$ is that of polarity. The ability to distincguish between positive and negative occurrences of a variable will allow us to transpose variables from inputs to outputs, or vice versa. This possibility of transposing variables means that we no longer have the simple situation that morphisms must be between lists of generating objects of the same length. However, note that in a compact closed category, $(A\otimes B)^{*}\simeq A^{*}\otimes B^{*}$, so any object constructed from generating objects by tensor product and duality will be isomorphic to one of the form

will, after transposing the negative objects, be in biunique correspondence with one of the form

A key observation is that in the free category, this transposed map (15) will again be of the closed form (13) which characterizes morphisms in $F_{\mathsf{Tr}}(\mathcal{C})$, as we saw in the previous section. From this, the construction of $F_{\mathsf{CC}}(\mathcal{C})$ will follow directly.

The objects in $F_{\mathsf{CC}}(\mathcal{C})$ are, following the $\mathcal{G}$ construction applied to $F_{\mathsf{Tr}}(\mathcal{C})$, pairs of objects of $F_{\mathsf{Tr}}(\mathcal{C})$, hence of the form $(n,m,A^{+},A^{-})$, where

Such an object can be read as the tensor product

This is equivalent to the Kelly-Laplaza notion of signed set, under which objects have the form $(n,A,\mathsf{sgn})$, where $\mathsf{sgn}:[n]\rightarrow\{{+},{-}\}$.

Operations on objects

The tensor product is defined componentwise on the positive and negative components. Formally:

The duality simply interchanges positive and negative components:

Note that the duality is involutive, and distributes through tensor:

Morphisms

where we require $n+q=k=m+p$, $\pi\in S(k)$, and $\lambda:[k]\rightarrow\mathsf{Mor}\,\mathcal{C}$, such that

$S$ is a multiset of loops, just as in $F_{\mathsf{Tr}}(\mathcal{C})$. Note that $(S,\lambda,\pi)$ can indeed be seen as a morphism in $F_{\mathsf{Tr}}(\mathcal{C})$ in the transposed form (15), as discussed previously.

We now describe the compact closed operations on morphisms.

Composition

Composition of a morphism $f:A\rightarrow B$ with a morphism $g:B\rightarrow B$ is given by feeding ‘outputs’ by $f$ from the positive component of $B$ as inputs to $g$ (since for $g$, $B$ occurs negatively, and hence the positive and negative components are interchanged); and symmetrically, feeding the $g$ outputs from the negative components of $B$ as inputs to $f$. This symmetry allows the strong form of duality present in compact closed categories to be interpreted in a very direct and natural fashion.

This general prescription is elegantly captured algebraically in terms of the trace, which co-operates with the duality to allow symmetric interaction between the two morphisms which are being composed. This is illustrated by the following diagram, which first appeared in :

A concrete account for $F_{\mathsf{CC}}(\mathcal{C})$ follows directly from our description of the trace in $F_{\mathsf{Tr}}(\mathcal{C})$: chase paths, and compose (in $\mathcal{C}$) the morphisms labelling the paths to get the labels. In general, loops will be formed, and must be added to the multiset. Formally, given arrows

This is essentially the ‘Execution formula’ — see also and ; it appears implicitly in as a coequaliser.

Similarly, we can characterize the loops formed by composing $\pi$ and $\sigma$, $\mathcal{L}(\pi,\sigma)$, by

Tensor Product

This is defined componentwise as in $F_{\mathsf{Tr}}(\mathcal{C})$, with appropriate permutation of indices in order to align positive and negative components correctly.

Units and Counits

Firstly, we describe the identity morphisms explicitly:

We join each dot in the input to the corresponding one in the output, and label it with the appropriate identity arrow.

Thus identities, units and counits are essentially all the same, except that the polarities allow variables to be transposed freely between the domain and codomain.

5 Strongly Compact Closed Categories

We now wish to analyze the new notion of strongly compact closed category in the same style as the previous constructions. Fortunately, there is a simple observation which makes this quite transparent. Provided that the category we begin with is already equipped with an involution (but no other structure), then this involution ‘lifts’ through all our constructions, yielding the free ‘dagger version’ (in the sense of ) of each of our constructions. In particular, our construction of $F_{\mathsf{CC}}(\mathcal{C})$ in the previous section in fact gives rise to the free strongly compact closed category.

More precisely, we shall describe an adjunction {diagram} where $\mathbf{InvCat}$ is the category of categories with a specified involution, i.e. an identity on objects, contravariant, involutive functor; and functors preserving the involution.

Our previous construction of $F_{\mathsf{CC}}(\mathcal{C})$ lifts directly to this setting. The main point is that we can define an involution $()^{\dagger}$ on $F_{\mathsf{CC}}(\mathcal{C})$, under the assumption that we are given a primitive $()^{\dagger}$ on the generating category $\mathcal{C}$. The dagger on $F_{\mathsf{CC}}(\mathcal{C})$ will endow it with the structure of a strongly compact closed category (for which the compact closed part will coincide with that already described for $F_{\mathsf{CC}}(\mathcal{C})$).

In short, we reverse direction on the arrows connecting the dots (including reversing the direction of loops), and label the reversed arrows with the reversals of the original labels. This contrasts with the dual $f^{*}$, which by the way types are interpreted in this free situation, is essentially the same combinatorial object as $f$, but with a different ‘marking’ by polarities — there are no reversals involved. Thus, if we had a labelling morphism

then we will get {diagram} It is easy to see that $\eta_{A}=\epsilon_{A}^{\dagger}$, so this is compatible with our previous construction of $F_{\mathsf{CC}}(\mathcal{C})$.

6 Parameterizing on the Monoid

which sends a category to its sets of loops. The dagger defines an involution on the set of loops. Involution-preserving functors induce involution-preserving functions on the loops.

Now let $\mathbf{InvCMon}$ be the category of commutative monoids with involution, and involution-preserving homomorphisms. There is an evident forgetful functor $U_{\mathbf{InvCMon}}\longrightarrow\mathbf{InvSet}$. We can form the comma category $(\mathcal{L}\downarrow U_{\mathbf{InvCMon}})$, whose objects are of the form $(\mathcal{C},\varphi,M)$, where $\varphi$ is an involution-preserving map from $\mathcal{L}[\mathcal{C}]$ to the underlying set of $M$. Here we can think of $M$ as the prescribed monoid of scalars, and $\varphi$ as specifying how to evaluate loops from $\mathcal{C}$ in this monoid.

There is a forgetful functor $U_{\mathcal{V}}:\mathsf{SCC}{-}\mathbf{Cat}\longrightarrow\mathcal{V}$

Our task is to construct an adjunction {diagram} which builds the free SCC on a category with prescribed scalars. This is a simple variation on our previous construction of $F_{\mathsf{SCC}}(\mathcal{C})$, which essentially acts by composition with the loop evaluation function $\varphi$ on $F_{\mathsf{SCC}}(\mathcal{C})$. We use the prescribed monoid $M$ in place of $\mathcal{M}(\mathcal{L}[\mathcal{C}])$. Thus a morphism in $F_{\mathcal{V}}(\mathcal{C})$ will have the form $(m,\pi,\lambda)$, where $m\in M$. Multiset union is replaced by the monoid operation of $M$. The action of the dagger functor on elements of $M$ is by the given involution on $M$. When loops in $\mathcal{C}$ arise in forming compositions in the free category, they are evaluated in $M$ using the function $\varphi$.

The monoid of scalars in this free category will of course be $M$.

References

Appendix

The following equational proofs involve some long typed formulas. To aid in readability, we have annotated each equational step (reading down the page) by $\underline{\text{\emph{underlining}}}$ each redex, and $\overline{\text{\emph{overlining}}}$ the corresponding contractum.

Proof of Lemma 4

Note that for $k=0$, this is just Vanishing I. We now reason inductively when $k>0$.