On poset-valued sets

On Monday afternoon I had a look at Andrea Schalk and Valeria de Paiva’s paper on Poset-valued sets, which I was reminded of recently by Greg Restall’s survey of relevant and substructural logics.

It gives a recipe for constructing models of linear logic that have specified properties, by starting from a poset that has the required properties and constructing a category based on that. There is something rather mystifying about the construction as it stands, so I wondered whether there’s some way of thinking about it that sheds more light on it. I think there is, and I may as well record it here in case anyone is interested. The ingredients of the construction are: a poset P that has some additional (monoidal, monoidal closed, star-autonomous) structure, and a lax monoidal functor F: RelRel. These ingredients are used to construct a (monoidal, etc.) category PFSet.

Now, there is a standard construction that builds from any category C a category Rel(C) that can be described concretely as follows: an object of Rel(C) is a set S together with a function fS: S → |C|, and a morphism r: S → T consists of a relation S → T together with, for every (x,y) ∈ r, a set of C-morphisms from fS(x) to fT(y). Abstractly, Rel(C) is the free sup-lattice-enriched category with small biproducts generated by C, which can be constructed by freely changing the base of enrichment and then freely adding the biproducts.

For any C there is an obvious forgetful functor U: Rel(C) → Rel. My basic observation is that the category PFSet is precisely the pullback of F: RelRel and U: Rel(P) → Rel. (The assumption that P is a poset rather than an arbitrary category does not seem to have any effect beyond simplifying the concrete description of the result.)

The interesting part is the monoidal structure. For the sake of simplicity, just suppose that C is monoidal; we want to see how a monoidal structure is induced on PFSet. It’s easy to see that Rel(C) inherits, and U strictly preserves, any monoidal structure possessed by C. On the other hand, F is only lax monoidal (or equivalently oplax monoidal, since Rel is self-dual), so that doesn’t immediately help. At this point, perhaps it makes things easier to abstract away from the details for a moment. We have a pullback like this:

PVS pullback

where the three categories we started with (C, D and E) are all monoidal, U is strict monoidal, and F is oplax monoidal. It turns out that if U is a fibration then there is a natural way to define a monoidal structure on B. (I’m not sure whether this has been observed before [update: it has – see Richard’s comment below], but it’s quite easy.) Furthermore, U doesn’t actually need to be a fibration: the only maps that need to have cartesian liftings are the structural maps F(A⊗B) → FA⊗FB and FI → I that give the oplax monoidal structure on F.

Coming back to our concrete U: Rel(C) → Rel, there are two simple extreme cases: on the one hand, a relation that is the graph of a function always has a cartesian lifting; on the other, if C has (set-indexed) products then every relation has one (so in this case U really is a fibration). The former case is the one that’s addressed in the paper – it’s assumed that the structural maps are always graphs of functions – but it’s clear from what I’ve just said that this can be generalised. In the former case our general construction does seem to give the same result as the concrete description in the paper.

The same idea can certainly be extended to monoidal closed structure: in this case we need F to be lax monoidal as well as oplax monoidal, which is a triviality in the concrete case in question. I haven’t thought about star-autonomous structure, but I would be surprised if that didn’t work too.

This entry was posted in category theory, chatter. Bookmark the permalink.

5 Responses to On poset-valued sets

  1. urs says:

    […] models of linear logic […]

    The ingredients of the construction are: a poset P that has some additional (monoidal, monoidal closed, star-autonomous) structure, and a lax monoidal functor

    This reminds me of the paper

    F. W. Lawvere,
    Metric Spaces, Generalized Logic, and Closed Categories
    (discussed here).

  2. bosker says:

    And what a wonderful paper to be reminded of! I can’t see a precise connection, but it would be very nice if one could be made. The most obvious difference is that Lawvere is enriching in a monoidal poset (so associating a poset element with every pair of objects) whereas de Paiva and Schalk are associating a poset element with every member of some set. Is there a way to bridge that gap?

  3. Hi Robin,

    Your observation about monoidal structures appears in this paper of M. Hasegawa’s


    He uses it as a jumping off point to explain glueings, double glueings, etc, in a manner similar to yours.

  4. bosker says:

    So it does! Marvellous, thanks.

  5. Valeria says:

    hi Robin,
    I only saw these messages now more than a year after they were originally posted,sorry. I wanted to say that the similarity to Lawvere’s metric spaces is totally what we were after. One of the versions of dialectica categories that I had already worked on before, in a technical report called “Categorical Multirelations” was exactly a version of metric spaces. Now when we started talking about models of linear logic I said I wanted to separate chu-like models where every object has two-sides, one almost fighting the other, and models, more like coherence spaces where you map into an algebraic structure a bit like the one you want in the whole category, the case of the poset-valued sets. in the case of dialectica you kind of need both, but it seemed clear that either of these strategies was enough for an interesting model.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s