Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

November 17, 2017

Star-autonomous Categories are Pseudo Frobenius Algebras

Posted by Mike Shulman

A little while ago I talked about how multivariable adjunctions naturally form a polycategory: a structure like a multicategory, but in which codomains as well as domains can involve multiple objects. Now I want to talk about some structures we can define inside this polycategory MVarMVar.

What can you define inside a polycategory? Well, to start with, a polycategory has an underlying multicategory, consisting of the arrows with unary target; so anything we can define in a multicategory we can define in a polycategory. And the most basic thing we can define in a multicategory is a monoid object — in fact, there are some senses in which this is the canonical thing we can define in a multicategory.

So what is a monoid object in MVarMVar?

Well, actually it’s more interesting to ask about pseudomonoid objects, using the 2-categorical structure of MVarMVar. In this case what we have is an object AA, a (0,1)-variable adjunction i:()Ai:()\to A (which, recall, is just an object iAi\in A), and a (2,1)-variable adjunction m:(A,A)Am:(A,A)\to A, together with coherent associativity and unit isomorphisms. The left adjoint part of mm is a functor A×AAA\times A\to A, and the associativity and unit isomorphisms then make AA into a monoidal category. And to say that this functor extends to a multivariable adjunction is precisely to say that AA is a closed monoidal category, i.e. that its tensor product has a right adjoint in each variable:

A(xy,z)A(y,xz)A(x,zy) A(x\otimes y,z) \cong A(y, x\multimap z) \cong A(x, z \;⟜\; y)

Similarly, we can define braided pseudomonoids and symmetric pseudomonoids in any 2-multicategory, and in MVarMVar these specialize to braided and symmetric closed monoidal categories.

Now, what can we define in a polycategory that we can’t define in a multicategory? The most obvious monoid-like thing that involves multiple objects in a codomain is a comonoid. So what is a pseudo-comonoid in MVarMVar?

I think this question is easiest to answer if we use the duality of MVarMVar to turn everything around. So a pseudo-comonoid structure on a category AA is the same as a pseudo-monoid structure on A opA^{op}. In terms of AA, that means it’s a monoidal structure that’s co-closed, i.e. the tensor product functor has a left adjoint in each variable:

A(x,yz)A(yx,z)A(xz,y). A(x, y \odot z) \cong A(y \rhd x, z) \cong A(x \lhd z , y).

The obvious next thing to do is to mix a monoid structure with a comonoid structure. In general, there’s more than one way to do that: we could think about bimonoids, Hopf monoids, or Frobenius monoids. However, while all of these can be defined in any symmetric monoidal category (or PROP), in a polycategory, bimonoids and Hopf monoids don’t make sense, because their axioms involve composing along multiple objects at once, whereas in a polycategory we are only allowed to compose along one object at a time.

Frobenius algebras, however, make perfect sense in a polycategory. If you look at the usual definition in a monoidal category, you can see that the axioms only involve composing along one object at once; when they’re written topologically that corresponds to the “absence of holes”.

So what is a pseudo Frobenius algebra in MVarMVar? Actually, let’s ask a more general question first: what is a lax Frobenius algebra in MVarMVar? By a lax Frobenius algebra I mean an object with a pseudo-monoid structure and a pseudo-comonoid structure, together with not-necessarily invertible “Frobenius-ator” 2-cells

satisfying some coherence axioms, which can be found for instance in this paper (pages 52-55). This isn’t quite as scary as it looks; there are 20 coherence diagrams listed there, but the first 2 are the associativity pentagons for the pseudomonoid and pseudo-comonoid, while the last 8 are the unit axioms for the pseudomonoid and pseudo-comonoid (of which the 17 th17^{\mathrm{th}} and 18 th18^{\mathrm{th}} imply the other 6, by an old observation of Kelly). Of the remaining 10 axioms, 6 assert compatibility of the Frobenius-ators with the associativities, while 4 assert their compatibility with the units.

Now, to work out what a lax Frobenius algebra in MVarMVar is, we need to figure out what (2,2)-variable adjunctions (A,A)(A,A)(A,A)\to (A,A) those pictures represent. To work out what these functors are, I find it helpful to draw the monoid and comonoid structures with all the possible choices for input/output:

By the mates correspondence, to characterize a 2-cell in MVarMVar it suffices to consider one of the functors involved in the multivariable adjunctions, which means we should pick one of the copies of AA to be the “output” and consider all the others as the “input”. I find it easier to pick different copies of AA for the two Frobenius-ators. For the first one, let’s pick the second copy of AA in the codomain; this gives

