nLab star-autonomous category

Context

Monoidal categories

monoidal categories

With traces

• trace

• traced monoidal category?

category theory

Contents

Definition

A $*$-autonomous category is a symmetric closed monoidal category $\langle C,\otimes, I\rangle$ with a dualizing object: an object $\bot$ such that the canonical morphism

$d_A: A \to (A \multimap \bot) \multimap \bot ,$

which is the transpose of the evaluation map

$ev_{A,\bot}: (A \multimap \bot) \otimes A \to \bot ,$

is an isomorphism for all $A$. (Here, $\multimap$ denotes the internal hom.)

Define a functor $(-)^*=(-)\multimap\bot$. The map $d_A$ is natural in $A$, so that there is a natural isomorphism $d:1\Rightarrow(-)^{**}$. We also have

\begin{aligned} \hom(A\otimes B,C^*)& = \hom(A\otimes B, C\multimap\bot) \\ & \cong \hom((A\otimes B)\otimes C,\bot) \\ & \cong \hom(A\otimes(B\otimes C), \bot) \\ & \cong \hom(A,(B\otimes C)\multimap\bot) \\ & = \hom(A,(B\otimes C)^*) \end{aligned}

The functor $(-)^*$, together with these two isomorphisms, can be taken as an alternative definition of a $*$-autonomous category. The dualizing object $\bot$ is then defined as $I^*$.

Properties

Internal logic

The internal logic of star-autonomous categories is classical linear logic, conversely star-autonomous categories are the categorical semantics of classical linear logic (Seely 89, prop. 1.5). See also at relation between type theory and category theory.

Examples

• A simple example of a $*$-autonomous category is the category of finite-dimensional vector spaces over some field $k$. In this case $k$ itself plays the role of the dualizing object, so that for an f.d. vector space $V$, $V^*$ is the usual dual space of linear maps into $k$.

• More generally, any compact closed category is $*$-autonomous with the unit $I$ as the dualizing object.

• A more interesting example of a $*$-autonomous category is the category of sup-lattices and sup-preserving maps (= left adjoints). Clearly the poset of sup-preserving maps $hom(A, B)$ is itself a sup-lattice, so this category is closed. The free sup-lattice on a poset $X$ is the internal hom of posets $[X^{op}, \Omega]$; in particular the poset of truth values $\Omega$ is a unit for the closed structure. Define a duality $(-)^*$ on sup-lattices, where $X^* = X^{op}$ is the opposite poset (inf-lattices are sup-lattices), and where $f^*: Y^* \to X^*$ is the left adjoint of $f^{op}: X^{op} \to Y^{op}$. In particular, take as dualizing object $D = \Omega^{op}$. Some simple calculations show that under the tensor product defined by the formula $(X \multimap Y^*)^*$, the category of sup-lattices becomes a $*$-autonomous category.

• Another interesting example is due to Yuri Manin: the category of quadratic algebras. A quadratic algebra over a field $k$ is a graded algebra $A = T(V)/I$, where $V$ is a finite-dimensional vector space in degree 1, $T(V)$ is the tensor algebra (the free $k$-algebra generated by $V$), and $I$ is a graded ideal generated by a subspace $R \subseteq V \otimes V$ in degree 2; so $R = I_2$, and $A$ determines the pair $(V, R)$. A morphism of quadratic algebras is a morphism of graded algebras; alternatively, a morphism $(V, R) \to (W, S)$ is a linear map $f: V \to W$ such that $(f \otimes f)(R) \subseteq S$. Define the dual $A^*$ of a quadratic algebra given by a pair $(V, R)$ to be that given by $(V^*, R^\perp)$ where $R^\perp \subseteq V^* \otimes V^*$ is the kernel of the transpose of the inclusion $i: R \subseteq V \otimes V$, i.e., there is an exact sequence

$0 \to R^\perp \to V^* \otimes V^* \overset{i^*}{\to} R^* \to 0$

Define a tensor product by the formula

$(V, R) \otimes (W, S) = (V \otimes W, (1_V \otimes \sigma \otimes 1_W)(R \otimes S))$

where $\sigma: V \otimes W \to W \otimes V$ is the symmetry. The unit is the tensor algebra on a 1-dimensional space. The hom that is adjoint to the tensor product is given by the formula $A \multimap B = (A \otimes B^*)^*$, and the result is a $*$-autonomous category.

• In a similar vein, I am told that there is a $*$-autonomous category of quadratic operad?s.

• Girard’s coherence spaces?, developed as models of linear logic, give an historically important example of a $*$-autonomous category.

• Hyland and Ong have given a completeness theorem for multiplicative linear logic in terms of a $*$-autonomous category of fair games, part of a series of work on game semantics for closed category theory (compare Joyal’s interpretation of Conway games as forming a compact closed category).

• The Chu construction can be used to form many more examples of $*$-autonomous categories.

References

The notion is originally due to

• Michael Barr, $*$-Autonomous Categories. LNM 752, Springer-Verlag 1979.

The relation to linear logic was first described in

• R. A. G. Seely, Linear logic, $\ast$-autonomous categories and cofree coalgebras, Contemporary Mathematics 92, 1989. (pdf, ps.gz)

and a detailed review (also of a fair bit of plain monoidal category theory) is in

• Paul-André Melliès , Categorial Semantics of Linear Logic, in Interactive models of computation and program behaviour, Panoramas et synthèses 27, 2009 (pdf)

Revised on December 9, 2013 07:20:34 by Urs Schreiber (89.204.139.250)