A Note on Bainbridge’s Power Set Construction

Peter Selinger^{∗} Department of Mathematics University of Michigan Ann Arbor, MI 48109-1109

4 May 1998

Abstract The category Rel of sets and relations has two natural traced monoidal structures: in (Rel, +, Tr), the tensor is given by disjoint union, and in (Rel, ×, Tr′) by products of sets. Already in 1976, predating the definition of traced monoidal categories by 20 years, Bainbridge has shown how to model flowcharts and networks in these two respective settings. Bainbridge has also pointed out that one can move from one setting to the other via the power set operation. However, Bainbridge’s power operation is not functorial, and in this paper we show that there is no traced monoidal embedding of (Rel, +, Tr) into (Rel, ×, Tr′) whose object part is given by the power set operation. On the other hand, we show that there is such an embedding whose object part is given by the power-multiset operation.

Introduction

Predating the definition of traced monoidal categories [2] by 20 years, Bainbridge [1] has pointed out in 1976 that there exist (in today’s terminology) two natural traced monoidal structures on the category Rel of sets and relations. The first one is (Rel, +, Tr), where the tensor product is given by disjoint union of sets. The second one is (Rel, ×, Tr′), where tensor is given by products of sets. Bainbridge used these categories to give a compositional semantics to flowcharts and networks, respectively, and he pointed out a duality between the two situations: the power set operation takes the first category to the second, and it gives rise to a homset-wise Galois connection. Bainbridge’s power operation maps a set X to the power set P X, and a relation R : X → Y to the relation P R : P X → P Y given by α P R β iff for all x ∈ α, xRy implies y ∈ β. Remarkably, this operation preserves not only composition and tensor, but also trace. However, it does not preserve identities, and it is therefore not a functor.

One may now ask whether there is some variant of Bainbridge’s construction that yields an actual functor of traced monoidal categories. More precisely: is there a traced monoidal embedding of (Rel, +, Tr) into (Rel, ×, Tr′) whose object part is given by power sets? The answer, as we shall see, is no. In fact, there is no traced monoidal embedding between these categories that maps finite sets to finite sets. On the other hand, we will show that such an embedding exists whose object part is given by the power-multiset operation.

Thanks to Thomas Hildebrandt for pointing out a mistake in the first draft of this manuscript.

An embedding of (Rel, +, Tr) into (Rel, ×, Tr′)

Let Rel be the category of sets and relations, and let Rel_{fin} be the full subcategory of finite sets. On Rel, we consider two traced monoidal structures (Rel, +, Tr) and (Rel, ×, Tr′). For the first one, + is disjoint union of sets, and for R : X + Z → Y + Z, Tr_{Z}R : X → Y is given by x(Tr_{Z}R)y iff there exist z_{1}, …, z_{n} ∈ Z, with n ≥ 0, such that xRz_{1}R … Rz_{n}Ry. The second traced monoidal structure is given by × as the product of sets, and for R : X × Z → Y × Z, Tr′_{Z}R : X → Y is given by x(Tr′_{Z}R)y iff there exists z ∈ Z such that (x, z)R(y, z). Both these traced monoidal structures restrict to Rel_{fin}. The goal of this section is to prove:

∗This research was done while the author was visiting BRICS, Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Theorem 1 There exists an embedding F : (Rel, +, Tr) → (Rel, ×, Tr′) of traced monoidal categories.

Let N = {0, 1, …} be the set of natural numbers with addition. For any set X, let [X → N]_{fin} denote the set of finitely supported X-tuples of natural numbers, i.e. the set of X-tuples (a_{x})_{x∈X} such that for all but finitely many x ∈ X, a_{x} = 0 (notice that these tuples could be regarded as finite multisets). If (a_{x})_{x}, (b_{y})_{y}, and (e_{xy})_{xy} are such tuples, then we write

b_{y} ⋯ b_{y′}
a_{x} e_{xy} ⋯ e_{xy′}
⋮  ⋮ ...  ⋮
a_{x′} e_{x′y} ⋯ e_{x′y′}

as a suggestive notation for

a_{x} = ∑_{y∈Y} e_{xy} for all x ∈ X and
b_{y} = ∑_{x∈X} e_{xy} for all y ∈ Y.

We use this notation for infinite as well as for finite index sets, which is justified since the tuples are finitely supported.

Lemma 2 There exist (e_{xy})_{xy} satisfying the above equations if and only if ∑_{x∈X} a_{x} = ∑_{y∈Y} b_{y}.

