nLab
star-autonomous category

Context

Monoidal categories

Category theory

Contents

Definition

There are two useful equivalent formulation of the definition

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.)

Definition

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 isomorphism

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

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

Proof

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^*.

Remark

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 \parr B \coloneqq (A^\perp \otimes B^\perp)^\perp \,.

making it into a linearly distributive category. Here the notation on the left is that used in linear logic, see below at Properties – Internal logic.

A general *\ast-autonomous category can be thought of as like a compact closed category in which the unit and counit of the dual objects refer to two different tensor products: we have AA *\top \to A \parr A^* but A *AA^* \otimes A \to \bot, where (,)(\otimes,\top) and (,)(\parr,\bot) are two different monoidal structures. The necessary relationship between two such monoidal structures such that this makes sense, i.e. such that the triangle identities can be stated, is encoded by a linearly distributive category; then an *\ast-autonomous category is precisely a linearly distributive category in which all such “mixed duals” (or “negations”) exist.

Properties

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.

Examples

  • 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.

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)

Examples from algebraic geometry are given here:

  • Mitya Boyarchenko and Vladimir Drinfeld, A duality formalism in the spirit of Grothendieck and Verdier, arXiv:1108.6020 (pdf)

These authors call any closed monoidal category with a dualizing object a Grothendieck-Verdier category, thanks to the examples coming from Verdier duality.

Here it is explained how **-autonomous categories give Frobenius pseudomonads in the 2-category where morphisms are profunctors:

  • Ross Street, Frobenius monads and pseudomonoids, J. Math. Physics 45 (2004) 3930-3948. (pdf)

Revised on May 15, 2016 00:20:48 by Mike Shulman (76.167.222.204)