star-autonomous category


Monoidal categories

Category theory



There are two useful equivalent formulation of the definition


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

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

which is the transpose of the evaluation map

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

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


A **-autonomous category is a symmetric monoidal category 𝒞\mathcal{C} equipped with a full and faithful functor

() *:𝒞 op𝒞 (-)^\ast \colon \mathcal{C}^{op} \longrightarrow \mathcal{C}

such that there is a natural equivalence

𝒞(AB,C *)𝒞(A,(BC) *). \mathcal{C}(A \otimes B, C^\ast) \simeq \mathcal{C}(A, (B\otimes C)^\ast) \,.

These two definitions, def. 1 and def. 2, are indeed equivalent.


Given def. 1, define the dualization functor as the internal hom into the dualizing object

() *(). (-)^ \ast \coloneqq (-)\multimap\bot \,.

Then the morphism d Ad_A is natural in AA, so that there is a natural isomorphism d:1() **d:1\Rightarrow(-)^{**}. We also have

hom(AB,C *) =hom(AB,C) hom((AB)C,) hom(A(BC),) hom(A,(BC)) =hom(A,(BC) *)\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}

This yields the structure of def. 2.

Conversely, given the latter then the dualizing object \bot is defined as the dual of the tensor unit I *\bot \coloneqq I^*.


A *\ast-autonomous category in which the tensor product is compatible with duality in that there is a natural isomorphism

(AB) *A *B * (A \otimes B)^\ast \simeq A^\ast \otimes B^\ast

is a compact closed category.

Conversely, if the *\ast-autonomous category is not compact closed, then by this linear ” de Morgan duality” the tensor product induces a second binary operation

(AB) A B . (A \otimes B)^\perp \equiv A^\perp \parr B^\perp \,.

Here the notatioon on the right is that used in linear logic, see below at Properties – Internal logic.


Internal logic

The internal logic of star-autonomous categories is the multiplicative fragment of 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.


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

  • More generally, any compact closed category is **-autonomous with the unit II 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)hom(A, B) is itself a sup-lattice, so this category is closed. The free sup-lattice on a poset XX is the internal hom of posets [X op,Ω][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 X^* = X^{op} is the opposite poset (inf-lattices are sup-lattices), and where f *:Y *X * f^*: Y^* \to X^* is the left adjoint of f op:X opY opf^{op}: X^{op} \to Y^{op}. In particular, take as dualizing object D=Ω opD = \Omega^{op}. Some simple calculations show that under the tensor product defined by the formula (XY *) * (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 kk is a graded algebra A=T(V)/IA = T(V)/I, where VV is a finite-dimensional vector space in degree 1, T(V)T(V) is the tensor algebra (the free kk-algebra generated by VV), and II is a graded ideal generated by a subspace RVVR \subseteq V \otimes V in degree 2; so R=I 2R = I_2, and AA determines the pair (V,R)(V, R). A morphism of quadratic algebras is a morphism of graded algebras; alternatively, a morphism (V,R)(W,S)(V, R) \to (W, S) is a linear map f:VWf: V \to W such that (ff)(R)S(f \otimes f)(R) \subseteq S. Define the dual A *A^* of a quadratic algebra given by a pair (V,R)(V, R) to be that given by (V *,R )(V^*, R^\perp) where R V *V *R^\perp \subseteq V^* \otimes V^* is the kernel of the transpose of the inclusion i:RVVi: R \subseteq V \otimes V, i.e., there is an exact sequence

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

    Define a tensor product by the formula

    (V,R)(W,S)=(VW,(1 Vσ1 W)(RS))(V, R) \otimes (W, S) = (V \otimes W, (1_V \otimes \sigma \otimes 1_W)(R \otimes S))

    where σ:VWWV\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 AB=(AB *) *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.

  • A quantale (see there) is a *\ast-autonomous category if it has a dualizing object.


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 March 4, 2014 21:33:47 by Urs Schreiber (