University of Birmingham > Talks@bham > Lab Lunch > String diagrams for stably compact locales

String diagrams for stably compact locales

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dr Steve Vickers.

In my 2004 paper “Entailment systems for stably locally compact locales” I looked at the Kleisli category for the upper powerlocale monad on stably compact locales – it is dual to the category of stably continuous frames and preframe homomorphisms. I showed that if you start with the full subcategory on powersets PX (their Scott topologies are the free frames), then the rest can be got by splitting idempotents (the Karoubi envelope). (That is more general than splitting Scott continuous nuclei, as the idempotents don’t have to be inflationary.)

Following the idea of multilingual sequent calculus (Jung, Kegelmann, Moshier), I showed that the morphisms from PX to PY are in bijection with up-closed (“weakening”) relations between the finite powersets FX and FY, with a complicated “cut composition” that deals with the way that, in sequent calculus, finite sets may be interpreted either as conjunctions or disjunctions, depending on where they appear.

The resulting category Ent gives a very economical way to deal with stably compact locales, with duality appearing in a natural way as relational transpose, but is hard to work with because of the cut composition. Yet there were signs that there might be a powerful calculus of string diagrams.

Drew Moshier proposed that these categories, Ent and its Karoubi envelope, might get a string diagrammatic toolkit from structure as cartesian bicategories (Carboni and Walters – CW). This would provide strong analogies with Rel and its Karoubi envelope, which is equivalent to continuous dcpos and their Kleisli morphisms for the lower powerlocale.

I shall outline how this works for Ent. It is a cartesian bicategory. It is also compact closed, though not quite by the mechanism of “bicategories of relations”, proposed by CW, which applies to Rel.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.