nLab
star-autonomous category

Context

Monoidal categories

Category theory

Contents

Idea

There are many ways to describe a **-autonomous category; here are a few:

In particular, it has two monoidal structures \otimes and \parr, as in a linearly distributive category. However, because of the dualization operation () *(-)^\ast, each of them determines the other by a “multiplicative de Morgan duality”: AB(A *B *) *A\parr B \cong (A^\ast \otimes B^\ast)^\ast. Thus, in the definition we only have to refer to one monoidal structure.

A *\ast-autonomous category is a special case of the notion of star-autonomous pseudomonoid (a.k.a. Frobenius pseudomonoid, since it categorifies a Frobenius algebra) in a monoidal bicategory.

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 global dualizing object: 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^\ast \otimes B^\ast)^\ast \,.

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.

Functors and transformations

It may not be clear from the above definitions what the appropriate notion of “*\ast-autonomous functor” is. In fact, from at least one perspective it suffices to consider ordinary lax monoidal functors, at least in the symmetric case; no interaction with the *\ast-autonomy is required.

Let *Aut\ast Aut denote the full sub-2-category of SymMonCat laxSymMonCat_{lax} on the (symmetric) *\ast-autonomous categories; hence its morphisms and 2-cells are lax symmetric monoidal functors and monoidal natural transformations. Let SymLinDistSymLinDist denote the 2-category of symmetric linearly distributive categories, symmetric linear functors, and linear transformations (defined at linearly distributive category).

Theorem

There is a functor *AutSymLinDist\ast Aut \to SymLinDist that is 2-fully-faithful, i.e. an equivalence on hom-categories, and has both a left and a right 2-adjoint.

Proof

A linearly distributive functor consists of a functor F F_\otimes that is lax monoidal for \otimes and a functor F F_\parr that is lax monoidal for \parr. Recalling that \parr is defined in a *\ast-autonomous category as AB=(A *B *) *A\parr B = (A^* \otimes B^*)^*, if FF is a lax monoidal functor between *\ast-autonomous categories we define F =FF_\otimes = F and F (A)=(F(A *)) *F_\parr(A) = (F(A^*))^*. See Cockett-Seely 1999 for details.

In the non-symmetric case, we need to additionally require of an “*\ast-autonomous functor” that *(F(A *))(F( *A)) *^*(F(A^*)) \cong (F({}^*A))^*, and define F F_\parr to be their common value.

On the other hand, if we consider instead “Frobenius linear functors” between linearly distributive categories, then such functors necessarily preserve duals. Thus, the corresponding notion of *\ast-autonomous functor would need to preserve the dualization functors as well, F(A *)(F(A)) *F(A^*) \cong (F(A))^*.

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.

See also

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)

Relation to linearly distributive categories:

Revised on October 31, 2017 00:31:32 by Mike Shulman (76.167.222.204)