nLab traced monoidal category

Contents

Context

Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

Contents

Idea

The concept of traced monoidal category axiomatizes the structure on a monoidal category for it to have a sensible notion of (partial) trace the way it exists canonically in compact closed categories. Traced monoidal categories sometimes only have right or left traces, and are referred to as right traced or left traced respectively. A category with compatible right and left traces is called a planar traced category. If the right and left traces agree, then we call a planar traced category spherical.

Graphically, the trace of an endomorphism f:A→Af:A\to A is represented by the closed loop

The ambiguity in whether to close the loop to the right or to the left is codified in the difference between left and right traced categories. Every pivotal category can be canonically made into a planar traced category by using its implicit distinguished morphisms to close loops. Pivotal categories which induce spherical traced structures are known as spherical categories. In this way, traced monoidal categories generalize the trace operation to categories which do not necessarily have duals.

In denotational semantics of programming languages, the trace is used to model recursion, though if the language is not substructural?, then this can be simplified to a fixed point operator.

Definition

The original definition due to (Joyal-Street-Verity 96) is stated in the setting of balanced monoidal categories. Here we present a very general formulation, as given in Selinger’s survey.

A monoidal category π’ž\mathscr{C} is said to be right traced if it is equipped with family of operations

tr R X:Hom(AβŠ—X,BβŠ—X)β†’hom(A,B)\tr^X_R:\text{Hom}(A\otimes X,B\otimes X)\to \text{hom}(A,B)

for all A,B,Xβˆˆπ’³A,B,X\in \mathscr{X}, satisfying the following four axioms:

  • Tightening (naturality in A,BA,B) For all A,B,C,D,Xβˆˆπ’žA,B,C,D,X\in\mathscr{C}, g:Aβ†’Bg:A\to B, f:BβŠ—Xβ†’CβŠ—Xf:B\otimes X\to C\otimes X, h:Cβ†’Dh:C\to D
tr R X((gβŠ—id X)∘f∘(hβŠ—id X))=g∘tr R X(f)∘h\tr_R^X((g\otimes \text{id}_X)\circ f\circ (h\otimes \text{id}_X))=g\circ \tr_R^X(f)\circ h
  • Sliding (naturality in XX) for all A,B,X,Y∈A,B,X,Y\in , f:AβŠ—Xβ†’BβŠ—Yf:A\otimes X\to B\otimes Y, g:Yβ†’Xg:Y\to X
tr R X((id BβŠ—g)∘f)=tr R Y(f∘(id AβŠ—g))\tr_R^{X}((\text{id}_B\otimes g)\circ f)=\tr_R^{Y}(f\circ (\text{id}_A\otimes g))
  • Vanishing For all A,B,X,Yβˆˆπ’žA,B,X,Y\in \mathscr{C},
tr R 1(f)=f,βˆ€f:Aβ†’B\tr^1_R(f)=f,\,\, \forall \, f:A\to B

and

tr R XβŠ—Y(f)=tr R X(tr R Y(f))\tr^{X\otimes Y}_R(f)=\tr_R^X(\tr_R^Y(f))

for all f:AβŠ—XβŠ—Yβ†’BβŠ—XβŠ—Yf:A\otimes X\otimes Y\to B\otimes X\otimes Y.

  • Strength For all A,B,C,D,Xβˆˆπ’žA,B,C,D,X\in \mathscr{C}, f:CβŠ—Xβ†’DβŠ—Xf:C\otimes X\to D\otimes X, g:Aβ†’Bg:A\to B
tr R X(gβŠ—f)=gβŠ—tr R X(f)\tr_R^X(g\otimes f)=g\otimes \tr_R^X(f)

Graphically, we fix the notation for right trace

The above axioms are described with the following pictures:

In the presence of a braiding (such as in a symmetric monoidal category), we additionally require a yanking axioms:

  • Yanking: Tr X(Ξ² X,X)=id XTr^X(\beta_{X,X}) = id_X for all Xβˆˆπ’žX\in\mathscr{C}

where Ξ²:XβŠ—Xβ†’XβŠ—X\beta:X\otimes X\to X\otimes X is the briading.

A left traced category is defined similarly, with a family of morphisms

tr L X:Hom(XβŠ—A,XβŠ—B)β†’Hom(A,B)\tr_L^X:\text{Hom}(X\otimes A,X\otimes B)\to \text{Hom}(A,B)

satisfying symmetric axioms. We write the left trace graphically as

A planar traced category is a monoidal category π’ž\mathscr{C} which is simultaneously left and right traced, such that the following axioms are satisfied:

  • Interchange For all A,B,X,Yβˆˆπ’žA,B,X,Y\in \mathscr{C}, f:YβŠ—AβŠ—Xβ†’YβŠ—BβŠ—Xf:Y\otimes A\otimes X\to Y\otimes B\otimes X
tr R X(tr L Y(f))=tr L Y(tr R X(f)).\tr_R^X(\tr_L^Y(f))=\tr_L^Y(\tr_R^X(f)).
  • Left pivoting For all A,Bβˆˆπ’žA,B\in\mathscr{C}, f:1β†’AβŠ—Bf:1\to A\otimes B