Proof: The “only if” direction is trivial, the other direction follows by induction on ∑_{x∈X} a_{x}. □

We now construct a functor F : Rel → Rel as follows. For any set X, let F X = [X → N]_{fin}. On morphisms R : X → Y, we define F R : F X → F Y to be the relation given by (a_{x})_{x} F R (b_{y})_{y} if and only if there exist (e_{xy})_{xy} such that e_{xy} ≠ 0 implies xRy for all x, y, and such that

b_{y} ⋯ b_{y′}
a_{x} e_{xy} ⋯ e_{xy′}
⋮  ⋮ ...  ⋮
a_{x′} e_{x′y} ⋯ e_{x′y′}

It is easy to see that if R : X → X is the identity relation, then (a_{x})_{x} F R (b_{x})_{x} iff for all x, a_{x} = b_{x}. Thus, F preserves identities. To see that F preserves composition^{1}, consider R : X → Y and S : Y → Z. Suppose (a_{x})_{x} F R (b_{y})_{y} F S (c_{z})_{z} via

\begin{aligned}& b_{y} & ⋯ & b_{y′} \\ a_{x} & e_{xy} & ⋯ & e_{xy′} \\ ⋮ & ⋮ & ... & ⋮ \\ a_{x′} & e_{x′y} & ⋯ & e_{x′y′} \end{aligned}  and  \begin{aligned}& c_{z} & ⋯ & c_{z′} \\ b_{y} & f_{yz} & ⋯ & f_{yz′} \\ ⋮ & ⋮ & ... & ⋮ \\ b_{y′} & f_{y′z} & ⋯ & f_{y′z′} \end{aligned}

such that e_{xy} ≠ 0 implies xRy, and f_{yz} ≠ 0 implies ySz. By Lemma 2, for every y ∈ Y there is (g_{xyz})_{xz} such that

f_{yz} ⋯ f_{yz′}
e_{xy} g_{xyz} ⋯ g_{xyz′}
⋮  ⋮  ...  ⋮
e_{x′y} g_{x′yz} ⋯ g_{x′yz′}

Let h_{x}z = ∑_{y} g_{xyz}. Then for all x ∈ X,

a_{x} = ∑_{y} e_{xy} = ∑_{y,z} g_{xyz} = ∑_{z} h_{xz},

1Since in any traced monoidal category, f; g = Tr((f ⊗ g); c), it would suffice to check this for the case where g = c.

and similarly c_{z} = ∑_{x} h_{xz} for all z ∈ Z. Thus

c_{z} ⋯ c_{z′}
a_{x} h_{xz} ⋯ h_{xz′}
⋮  ⋮ ...  ⋮
a_{x′} h_{x′z} ⋯ h_{x′z′}

Moreover, if h_{xz} ≠ 0 then there exists y such that g_{xyz} ≠ 0, hence e_{xy} ≠ 0 and f_{yz} ≠ 0, hence xRy and ySz, hence xRSz. Thus, (a_{x})_{x} F (RS) (c_{z})_{z}. This shows that (F R)(F S) ⊆ F (RS).

Conversely, assume that (a_{x})_{x} F (RS) (c_{z})_{z} via

c_{z} ⋯ c_{z′}
a_{x} h_{xz} ⋯ h_{xz′}
⋮  ⋮ ...  ⋮
a_{x′} h_{x′z} ⋯ h_{x′z′}

such that h_{xz} ≠ 0 implies xRSz. For each pair (x, z) such that xRSz, choose a particular y_{xz} ∈ Y such that xRy_{xz}Sz. Define