In the domain of the 2-cell, on the right, xx and yy come in and get combined into xyx\otimes y, and then that gets treated as ww and gets combined with uu coming in from the lower-left to give u(xy)u\rhd (x\otimes y). In the codomain of the 2-cell, on the left, first xx gets combined with uu to give uxu\rhd x, then that gets multiplied with yy to give (ux)y(u\rhd x) \otimes y. Thus, the first Frobenius-ator is

u(xy)(ux)y. u\rhd (x\otimes y)\to (u\rhd x) \otimes y.

For the second Frobenius-ator, let’s dually pick the first copy of AA in the codomain to be the output:

Thus the second Frobenius-ator is

(xy)vx(yv). (x\otimes y)\lhd v \to x\otimes (y\lhd v).

What is this? Well, let’s take mates once with respect to the co-closed monoidal structure to reexpress both Frobenius-ators in terms of \otimes and \odot. The first gives

(ux)yu(u((ux)y))u((u(xx))y)u(xy). (u \odot x) \otimes y \to u \odot (u\rhd ((u \odot x) \otimes y)) \to u\odot ((u\rhd (x\odot x)) \otimes y) \to u \odot (x\otimes y).

and the second dually gives

x(yv)((x(yv))v)v(x((yv)v))v(xy)v. x \otimes (y\odot v) \to ((x \otimes (y\odot v)) \lhd v) \odot v \to (x \otimes ((y\odot v) \lhd v)) \odot v \to (x\otimes y)\odot v.

These two transformations (ux)yu(xy)(u \odot x) \otimes y \to u \odot (x\otimes y) and x(yv)(xy)vx \otimes (y\odot v) \to (x\otimes y)\odot v have exactly the shape of the “linear distributivity” transformations in a linearly distributive category! (Remember from last time that linearly distributive categories are the “representable” version of polycategories.) The latter are supposed to satisfy their own coherence axioms, which aren’t listed on the nLab, but if you look up the original Cockett-Seely paper and count them there are… 10 axioms… 6 asserting compatibility with associativity of \otimes and \odot, and 4 asserting compatibility with the unit. In other words,

A lax Frobenius algebra in MVarMVar is precisely a linearly distributive category! (In which \otimes is closed and \odot is co-closed.)

Note that this is at least an approximate instance of the microcosm principle. (I have to admit that I have not actually checked that the two groups of coherence axioms coincide under the mates correspondence, but I find it inconceivable that they don’t.)

The next thing to ask is what a pseudo Frobenius algebra is, i.e. what it means for the Frobenius-ators to be invertible. If you’ve come this far (or if you read the title of the post) you can probably guess the answer: a *\ast-autonomous category, i.e. a linearly distributive category in which all objects have duals (in the polycategorical sense I defined in the first post).

First note that in a *\ast-autonomous category, \otimes is always closed and \odot is co-closed, with (xz)=(x *z)(x\multimap z) = (x^\ast \odot z) and (uw)=(u *w)(u\rhd w) = (u^\ast \otimes w) and so on. With these definitions, the Frobenius-ators become just associativity isomorphisms:

u(xy)=u *(xy)(u *x)y=(ux)y. u\rhd (x\otimes y) = u^\ast \otimes (x\otimes y) \cong (u^\ast \otimes x) \otimes y = (u\rhd x) \otimes y.

(xy)v=(xy)v *x(yv *)=x(yv). (x\otimes y)\lhd v = (x\otimes y)\otimes v^\ast \cong x\otimes (y\otimes v^\ast) = x\otimes (y\lhd v).

Thus, an *\ast-autonomous category is a pseudo Frobenius algebra in MVarMVar. Conversely, if AA is a pseudo Frobenius algebra in MVarMVar, then letting x=ix=i be the unit object of \otimes, we have

uyu(iy)(ui)y u\rhd y \cong u\rhd (i\otimes y) \cong (u\rhd i) \otimes y

giving an isomorphism

A(y,uv)A(uy,v)A((ui)y,v).A(y, u\odot v) \cong A(u\rhd y, v) \cong A((u\rhd i) \otimes y, v).

Thus uiu\rhd i behaves like a dual of uu, and with a little more work we can show that it actually is. (I’m totally glossing over the symmetric/non-symmetric distinction here; in the non-symmetric case one has to distinguish between left and right duals, blah blah blah, but it all works.) So

A pseudo Frobenius algebra in MVarMVar is precisely a *\ast-autonomous category!

