category with duals (list of them)
dualizable object (what they have)
which is the transpose of the evaluation map
Define a functor . The map is natural in , so that there is a natural isomorphism . We also have
The functor , together with these two isomorphisms, can be taken as an alternative definition of a -autonomous category. The dualizing object is then defined as .
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.
A simple example of a -autonomous category is the category of finite-dimensional vector spaces over some field . In this case itself plays the role of the dualizing object, so that for an f.d. vector space , is the usual dual space of linear maps into .
More generally, any compact closed category is -autonomous with the unit 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 is itself a sup-lattice, so this category is closed. The free sup-lattice on a poset is the internal hom of posets ; in particular the poset of truth values is a unit for the closed structure. Define a duality on sup-lattices, where is the opposite poset (inf-lattices are sup-lattices), and where is the left adjoint of . In particular, take as dualizing object . Some simple calculations show that under the tensor product defined by the formula , 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 is a graded algebra , where is a finite-dimensional vector space in degree 1, is the tensor algebra (the free -algebra generated by ), and is a graded ideal generated by a subspace in degree 2; so , and determines the pair . A morphism of quadratic algebras is a morphism of graded algebras; alternatively, a morphism is a linear map such that . Define the dual of a quadratic algebra given by a pair to be that given by where is the kernel of the transpose of the inclusion , i.e., there is an exact sequence
Define a tensor product by the formula
where 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 , and the result is a -autonomous category.
In a similar vein, I am told that there is a -autonomous category of quadratic operad?s.
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.
The notion is originally due to
The relation to linear logic was first described in
and a detailed review (also of a fair bit of plain monoidal category theory) is in