g_{xyz} = \{ \begin{matrix}h_{xz} & if y = y_{xz}, \\ 0 & else, \end{matrix}
b_{y} = ∑_{x,z} g_{xyz},
e_{xy} = ∑_{z} g_{xyz},
f_{yz} = ∑_{x} g_{xyz}.

Then

∑_{y} g_{xyz} = h_{xz},
∑_{x} e_{xy} = ∑_{x,z} g_{xyz} = b_{y},
∑_{y} e_{xy} = ∑_{y,z} g_{xyz} = ∑_{z} h_{xz} = a_{x},
∑_{y} f_{yz} = ∑_{x,y} g_{xyz} = ∑_{x} h_{xz} = c_{z},
∑_{z} f_{yz} = ∑_{x,z} g_{xyz} = b_{y},

thus

\begin{aligned}& b_{y} & ⋯ & b_{y′} \\ a_{x} & e_{xy} & ⋯ & e_{xy′} \\ ⋮ & ⋮ & ... & ⋮ \\ a_{x′} & e_{x′y} & ⋯ & e_{x′y′} \end{aligned}  and  \begin{aligned}& c_{z} & ⋯ & c_{z′} \\ b_{y} & f_{yz} & ⋯ & f_{yz′} \\ ⋮ & ⋮ & ... & ⋮ \\ b_{y′} & f_{y′z} & ⋯ & f_{y′z′} \end{aligned}

Moreover, if e_{xy} ≠ 0, then for some z, g_{xyz} ≠ 0, hence y = y_{xz}, hence xRy. Similarly, if f_{yz} ≠ 0, then ySz. It follows that (a_{x})_{x} F R (b_{y})_{y} F S (c_{z})_{z}, and thus F (RS) ⊆ (F R)(F S). We have shown that F is a functor.

Next, we show that F preserves the symmetric monoidal structure. On objects, F (X +Y) ≅ F (X)×F (Y) via the identification of (a_{i})_{i∈X+Z} with ((a_{x})_{x∈X}, (a_{z})_{z∈Z}). Moreover, F (0) ≅ 1. For morphisms, consider R : X → Y and S : Z → W. Then R + S : X + Z → Y + W. Assume ((a_{x})_{x}, (c_{z})_{z}) F (R + S) ((b_{y})_{y}, (d_{w})_{w}) via

b_{y} ⋯ b_{y′} d_{w} ⋯ d_{w′}
a_{x} e_{xy} ⋯ e_{xy′} e_{xw} ⋯ e_{xw′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
a_{x′} e_{x′y} ⋯ e_{x′y′} e_{x′w} ⋯ e_{x′w′}
c_{z} e_{zy} ⋯ e_{zy′} e_{zw} ⋯ e_{zw′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
c_{z′} e_{z′y} ⋯ e_{z′y′} e_{z′w} ⋯ e_{z′w′}

where e_{ij} ≠ 0 implies i(R + S)j. Thus, in particular, e_{xw} = 0 for all x ∈ X and w ∈ W, and e_{yz} = 0 for all y ∈ Y and z ∈ Z. Hence (a_{x})_{x} F R (b_{y})_{y} and (c_{z})_{z} F R (d_{w})_{w}. The converse is also trivial, and thus we have F (R + S) = F R × F S. Last, F preserves the canonical isomorphisms for associativity, unit, and symmetry.

We will now show that F preserves trace. Consider R : X + Z → Y + Z and let Q = Tr_{Z}R : X → Y. First, suppose that (a_{x})_{x} F Q (b_{y})_{y} via

b_{y} ⋯ b_{y′}
a_{x} e_{xy} ⋯ e_{xy′}
⋮  ⋮ ...  ⋮
a_{x′} e_{x′y} ⋯ e_{x′y′}

where e_{xy} ≠ 0 implies xQy. Now choose a set of words A ⊆ X × Z^{∗} × Y such that

1. whenever xz_{1} … z_{n}y ∈ A, then xRz_{1}R … Rz_{n}Ry, and

2. for each pair (x, y) with xQy, there is exactly one word xz_{1} … z_{n}y ∈ A.

If w and w′ are words, then we say w is a subword of w′, in symbols w ◁ w′, if there exist words u and v such that uwv = w′. In the following, we denote words in Z^{∗} by ξ. For i ∈ X + Z and j ∈ Y + Z, define

f_{ij} = ∑{e_{xy} | ij ◁ xξy ∈ A},
c_{z} = ∑{e_{xy} | z ◁ xξy ∈ A}.

Notice that these sums are finite, because only finitely many e_{xy} ≠ 0. Then

∑_{j∈Y +Z} f_{xj} = ∑_{y | xξy∈A} e_{xy} = ∑_{y | xQy} e_{xy} = ∑_{y} e_{xy} = a_{x},
∑_{i∈X+Z} f_{iy} = ∑_{x | xξy∈A} e_{xy} = ∑_{x | xQy} e_{xy} = ∑_{x} e_{xy} = b_{y},
∑_{j∈Y +Z} f_{zj} = ∑_{x,y | z◁xξy∈A} e_{xy} = c_{z},
∑_{i∈X+Z} f_{iz} = ∑_{x,y | z◁xξy∈A} e_{xy} = c_{z}.

Thus

b_{y} ⋯ b_{y′} c_{z} ⋯ c_{z′}
a_{x} f_{xy} ⋯ f_{xy′} f_{xz} ⋯ f_{xz′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
a_{x′} f_{x′y} ⋯ f_{x′y′} f_{x′z} ⋯ f_{x′z′}
c_{z} f_{zy} ⋯ f_{zy′} f_{zz} ⋯ f_{zz′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
c_{z′} f_{z′y} ⋯ f_{z′y′} f_{z′z} ⋯ f_{z′z′}

Moreover, if f_{ij} ≠ 0, then there exists xξy ∈ A with ij ◁ xξy, hence iRj by definition of A. Thus, it follows that ((a_{x})_{x}, (c_{z})_{z}) F R ((b_{y})_{y}, (c_{z})_{z}), and therefore (a_{x})_{x} Tr′_{F Z}(F R) (b_{y})_{y}. This shows F (Tr_{Z}R) ⊆ Tr′_{F Z}(F R).

For the converse, assume that (a_{x})_{x} Tr′_{F Z}(F R) (b_{y})_{y} holds. By definition of Tr′, there exists (c_{z})_{z} such that ((a_{x})_{x}, (c_{z})_{z}) F R ((b_{y})_{y}, (c_{z})_{z}). Let (f_{ij})_{i∈X+Z,j∈Y +Z} be such that f_{ij} ≠ 0 implies iRj and

b_{y} ⋯ b_{y′} c_{z} ⋯ c_{z′}
a_{x} f_{xy} ⋯ f_{xy′} f_{xz} ⋯ f_{xz′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
a_{x′} f_{x′y} ⋯ f_{x′y′} f_{x′z} ⋯ f_{x′z′}
c_{z} f_{zy} ⋯ f_{zy′} f_{zz} ⋯ f_{zz′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
c_{z′} f_{z′y} ⋯ f_{z′y′} f_{z′z} ⋯ f_{z′z′}

Again, let Q = Tr_{Z}R. We will show that (a_{x})_{x} F Q (b_{y})_{y} by induction on ∑_{z} c_{z}. We distinguish three cases:

• Case 1: ∑_{z} c_{z} = 0. Then for all i, j, z, f_{iz} = 0 and f_{zj} = 0, hence

b_{y} ⋯ b_{y′}
a_{x} f_{xy} ⋯ f_{xy′}
⋮  ⋮ ...  ⋮
a_{x′} f_{x′y} ⋯ f_{x′y′}

and f_{xy} ≠ 0 implies xRy implies xQy, hence we are done.

• Case 2: There exists n ≥ 2 and distinct z_{1}, …, z_{n} ∈ Z such that f_{z_{1}z_{2}}, …, f_{z_{n−1}z_{n}}, f_{z_{n},z_{1}} ≠ 0. Define

c′_{z} = \{ \begin{matrix}c_{z} − 1 & if z ∈ z_{1}, …, z_{n}, \\ c_{z} & else, \end{matrix}

f′_{ij} = \{ \begin{matrix}f_{ij} − 1 & if ij ◁ z_{1} … z_{n}z_{1}, \\ f_{ij} & else. \end{matrix}

Then

b_{y} ⋯ b_{y′} c′_{z} ⋯ c′_{z′}
a_{x} f′_{xy} ⋯ f′_{xy′} f′_{xz} ⋯ f′_{xz′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
a_{x′} f′_{x′y} ⋯ f′_{x′y′} f′_{x′z} ⋯ f′_{x′z′}
c′_{z} f′_{zy} ⋯ f′_{zy′} f′_{zz} ⋯ f′_{zz′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
c′_{z′} f′_{z′y} ⋯ f′_{z′y′} f′_{z′z} ⋯ f′_{z′z′}

holds and f′_{ij} ≠ 0 still implies iRj, moreover ∑_{z} c′_{z} < ∑_{z} c_{z}. By induction hypothesis, we get (a_{x})_{x} F Q (b_{y})_{y}.

• Case 3: Since we are not in Case 1, we can assume that there is i_{0} ∈ Z such that c_{i_{0}} ≠ 0. Inductively suppose that we are given i_{k} ∈ Z such that c_{i_{k}} ≠ 0, then there is i_{k+1} ∈ X + Z such that f_{i_{k+1}i_{k}} ≠ 0, and thus also c_{i_{k+1}} ≠ 0. In this manner, we construct a sequence i_{0}, i_{1}, i_{2}, . . .. Since we are not in Case 2, this sequence is non-repeating, and since only finitely many c_{z} are different from 0, the sequence must eventually stop with some i_{k} ∈ X. Proceeding from i_{0} in the other direction, we can construct a similar sequence, so that in the end we get a path x̂z_{0} … z_{n}ŷ with f_{x̂z_{0}}, f_{z_{0}z_{1}}, …, f_{z_{n}ŷ} ≠ 0. Define

a′_{x} = \{ \begin{matrix}a_{x} − 1 & if x = x̂, \\ a_{x} & else, \end{matrix}

b′_{y} = \{ \begin{matrix}b_{y} − 1 & if y = ŷ, \\ b_{y} & else, \end{matrix}

c′_{z} = \{ \begin{matrix}c_{z} − 1 & if z ∈ z_{0}, …, z_{n}, \\ c_{z} & else, \end{matrix}

f′_{ij} = \{ \begin{matrix}f_{ij} − 1 & if ij ◁ x̂z_{0} … z_{n}ŷ, \\ f_{ij} & else. \end{matrix}

Then

b′_{y} ⋯ b′_{y′} c′_{z} ⋯ c′_{z′}
a′_{x} f′_{xy} ⋯ f′_{xy′} f′_{xz} ⋯ f′_{xz′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
a′_{x′} f′_{x′y} ⋯ f′_{x′y′} f′_{x′z} ⋯ f′_{x′z′}
c′_{z} f′_{zy} ⋯ f′_{zy′} f′_{zz} ⋯ f′_{zz′}
⋮  ⋮ ...  ⋮  ⋮ ...  ⋮
c′_{z′} f′_{z′y} ⋯ f′_{z′y′} f′_{z′z} ⋯ f′_{z′z′}

and f′_{ij} ≠ 0 still implies iRj; moreover ∑_{z} c′_{z} < ∑_{z} c_{z}. By induction hypothesis, we get (a′_{x})_{x} F Q (b′_{y})_{y} via some

b′_{y} ⋯ b′_{y′}
a′_{x} e′_{xy} ⋯ e′_{xy′}
⋮  ⋮ ...  ⋮
a′_{x′} e′_{x′y} ⋯ e′_{x′y′}

where e′xy ≠ 0 implies xQy. Now let

e_{xy} = \{ \begin{matrix}e′_{xy} + 1 & if x = x̂ and y = ŷ, \\ e′_{xy} & else. \end{matrix}

Then

b_{y} ⋯ b_{y′}
a_{x} e_{xy} ⋯ e_{xy′}
⋮  ⋮ ...  ⋮
a_{x′} e_{x′y} ⋯ e_{x′y′}

and if e_{xy} ≠ 0, then either e′_{xy} ≠ 0, in which case xQy, or else x = x̂ and y = ŷ. But, by construction, x̂Rz_{0}R … Rz_{n}Rŷ, and thus xQy. Thus (a_{x})_{x} F Q (b_{y})_{y}, which shows that Tr′_{F Z}(F R) ⊆ F (Tr_{Z}R), thereby finishing the proof of Theorem 1. □

There is no embedding of (Rel_{fin}, +, Tr) into (Rel_{fin}, ×, Tr′)

In this section, we will show that Bainbridge’s construction cannot be made into a functor from (Rel, +, Tr) into (Rel, ×, Tr′). More generally:

Theorem 3 There exists no embedding F : (Rel_{fin}, +, Tr) → (Rel_{fin}, ×, Tr′) of traced monoidal categories.

Notice that this theorem implies that there is no embedding of (Rel, +, Tr) into (Rel, ×, Tr′) which is given by the power set operation on objects.

For any finite set N, let F_{N} : (Rel_{fin}, +) → (Rel_{fin}, ×) be the symmetric monoidal functor that is given on objects by F_{N}X = N^{X} and on morphisms by (a_{x})_{x∈X} F_{N}R (b_{y})_{y∈Y} iff for all x, y, xRy implies a_{x} = b_{y}. One checks that the functor F_{N} preserves trace if and only if N ≠ ∅. However, F_{N} is never an embedding.

For an arbitrary symmetric monoidal functor F : (Rel_{fin}, +) → (Rel_{fin}, ×), we will show that if F preserves trace, then it is naturally isomorphic to F_{N} for some N. In particular, there is no traced monoidal embedding F : (Rel_{fin}, +, Tr) → (Rel_{fin}, ×, Tr′).

Given such a functor F, let N = F (1). Notice that any object X in Rel_{fin} is of the form X = 1 + 1 + … + 1, and thus, F X = N × N × … × N = N^{X}. For any two objects X and Y, let ∇_{XY}: N^{X} → N^{Y} = F (⊤_{XY}) be the image of the full relation ⊤_{XY} : X → Y, i.e.of the relation ⊤_{XY} = X × Y.

Notice that F is completely determined (up to natural isomorphism) by N and the relations ∇_{XY}, because any morphism R : X → Y in Rel can be written as

X = ∑_{x∈X} 1 \underrightarrow{∑_{x} ⊤_{1Y}} ∑_{x∈X} Y ≅ ∑_{x∈X,y∈Y} 1 \underrightarrow{∑_{xy} R_{xy}} ∑_{x∈X,y∈Y} 1 ≅ ∑_{y∈Y} X \underrightarrow{∑_{y} ⊤_{X1}} ∑_{y∈Y} 1 = Y,

where

R_{xy} : 1 → 1 = \{ \begin{matrix}id_{1} & if xRy, \\ 1 ⟶^{⊤_{10}} 0 ⟶^{⊤_{01}} 1 & else. \end{matrix}

Thus, F R can be computed from ∇_{XY} via

N^{X} = ∏_{x∈X} N \underrightarrow{∏_{x}∇_{1Y}} ∏_{x∈X} N^{Y} ≅ ∏_{x∈X,y∈Y} N \underrightarrow{∏_{xy} F (R_{xy})} ∏_{x∈X,y∈Y} N ≅ ∏_{y∈Y} N^{X} \underrightarrow{∏_{y}∇_{X1}} ∏_{y∈Y} N = Y,

where

F (R_{xy}) : N → N = \{ \begin{matrix}id_{N} & if xRy, \\ N ⟶^{∇_{10}} 1 ⟶^{∇_{01}} N & else. \end{matrix}

Let • be a tag such that • ∉ N. We extend the relations ∇_{XY} to ∇_{XY}^{•} ⊆ (N + {•})^{X} × (N + {•})^{Y} by setting (a_{x})_{x} ∇_{XY}^{•} (b_{y})_{y} if and only if there exist (a′_{x})_{x} and (b′_{y})_{y} such that (a′_{x})_{x} ∇_{XY} (b′_{y})_{y} and

a′_{x} = a_{x} if a_{x} ≠ •,
a′_{x} ∈ ∇_{01} if a_{x} = •,
b′_{y} = b_{y} if b_{y} ≠ •,
b′_{y} ∈ ∇_{10} if b_{y} = •.

If (a_{x})_{x∈X} and (b_{y})_{y∈Y} are tuples in N, and (e_{xy})_{x∈X,y∈Y} is a tuple in N + {•}, we will write

b_{y} ⋯ b_{y′}
a_{x} e_{xy} ⋯ e_{xy′}
⋮  ⋮ ...  ⋮
a_{x′} e_{x′y} ⋯ e_{x′y′}

as an abbreviation for

a_{x} ∇_{1Y}^{•} (e_{xy})_{y} for all x ∈ X and
(e_{xy})_{x} ∇_{X1}^{•} b_{y}  for all y ∈ Y,

Lemma 4 (a_{x})_{x} F R (b_{y})_{y} if and only if there exist a tuple (e_{xy})_{x∈X,y∈Y} of elements of N + {•}, such that e_{xy} ≠ • iff xRy, and such that

b_{y} ⋯ b_{y′}
a_{x} e_{xy} ⋯ e_{xy′}
⋮  ⋮ ...  ⋮
a_{x′} e_{x′y} ⋯ e_{x′y′}

Proof: We already know that (a_{x})_{x} F R (b_{y})_{y} if and only if

(a_{x})_{x} (∏_{x} ∇_{1Y}; ∏_{xy} F (R_{xy}); ∏_{y} ∇_{X1}) (b_{y})_{y},

which is the case if and only if there exist (e′_{xy})_{x∈X,y∈Y} and (e′_{xy})_{x∈X,y∈Y} from N such that

a_{x} ∇_{1Y} (e′_{xy})_{y}  for all x ∈ X,
e′_{xy} = e′′_{xy}  for all xRy,
e′_{xy} ∈ ∇_{10} and e′′_{xy} ∈ ∇_{01} for all x R̸ y,
(e′′_{xy})_{x} ∇_{X1} b_{y}  for all y ∈ Y.

Now letting e_{xy} = e′_{xy} = e′′_{xy} if xRy, and e_{xy} = • if x R̸ y, the claim follows. □ Lemma 5 The following statements, along with their duals, are properties of the relations ∇_{XY}:

1. For all (a_{x})_{x} and all permutations ϕ : X → X, one has b ∇_{1X} (a_{x})_{x} iff b ∇_{1X} (a_{ϕx})_{x}.

2. If e ∈ ∇_{10}, then a ∇_{1,X+1} (b_{1}, …, b_{X}, e) implies a ∇_{1,X} (b_{1}, …, b_{X}). Conversely, whenever a ∇_{1,X} (b_{1}, …, b_{X}), then there exists an e ∈ ∇_{10} such that a ∇_{1,X+1} (b_{1}, …, b_{X}, e). (Actually, e depends only on a, but we don’t need this fact).

3. For every b ∈ N, and every n ≥ 1, there exists (a_{1}, …, a_{n}) such that b ∇_{1n} (a_{1}, …, a_{n}) ∇_{n1} b.

4. For every b ∈ N and every n ≥ 1, there exists a ∈ N such that (b, …, b) ∇_{n1} a ∇_{1n} (b, …, b).

5. If ∇_{01}≠ N, then there exist a, b ∈ N such that a ∇_{12} (b, a) and b ∉ ∇_{01}. Proof:

1. Consider the following two diagrams. The left diagram communtes in (Rel_{fin}, +). By applying F, one gets the right diagram in (Rel_{fin}, ×):

\xymatrix{1 \ar[r]^{⊤_{1X}} \ar[dr]_{⊤_{1X}} & X \ar[d]^{ϕ} \\  & X}  ⇒  \xymatrix{N \ar[r]^{^{∇^{1X}}} \ar[dr]_{_{∇_{1X}}} & N^{X} \ar[d]^{F ϕ} \\  & N^{X}.}

But since ϕ is given in terms of the symmetric monoidal structure, F ϕ behaves as expected, which implies the claim.

2. Again, commutativity of the left diagram implies commutativity of the right one:

\xymatrix{1 \ar[r]^{⊤_{1,X+1}} \ar[dr]_{⊤_{1X}} & X + 1 \ar[d]^{id+⊤_{10}} \\  & X}  ⇒  \xymatrix{N \ar[r]^{^{∇^{1,X+1}}} \ar[dr]_{_{∇_{1X}}} & N^{X} × N \ar[d]^{id×∇_{10}} \\  & N^{X},}

Thus, a ∇_{1,X} (b_{1}, …, b_{X}) iff there exists e ∈ ∇_{01} with a ∇_{1,X+1} (b_{1}, …, b_{X}, e), which was the claim.

3. Again, we transfer a diagram from (Rel_{fin}, +) to (Rel_{fin}, ×) along F:

\xymatrix{1 \ar[r]^{⊤_{1n}} \ar[dr]_{id} & n \ar[d]^{⊤_{n1}} \\  & 1}  ⇒  \xymatrix{N \ar[r]^{^{∇^{1n}}} \ar[dr]_{id} & N^{n} \ar[d]^{_{∇_{n1}}} \\  & N.}

The claim follows.

4. Suppose b ∈ N and n ≥ 1 are given. By (3), there is (a_{1}, …, a_{n}) such that b ∇_{1n} (a_{1}, …, a_{n}) ∇_{n1} b. Then

b b ⋯  b  b
b a_{1} a_{2} ⋯ a_{n−1} a_{n}
b a_{n} a_{1} ⋯ a_{n−2} a_{n−1}
⋮ ⋮ ⋮ ...  ⋮  ⋮
b a_{3} a_{4} ⋯ a_{1}  a_{2}
b a_{2} a_{3} ⋯ a_{n}  a_{1}

and thus (b, …, b) ∇_{nn} (b, …, b) by Lemma 4. But

\xymatrix{n \ar[r]^{⊤_{n1}} \ar[dr]_{⊤_{nn}} & 1 \ar[d]^{⊤_{1n}} \\  & n}  ⇒  \xymatrix{N^{n} \ar[r]^{^{∇^{n1}}} \ar[dr]_{_{∇_{nn}}} & N \ar[d]^{_{∇_{1n}}} \\  & N^{n},}

and hence there exists a ∈ N such that (b, …, b) ∇_{n1} a ∇_{1n} (b, …, b).

5. Suppose there is some c ∈ N with c ∉ ∇_{01}. For each n ≥ 1, use (4) to choose d_{n} ∈ N such that (c, …, c) ∇_{n1} d_{n} ∇_{1n} (c, …, c). Since N is finite, there must be n, m ≥ 1 such that d_{n} = d_{n+m}. Now let a = d_{n} = d_{n+m}, and let b = d_{m}. Then

a ∇_{1,n+m} (c, …^{n}, c, c, …^{m}, c) (∇_{n1} × ∇_{m1}) (a, b).

But we have

\xymatrix{1 \ar[r]^{⊤_{1,n+m}} \ar[dr]_{⊤_{12}} & n + m \ar[d]^{⊤_{n1}+⊤_{m1}} \\  & 1 + 1}  ⇒  \xymatrix{N \ar[r]^{^{∇^{1,n+m}}} \ar[dr]_{_{∇_{12}}} & N^{n} × N^{m} \ar[d]^{∇_{n1}×∇_{m1}} \\  & N × N,}

and hence it follows that a ∇_{12} (a, b). Moreover, suppose b ∈ ∇_{01}. Because b ∇_{1m} (c, …^{m}, c), it follows that

(c, …^{m}, c) ∈ ∇_{0m}. But

⊤_{0m} = 0 ⟶^{⊤_{01}+...+⊤_{01}} m
⇒  ∇_{0m} = 1 ⟶^{∇_{01}×...×∇_{01}} N^{m},

hence c ∈ ∇_{01}, a contradiction. □

Up to this point, we have derived properties of an arbitrary symmetric monoidal functor F : (Rel_{fin}, +) → (Rel_{fin}, ×). Notice that the only time we have used the finiteness of N was in the last part of Lemma 5. Now, assume that F preserves trace. We will show that ∇_{01}= N. By way of contradiction, assume that ∇_{01}≠ N. Then, by Lemma 5(5), there exist a, b ∈ N with a ∇_{12} (b, a) and b ∉ ∇_{01}. Moreover, we can easily find c, d ∈ N with (c, d) ∇_{21} c, for instance by Lemma 5(2). Now let X = {x}, Y = {y}, and Z = {z_{1}, z_{2}}. Consider the relation R : X + Z → Y + Z given by the matrix

R = ( \begin{matrix}0 & 0 & 1 \\ 1 & 1 & 0 \\ 0 & 0 & 1 \end{matrix} )

i.e., xRz_{2}, z_{2}Rz_{2}, z_{1}Rz_{1}, and z_{1}Ry. From a ∇_{12} (b, a) and (c, d) ∇_{21} c, with Lemma 5(2), it follows that

\begin{aligned}& b & a & c \\ d & • & • & d \\ a & b & a & • \\ c & • & • & c \end{aligned}

and thus, by Lemma 4, (d, a, c)F R(b, a, c). By definition of the trace on (Rel_{fin}, ×, Tr′), it follows that d Tr′_{F Z}(F R) b. Since F preserves trace, we must have d F (Tr_{Z}R) b. But notice that Tr_{Z}R : X → Y is the empty relation. From d F (∅) b, it follows by Lemma 4 that b ∈ ∇_{01}, a contradiction. Therefore, it must have been the case that ∇_{01}= N.

By the dual argument, we also have ∇_{10}= N. Now we can apply Lemma 5(2) to arbitrary e ∈ N, and by repeatedly doing so, it follows that for all a and (b_{y})_{y}, if a ∇_{1Y} (b_{y})_{y}, then a = b_{y} for all y ∈ Y. (Note that ∇_{11}=id_{N}). Conversely, if (b_{y})_{y} is a constant tuple, then by Lemma 5(4), there exists a with a ∇_{1Y} (b_{y})_{y}. Thus

a ∇_{1Y} (b_{y})_{y} if and only if a = b_{y} for all y ∈ Y .

Similarly, the dual statement holds, and by writing ∇_{XY} =∇_{X1}∇_{1Y}, we get

(a_{x})_{x} ∇_{XY} (b_{y})_{y} if and only if a_{x} = b_{y} for all x ∈ X, y ∈ Y .

From here, it is easily seen that F is naturally isomorphic to the functor F_{N} defined at the beginning of this section (recall that F is uniquely determined by N and the relations ∇_{XY}). This concludes the proof of Theorem 3. □

Additional challenges

Notice that the proof of Theorem 3 only uses the trace of one particular matrix, namely

R = ( \begin{matrix}0 & 0 & 1 \\ 1 & 1 & 0 \\ 0 & 0 & 1 \end{matrix} )

Can one extract from this proof a universal sentence (in the predicates of traced monoidal categories and equality) which holds in (Rel_{fin}, ×, Tr′) but not in (Rel_{fin}, +, Tr)? Such a (possibly infinite) sentence must exist by abstract algebraic nonsense. But a nice such sentence would yield a possibly more elegant proof of the non-embedding theorem.

References

[1] E. S. Bainbridge. Feedback and generalized logic. Information and Control, 31:75–96, 1976.

[2] A. Joyal, R. Street, and D. Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119:447–468, 1996.