The fact that there’s a relationship between Frobenius algebras and *\ast-autonomous categories is not new. In this paper, Brian Day and Ross Street showed that pseudo Frobenius algebras in ProfProf can be identified with “pro-*\ast-autonomous categories”, i.e. promonoidal categories that are *\ast-autonomous in a suitable sense. In this paper Jeff Egger showed that Frobenius algebras in the *\ast-autonomous category Sup of suplattices can be identified with *\ast-autonomous cocomplete posets. And Jeff has told me personally that he also noticed that lax Frobenius algebras correspond to mere linear distributivity. (By the way, the above characterization of *\ast-autonomous categories as closed and co-closed linearly distributive ones such that certain transformations are invertible is due to Cockett and Seely.)

What’s new here is that the pseudo Frobenius algebras in MVarMVar are exactly *\ast-autonomous categories — not pro, not posets, not cocomplete.

There’s more that could be said. For instance, it’s known that Frobenius algebras can be defined in many different ways. One example is that instead of giving an algebra and coalgebra structure related by a Frobenius axiom, we could give just the algebra structure along with a compatible nondegenerate pairing AAIA\otimes A \to I. This is also true for pseudo Frobenius algebras in a polycategory, and in MVarMVar such a pairing (A,A)()(A,A) \to () corresponds to a contravariant self-equivalence () *:AA op(-)^\ast : A\simeq A^{op}, leading to the perhaps-more-common definition of star-autonomous category involving such a self-duality. And so on; but maybe I’ll stop here.

Posted at November 17, 2017 7:28 PM UTC

TrackBack URL for this Entry:

4 Comments & 0 Trackbacks

Re: Star-autonomous categories are pseudo Frobenius algebras

What I find fascinating about this is that, to the logician, polycategories are very appealing as they behave very much like sequents. But that’s not what is happening here: the polyarrows represent inference rules (several rules per polyarrow).

I can’t say I have quite wrapped my head around it yet. But it’s certainly appealing.

Posted by: Arnaud Spiwack on November 18, 2017 11:09 AM | Permalink | Reply to this

Re: Star-autonomous categories are pseudo Frobenius algebras

That’s the magic of the microcosm principle! The operations on a structure (e.g. the multiplication in a monoid AA) become the morphisms in a categorified version of the structure (e.g. a morphism AAAA\otimes A\to A in a monoidal category). Here, the operations on a *\ast-autonomous category (inference rules) become morphisms in a 2-polycategory.

From a syntactic point of view, it’s like a logical framework: the judgments of the object-language become types of the logical framework, and the inference rules of the object-language become terms of the logical framework.

Posted by: Mike Shulman on November 18, 2017 11:08 PM | Permalink | Reply to this

Re: Star-autonomous categories are pseudo Frobenius algebras

It makes sense, but I can’t quite convince myself that this is what is happening here. I think it boils down to: is this the “right” category to speak about categorical logic, or did we get to star-autonomous categories by coincidence? (the fact that *-autonomous categories are so expressive is a very good sign though) How can I, for instance, define a cartesian-closed category as a structure in the 2-polycategory of multivariate adjunctions (we’ve seen symmetric monoidal closed categories, so far, and my intuition fails me for cartesian-closed ones, surely we have to use something related to the cartesian product of categories, as with ordinary adjunctions, but is there a natural way to do it in this framework?)

More directly on the microcosm principle: can we define a polycategory as a structure in the 2-polycategory of multivariate adjunctions?

Posted by: Arnaud Spiwack on November 19, 2017 8:29 AM | Permalink | Reply to this

Re: Star-autonomous categories are pseudo Frobenius algebras

I’ve never claimed that any category is the right one to speak about categorical logic! The microcosm principle generally matches up one microcosm with one macrocosm; there’s no reason to expect a single macrocosm to suffice for all possible microcosms. In particular, I wouldn’t expect there to be any way to define a cartesian closed category in MVarMVar; the cartesian product of categories isn’t really visible in MVarMVar.

It is, I admit, a little unsatisfying that *\ast-autonomous categories are “representable” but the structure that we define them in is not. True, there are some *\ast-autonomous 2-categories closely related to MVarMVar, such as SupSup (which it contains) and Chu(Cat,Set)Chu(Cat,Set) (which contains it), and Frobenius pseudomonoids in these are either specializations or generalizations of *\ast-autonomous categories.

However, I would also argue it’s actually in line with other instances of the microcosm principle that the microcosm object is “strong” (*\ast-autonomous category, i.e. representable polycategory with duals) but the macrocosm is “weak” (2-polycategory, not *\ast-autonomous 2-category). Usually this “weakness” manifests itself as an up to isomorphism version of the microcosm, but there are also other instances where it manifests as an (even weaker) lax or multicategorical version, such as duoidal categories and intercategories.

Posted by: Mike Shulman on November 19, 2017 10:55 AM | Permalink | Reply to this

Post a New Comment