Jason (jcreed) wrote,

Completed some last-minute christmas shopping.

Hung out with bhudson in the afternoon. Saw the science & industry museum, had some dinner, chatted about theory and PL and academia and stuff. Good times.

I had a thought or two about partial equivalence relations in the shower this morning --- they're something I remember Andrej Bauer being very big on when he was back around CMU working with Dana Scott. The definition's really simple: a partial equivalence relation (often shortened to PER) is a relation that's transitive and symmetric. Just like an equivalence relation, but you drop reflexivity.

I seem to recall the setting in which you use them in realizability theory is the underlying set is typically something like the natural numbers thought of as Gödel-numbers of some data structure, and you're allowed to say that some numbers aren't valid codes at all (the partiality of the relation) and some numbers despite being different numbers code up the same data structure (the equivalence aspect of the relation).

So "cutting down a set to leave just the good stuff" and "quotienting by some relation" are two really common themes in mathematics generally, and in category theory we call them "taking equalizers" and "taking coequalizers". I found it interesting that PERs are sort of doing both at once, and not in any particular order: I could think of a PER as beginning life as a set that is first cut down and then quotiented out, or as a set that's first quotiented out and then cut down.

I then found myself meditating on a diagram that can be derived from any PER, namely
A ->> B
v     v
|     |
v     v
N ->> C

Where N is the underlying set of the PER, A is the subset of N for which reflexivity holds, B is the set of equivalence classes in the PER, and C is the union of B together with every point of N for which reflexivity falis.

The funny thing is that this diagram is (I think) both a pushout and a pullback.

Is there anything special about such diagrams in other categories? Do they behave kind of like "PER objects"?
Tags: categories, math, partial equivalence relations, social

  • (no subject)

    K's off at an atypically Saturdayish Type-Thursday event, so I stuck around the apartment hiding from 100-degree heat, and noodled around with…

  • (no subject)

    Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.

  • (no subject)

    https://deadlockempire.github.io is a very cute edutainment game, meant to teach people about deadlocks and race conditions and concurrency…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded