nLab
star-autonomous category

Context

Monoidal categories

monoidal categories

With symmetry

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products

Semisimplicity

Morphisms

Internal monoids

Examples

Theorems

In higher category theory

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.

(Regarding the use of “autonomous”, this was once used as a bare adjective to describe a closed monoidal category, or sometimes a compact closed monoidal category, but is rarely used in this way today. It has been suggested that in these cases with internal-hom objects the category is autonomous or “sufficient unto itself” without needing hom-sets, or suchlike.)

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,\multimap\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. and def. , are indeed equivalent.

Proof

Given def. , 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. .

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.

More generally, even 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

Relation to other structures

References

The notion is originally due to

See also

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

Examples from algebraic geometry are given here:

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:

Relation to linearly distributive categories:

Combination with traces yields compact closure:

A wide-ranging summary of different model constructions: