category with duals (list of them)
dualizable object (what they have)
There are two useful equivalent formulation of the definition
which is the transpose of the evaluation map
such that there is a natural equivalence
Then the morphism is natural in , so that there is a natural isomorphism . We also have
This yields the structure of def. 2.
is a compact closed category.
Conversely, if the -autonomous category is not compact closed, then by this linear ” de Morgan duality” the tensor product induces a second binary operation
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 . 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