tr R B(id BβŠ—f)=tr L A(fβŠ—id A).\tr_R^B(\text{id}_B\otimes f)=\tr_L^A(f\otimes \text{id}_A).
  • Right pivoting For all A,Bβˆˆπ’žA,B\in\mathscr{C}, f:AβŠ—Bβ†’1f:A\otimes B\to 1
tr R B(id BβŠ—f)=tr L A(fβŠ—id A).\tr_R^B(\text{id}_B\otimes f)=\tr_L^A(f\otimes \text{id}_A).

Graphically, these axioms can be stated as below:

It is from these axioms that pivotal categories get their name.

A spherical trace category is a planar traced category in which the left and right partial traces agree. That is, for any endomorphism f:Aβ†’Af:A\to A in π’ž\mathscr{C} we have that

tr R A(f)=tr L A(f).\tr_R^A(f)=\tr_L^A(f).

Examples

  • The category of finite-dimensional vector spaces is traced monoidal. In skeletal form, the objects are natural numbers regarded as dimensions, morphisms are matrices regarded as linear maps, and tensor product is multiplication of the dimensions. The trace is a minor generalization of matrix trace:

    Tr m,n p((a (i,k),(j,kβ€²)) (i,k),(j,kβ€²)∈mΓ—pΓ—nΓ—p) i,j=βˆ‘ k=1 pa (i,k),(j,k). Tr_{m,n}^p((a_{(i,k),(j,k')})_{(i,k),(j,k')\in m\times p\times n\times p})_{i,j}= \sum_{k=1}^p a_{(i,k),(j,k)}.

    This is an instance of a trace in a compact closed category.

  • The category of profunctors is also compact closed, hence traced monoidal (actually a bicategory, though). The trace of a profunctor H:(BΓ—X) opΓ—AΓ—Xβ†’SetH:(B\times X)^{op} \times A\times X\to \mathbf{Set} is the profunctor Tr A,B X(H):B opΓ—Aβ†’SetTr_{A,B}^X(H):B^{op}\times A\to \mathbf{Set} given by the coend formula:

    Tr(H)(b,a)=∫ xH(b,x,a,x). Tr(H)(b,a)=\int^x H(b,x,a,x) .
  • The category of sets and partial functions with the coproduct monoidal structure is traced, if we let the trace of a partial function f:A+Xβ†’B+Xf:A+X\to B+X be defined as follows. First, let f A,B:Aβ†’Bf_{A,B}:A\to B, f X,X:Xβ†’Xf_{X,X}:X\to X and so on be the evident partial functions that come from restricting the domain and codomain of ff. Then define

    Tr A,B X(f)(a)=bTr_{A,B}^X(f)(a)=b

    if either f A,B(a)=bf_{A,B}(a)=b or if there exists nn such that b=f X,B(f X,X n(f A,X(a)))b=f_{X,B}(f_{X,X}^n(f_{A,X}(a))). See for instance Section 5.2 of (Abramsky, Haghverdi and Scott). This is an example of a partially additive category.

    This is a basis for a categorical semantics of β€œwhile loops” in programming languages: we keep applying ff while it is returning in XX.

  • Consider the category of pointed cpoβ€˜s and continuous functions. A pointed cpo is a poset with a bottom element βŠ₯\bot and least upper bounds of Ο‰\omega-chains. The morphisms preserve least upper bounds of chains but are not required to preserve bottom elements. This is a cartesian monoidal category, and with this structure it is traced, if we let the trace of a continuous function f:AΓ—Xβ†’BΓ—Xf:A\times X\to B\times X be given as follows. First, for fixed a∈Aa\in A, let x a∈Xx_a\in X be the least fixed point of (Ο€ 2β‹…f(a,βˆ’)):Xβ†’X(\pi_2\cdot f(a,-)):X\to X, writing Ο€ 2\pi_2 for the second product projection. Here the least fixed point exists by Tarski’s fixed point theorem, indeed

    x a=⋁ n(Ο€ 2β‹…f(a,βˆ’)) n(βŠ₯).x_a=\bigvee_n(\pi_2\cdot f(a,-))^n(\bot).

    Then we let

    Tr A,B X(f)(a)=Ο€ 1(f(a,x a))∈BTr_{A,B}^X(f)(a)=\pi_1(f(a,x_a))\in B

    In Haskell notation, where β€˜let’ allows recursive definitions, we can more swiftly just write

    Tr A,B X(f)(a)=let(b,x)=f(a,x)inbTr_{A,B}^X(f)(a)\ \ \ = \ \ \ let\ (b,x)=f(a,x)\ in\ b

    (except that the built-in product types in Haskell are lifted products rather than categorical products: (A,B)(A,B) in Haskell is like AΓ—BA\times B but with an extra bottom element added).

    This is an example of a cartesian category with a parameterized fixed point operator (Hasegawa 1997).

Properties

Relation to compact closed categories

Every compact closed category is equipped with a canonical trace defined by

Tr A,B X(f)=Aβ†’idβŠ—Ξ·AβŠ—XβŠ—X *β†’fβŠ—idBβŠ—XβŠ—X *β†’idβŠ—Ξ΅β€²B Tr_{A,B}^X(f) = A \overset{id\otimes \eta}{\to} A \otimes X \otimes X^* \overset{f \otimes id}{\to} B \otimes X \otimes X^* \overset{id \otimes \varepsilon'}{\to} B

where Ξ·\eta is a unit and Ξ΅β€²\varepsilon' is a counit of appropriate adjunctions (note that the symmetry makes the dual X *X^* both a right and left adjoint of XX: the adjunctions are ambidextrous).

Conversely, given a traced monoidal category π’ž\mathcal{C}, there is a free construction completion of it to a compact closed category Int(π’ž)Int(\mathcal{C}) (Joyal-Street-Verity 96):

the objects of Int(π’ž)Int(\mathcal{C}) are pairs (A +,A βˆ’)(A^+, A^-) of objects of π’ž\mathcal{C}, a morphism (A +,A βˆ’)β†’(B +,B βˆ’)(A^+ , A^-) \to (B^+ , B^-) in Int(π’ž)Int(\mathcal{C}) is given by a morphism of the form A +βŠ—B βˆ’βŸΆA βˆ’βŠ—B +A^+\otimes B^- \longrightarrow A^- \otimes B^+ in π’ž\mathcal{C}, and composition of two such morphisms (A +,A βˆ’)β†’(B +,B βˆ’)(A^+ , A^-) \to (B^+ , B^-) and (B +,B βˆ’)β†’(C +,C βˆ’)(B^+ , B^-) \to (C^+ , C^-) is given by tracing out B βˆ’B^- from the composite

A +βŠ—B βˆ’βŠ—C βˆ’β†’fβŠ—1A βˆ’βŠ—B +βŠ—C βˆ’β†’1βŠ—gA βˆ’βŠ—B βˆ’βŠ—C +. A^+ \otimes B^- \otimes C^- \xrightarrow{f\otimes 1} A^- \otimes B^+ \otimes C^- \xrightarrow{1\otimes g} A^- \otimes B^- \otimes C^+.

Note that π’ž\mathcal{C} embeds fully-faithfully in Int(π’ž)Int(\mathcal{C}) by sending AA to (A,I)(A,I), where II is the unit object of the monoidal structure.

Furthermore, a traced monoidal category that is *\ast-autonomous must already be compact closed; see HH13.

In cartesian monoidal categories

For a cartesian monoidal category, the existence of a trace operator is equivalent to the existence of a β€œparameterized” fixed point operator satisfying certain properties (Hasegawa 1997). When the category is a Lawvere theory, this is related to the notion of iteration theory.

Adding traces

Since any full monoidal subcategory of a traced monoidal category inherits a trace, not every monoidal category can be fully embedded into a traced monoidal category, and hence also not into a compact closed category. In fact, Plotkin observed that there are monoidal categories that cannot even be faithfully mapped into a traced monoidal category. This can be seen from the fact that a traced monoidal category has the β€œcancellation property” that if fβŠ—id XβŠ—X=gβŠ—id XβŠ—Xf\otimes id_{X\otimes X} = g \otimes id_{X\otimes X} then fβŠ—id X=gβŠ—id Xf\otimes id_X = g\otimes \id_X (since the latter is a trace of the former with one of the copies of XβŠ—XX\otimes X transposed), but not all monoidal categories have this property.

Relation to feedback categories

Feedback categories?KSW02 are a weakening of the axioms of traced monoidal categories. Feedback categories do not satisfy the yanking axiom and they only satisfy a weaker form of naturality on the object to be traced. Examples include some categories of automata.

Categorical semantics

Traced monoidal categories serve as an β€œoperational” categorical semantics for linear logic, known as Geometry of Interactions. See there for more.

In this context the free compact closure Int(π’ž)Int(\mathcal{C}) from above is sometimes called the Geometry of Interaction construction and denoted 𝒒(π’ž)\mathcal{G}(\mathcal{C}) (Abramsky-Haghverdi-Scott 02, def. 2.6).

References

The concept was introduced in

A good exposition is found in

  • Peter Selinger, A survey of graphical languages for monoidal categories, New structures for physics (pdf)

A characterization of trace structures on cartesian monoidal categories is given in

  • Masahito Hasegawa, Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi, Proc. 3rd International Conference on Typed Lambda Calculi and Applications (TLCA 1997). Springer LNCS1210, 1997 (citeseer)

The equivalence between traces and parameterized fixed point operators appears as Theorem 3.1 (the author notes that this theorem was also proved independently by Martin Hyland).

Comprehensive discussion as a source for categorical semantics of the Geometry of Interactions is in

The combination with star-autonomous structure was discussed in

  • TamΓ‘s HajgatΓ³ and Masahito Hasegawa, Traced *\ast-autonomous categories are compact closed, TAC, 2013

Feedback categories and their connection to traced monoidal categories were discussed in

  • Piergiulio Katis, Nicoletta Sabadini, Bob Walters. Feedback, trace and fixed-point semantics, 2002 (Numdam).

Last revised on September 15, 2023 at 15:49:12. See the history of this page for a list of all contributions to it.