nLab star-autonomous category

Redirected from "*-autonomous category".
Contents

Context

Monoidal categories

monoidal categories

With braiding

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 \;\colon\; A \to (A \multimap \bot) \multimap \bot ,

which is the transpose of the evaluation map

ev A,:(A)A, ev_{A,\bot} \;\colon\; (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^* and the internal hom by ABA *BA \multimap B \coloneqq A^* \parr B (where \parr is defined as below).

(See this discussion on the categories mailing list for alternative definitions and remarks about coherence.)

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. This follows from a stronger result of Dold and Puppe [DP83].

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

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

  • Girard’s coherence spaces, developed as models of linear logic, give an historically important example of a **-autonomous category. These are closely related to a general construction of **-autonomous categories (and related types of categories) called poset-valued sets.

  • The category of finiteness spaces and their relations is **-autonomous. Probably so is any category of arity spaces, which includes coherence spaces and finiteness spaces.

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

  • If VV is a closed monoidal category with finite products, then V×V opV \times V^{op} is **-autonomous (Barr 1996). This is a special case of the Chu construction where the dualizing object is terminal.

  • Various subcategories of Chu constructions are also **-autonomous. For instance, if Vect is the category of vector spaces over a field kk, then Chu(Vect,k)Chu(Vect,k) is the category of vector spaces equipped with a specified “dual” having no further structure than an evaluation map VWkV\otimes W\to k. One often wants to impose nondegeneracy conditions on this “dual”, which in turn can be reflected as topological properties of the original space VV. Write (V,V)(V,V') for an object of Chu(Vect,k)Chu(Vect,k) and v,w\langle v,w \rangle the evaluation of ww on vv. We say that (V,V)(V,V') is separated if for each v0Vv \neq 0 \in V, there exists vVv' \in V' such that v,v0\langle v,v' \rangle \neq 0 and we say that it is extensional if for each v0Vv' \neq 0 \in V', there exists vVv \in V such that v,v0\langle v,v' \rangle \neq 0. Then, the full subcategory chu(Vect,k)chu(Vect,k) of separated, extensional pairs is **-autonomous.

  • A quantale (see there) is a *\ast-autonomous category if it has a dualizing object.

  • Suppose C,,I,\langle C,\otimes, I,\multimap\rangle is a closed symmetric monoidal category equipped with a “pre-dualizing object” \bot, in the sense that the contravariant self-adjunction ()()(-\multimap\bot) \dashv (-\multimap\bot) is idempotent, i.e. the double-dualization map A(A)A \to (A \multimap \bot) \multimap \bot is an isomorphism whenever AA is of the form BB\multimap\bot. (Note that idempotence is automatic if CC is a poset.) Then the category of fixed points of this adjunction, i.e. the full subcategory of objects of the form BB\multimap\bot, is **-autonomous. For it is closed under \multimap, as (A(B))(AB)(A\multimap (B\multimap \bot)) \cong (A\otimes B\multimap \bot), and reflective with reflector ()(-\multimap\bot)\multimap\bot, and it contains \bot since (I)\bot\cong (I\multimap \bot). Hence it is closed symmetric monoidal with tensor product ((AB))((A\otimes B)\multimap\bot)\multimap\bot, and all its double-dualization maps are isomorphisms by assumption. A historically important example is Girard’s phase semantics of linear logic. Note that this category is a full subcategory of Chu(C,)Chu(C,\bot) closed under duality — indeed, it is the intersection of the two embeddings of CC and C opC^{op} therein — but its tensor product is not the restriction of the tensor product of Chu(C,)Chu(C,\bot).

  • Phase semantics is also a special case of a ternary frame, which is the case of the previous example when C,,I,\langle C,\otimes, I,\multimap\rangle has the Day convolution structure induced from a promonoidal poset. There is also another way to obtain negation in a ternary frame involving a “compatibility relation”…

  • The unit interval [0,1][0,1] is a semicartesian *\ast-autonomous poset with the monoidal structure xy=max(x+y1,0)x \otimes y = \max(x+y-1,0) and dualizing object 00. The involution is x *=1xx^\ast = 1-x and the dual multiplicative disjunction is xy=min(x+y,1)x\parr y = \min(x+y,1). This is known as Lukasiewicz logic? and is used in fuzzy logic; it is also a special case of a t-norm.

  • A summary of many different ways to construct examples is in Hyland-Schalk.

Relation to other structures

  • A *\ast-autonomous category is a linearly distributive category with the cotensor product xy=(x *y *) *x\parr y = (x^* \otimes y^*)^*. Conversely, any linearly distributive category with “duals” in the appropriate sense is *\ast-autonomous.

  • Since a linearly distributive category is a representable polycategory, a *\ast-autonomous category is a representable polycategory with duals. If the duals are strictly involutive, then it is a *-polycategory.

  • As noted above, a compact closed category is a degenerate sort of *\ast-autonomous category.

  • It is shown in HH13 that a *\ast-autonomous category that is traced must be compact closed.

  • We can weaken the requirement that the canonical morphism d A:A(A) d_A: A \to (A \multimap \bot) \multimap \bot is an isomorphism to the one that it is a monomorphism: weak (star)-autonomous category.

References

The notion is originally due to:

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)

further discussed in

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]

Examples using toplogical vector spaces are given here:

Relation to linearly distributive categories:

Combination with traces yields compact closure:

  • Tamás Hajgató and Masahito Hasegawa, Traced *\ast-autonomous categories are compact closed, TAC, 2013

A wide-ranging summary of different model constructions:

The fact that a *\ast-autonomous category for which there is a natural isomorphism (AB) *A *B *(A \otimes B)^\ast \simeq A^\ast \otimes B^\ast is a compact closed category has a purely string diagrammatic proof, but it also follows from the implication (a)\implies (b) of Theorem 1.3 in this paper:

According to Tobias Fritz (on the Category Theory Community Server):

They apparently didn’t know about *\ast-autonomous categories (which were introduced a few years prior to that), and their statement has slightly weaker assumptions in that they start with a natural isomorphism 𝒞(AB,I)𝒞(A,B *)\mathscr{C}(A \otimes B, I) \cong \mathscr{C}(A, B^*) only, but they also require the induced morphisms A *B *(AB) *A^* \otimes B^* \to (A \otimes B)^* to be isomorphisms.

See also:

With an eye towards apication in 2d CFT (to representations of vertex operator algebras and their bimodules):

Last revised on April 24, 2024 at 01:49:13. See the history of this page for a list of all contributions to it.