Definition of partial trace

Given a symmetric monoidal category C: with a full subcategory (not necessarily symmetric monoidal) TC:

U : TC C

a partial trace is a natural transformation:

TrX Y A : C[X U A, Y U A] C[X, Y]

satisfying certain axioms (given below, since they are much simpler to present graphically than equationally).

As an example, the categories Cpo Cpo (where the inclusion maps D to D) have a partial trace given by fixed points.

As another example, given a generator with a subset of sorts defined to be traceable we can let C be the category of flow graphs over that generator where any cycle through the graph must pass through at least one edge labelled with a traceable sort, and TC be the full subcategory where the objects are traceable sorts. These categories have a partial trace given by forming a feedback loop:

We shall provide a different axiomatization of traces than that provided by Joyal, Street and Verity, but we shall show below that in the case when C and TC are the same category, we recover their definition. Note that these axioms are all graph isomorphisms, and indeed are a complete axiomatization for graph isomorphism.

Naturality in X (for f : X' X and g : X U A Y U A in C):

| = |
f; TrX Y A (g) | = | TrX' Y A (f idU A; g)

Naturality in Y (for f : Y Y' and g : X U A Y U A in C):

| = |
TrX Y A (g); f | = | TrX Y' A (g; f idU A)

Yanking:

| = |
TrU(A) U(A) A (symmU(A) U(A)) | = | idU(A)

Symmetry sliding (for f : X U(A) U(B) Y U(B) U(A)):

| = |
TrX Y A (Tr(X U(A)) (Y U(A)) B (f; (idY symmU(B) U(A))) | = | TrX Y B (Tr(X U(B)) (Y U(B)) A ((idX symmU(B) U(A)); f)

Strength (for f : V W and g : X U A Y U A in C):

| = |
f TrX Y A (g) | = | Tr(V X) (W Y) A (f g)

For those readers familiar with Joyal, Street and Verity's axiomatization of a trace, the above axioms are obviously derivable from theirs. Moreover, the following lemmas show that we can derive their axiomatization, so in the case where TC and C coincide, our axiomatization is the same as theirs.

Lemma (Parameterized dinaturality) (for f : Z U(B) U(A) and g : X U(A) Y U(B) in C):

| = |
Tr(X Z) Y A ((idX symmZ U(A)); (g idZ); (idY (symmU(B) Z); f))) | = | Tr(X Z) Y B ((idX f); g)

Proof.

Corollary (Dinaturality) (for f : U(B) U(A) and g : X U(A) Y U(B) in C):

| = |
TrX Y A (g; (idY f)) | = | TrX Y B ((idX f); g)

Proof. Let Z be I in the above.

Lemma (Trace respects unit) (for f : I U A and g : X U A Y in C):

| = |
TrX Y A (g; idY f) | = | (idX f); g

Proof.

Lemma (Trace respects tensor) (for f : U(B) U(C) U(A) and g : X U(A) Y U(B) U(C) in C):

| = |
TrX Y A (g; idY f) | = | TrX Y C (TrX Y B ((idX f); g))

Proof.

Lemma (Trace respects double symmetry) (for f : V W and g : X U A Y U A in C):

| = |
TrX Y A (g) f | = | Tr(X V) (Y W) A ((idX symmV U(A)); (g f); (idY symmU(A) W))

Proof.

Previous | Next