Category theory reduces a large chunk of math to the clever manipulation of arrows. One of the fun things about this is that you can often take a familiar mathematical construction, think of it category-theoretically, and just *turn around all the arrows* to get something new and interesting!

In math we love functions. If we have a function

we can formally turn around the arrow to think of as something going back from back to . But this something is usually not a function: it’s called a ‘cofunction’. A **cofunction** from to is simply a function from to

Cofunctions are somewhat interesting, but they’re really just functions viewed through a looking glass, so they don’t give much new—at least, not by themselves.

The game gets more interesting if we think of functions and cofunctions as special sorts of relations. A **relation** from to is a subset

It’s a **function** when for each there’s a unique with It’s a **cofunction** when for each there’s a unique with

Just as we can compose functions, we can compose relations. Relations have certain advantages over functions: for example, we can ‘turn around’ any relation from to and get a relation from to

If we turn around a function we get a cofunction, and vice versa. But we can also do other fun things: for example, since both functions and cofunctions are relations, we can compose a function and a cofunction and get a relation.

Of course, relations also have certain *disadvantages* compared to functions. But it’s utterly clear by now that the category where the objects are finite sets and the morphisms are relations, is very important.

So far, so good. But what happens if we take the definition of ‘relation’ and turn all the arrows around?

There are actually several things I could mean by this question, some more interesting than others. But one of them gives a very interesting new concept: the concept of ‘corelation’. And two of my students have just written a very nice paper on corelations:

• Brandon Coya and Brendan Fong, Corelations are the prop for extraspecial commutative Frobenius monoids.

Here’s why this paper is important for network theory: corelations between finite sets are exactly what we need to describe electrical circuits made of ideal conductive wires! A corelation from a finite set to a finite set can be drawn this way:

I have drawn more wires than strictly necessary: I’ve drawn a wire between two points whenever I want current to be able to flow between them. But there’s a reason I did this: a corelation from to simply tells us when current can flow from one point in either of these sets to any other point in these sets.

Of course circuits made solely of conductive wires are not very exciting for electrical engineers. But in an earlier paper, Brendan introduced corelations as an important stepping-stone toward more general circuits:

• John Baez and Brendan Fong, A compositional framework for passive linear circuits. (Blog article here.)

The key point is simply that you use conductive wires to connect resistors, inductors, capacitors, batteries and the like and build interesting circuits—so if you don’t fully understand the math of conductive wires, you’re limited in your ability to understand circuits in general!

In their new paper, Brendan teamed up with Brandon Coya, and they figured out all the rules obeyed by the category where the objects are finite sets and the morphisms are corelations. I’ll explain these rules later.

This sort of analysis had previously been done for and it turns out there’s a beautiful analogy between the two cases! Here is a chart displaying the analogy:

Spans |
Cospans |

extra bicommutative bimonoids | special commutative Frobenius monoids |

Relations |
Corelations |

extraspecial bicommutative bimonoids | extraspecial commutative Frobenius monoids |

I’m sure this will be cryptic to the nonmathematicians reading this, and even many mathematicians—but the paper explains what’s going on here.

I’ll actually say what an ‘extraspecial commutative Frobenius monoid’ is later in this post. This is a terse way of listing all the rules obeyed by corelations between finite sets—and thus, all the rules obeyed by conductive wires.

But first, let’s talk about something simpler.

### What is a corelation?

Just as we can define functions as relations of a special sort, we can also define relations in terms of functions. A relation from to is a subset

but we can think of this as an equivalence class of one-to-one functions

Why an equivalence class? The image of is our desired subset of The set here could be replaced by any isomorphic set; its only role is to provide ‘names’ for the elements of that are in the image of

Now we have a relation described as an arrow, or really an equivalence class of arrows. Next, let’s turn the arrow around!

There are different things I might mean by that, but we want to do it cleverly. When we turn arrows around, the concept of product (for example, cartesian product of sets) turns into the concept of sum (for example, disjoint union of sets). Similarly, the concept of monomorphism (such as a one-to-one function) turns into the concept of epimorphism (such as an onto function). If you don’t believe me, click on the links!

So, we should define a **corelation** from a set to a set to be an equivalence class of onto functions

Why an equivalence class? The set here could be replaced by any isomorphic set; its only role is to provide ‘names’ for the sets of elements of that get mapped to the same thing via

In simpler terms, a corelation from to a set is just a partition of the disjoint union So, it looks like this:

If we like, we can then draw a line connecting any two points that lie in the same part of the partition:

These lines determine the corelation, so we can also draw a corelation this way:

This is why corelations describe circuits made solely of wires!

### The rules governing corelations

The main result in Brandon and Brendan’s paper is that is equivalent to the PROP for extraspecial commutative Frobenius monoids. That’s a terse way of the laws governing

Let me just show you the most important laws. In each of these law I’ll draw two circuits made of wires, and write an equals sign asserting that they give the same corelation from a set to a set The inputs of each circuit are on top, and the outputs are at the bottom. I’ll draw 3-way junctions as little triangles, but don’t worry about that. When we compose two corelations we may get a wire left in mid-air, not connected to the inputs or outputs. We draw the end of the wire as a little circle.

There are some laws called the ‘commutative monoid’ laws:

and an upside-down version called the ‘cocommutative comonoid’ laws:

Then we have ‘Frobenius laws’:

and finally we have the ‘special’ and ‘extra’ laws:

All other laws can be derived from these in some systematic ways.

Commutative Frobenius monoids obey the commutative monoid laws, the cocommutative comonoid laws and the Frobenius laws. They play a fundamental role in 2d topological quantum field theory. Special Frobenius monoids are also well-known. But the ‘extra’ law, which says that a little piece of wire not connected to anything can be thrown away with no effect, is less well studied. Jason Erbele and I gave it this name in our work on control theory:

• John Baez and Jason Erbele, Categories in control. (Blog article here.)

### For more

David Ellerman has spent a lot of time studying what would happen to mathematics if we turned around a lot of arrows in a certain systematic way. In particular, just as the concept of relation would be replaced by the concept of corelation, the concept of subset would be replaced by the concept of partition. You can see how it fits together: just as a relation from to is a subset of a corelation from to is a partition of

There’s a lattice of subsets of a set:

In logic these subsets correspond to propositions, and the lattice operations are the logical operations ‘and’ and ‘or’. But there’s also a lattice of partitions of a set:

In Ellerman’s vision, this lattice of partitions gives a new kind of logic. You can read about it here:

• David Ellerman, Introduction to partition logic, *Logic Journal of the Interest Group in Pure and Applied Logic* **22** (2014), 94–125.

As mentioned, the main result in Brandon and Brendan’s paper is that is equivalent to the PROP for extraspecial commutative Frobenius monoids. After they proved this, they noticed that the result has also been stated in other language and proved in other ways by two other authors:

• Fabio Zanasi, *Interacting Hopf Algebras—the Theory of Linear Systems*, PhD thesis, École Normale Supériere de Lyon, 2015.

• K. Dosen and Z. Petrić, Syntax for split preorders, *Annals of Pure and Applied Logic* **164** (2013), 443–481.

Unsurprisingly, I prefer Brendan and Brandon’s approach to deriving the result. But it’s nice to see different perspectives!

Cool. But really not a fan of this term “corelation” because it’s way too easy to read as a misspelling of “correlation.” A new term unrelated to the term “relation” would probably have been fine. (I think mathematicians as a rule overrate the importance of systematic terminology, relative to e.g. physicists; that’s the kind of thinking that would’ve given the world “Lorentzian singularity” or something instead of “black hole.”)

Such problems in English can be resolved with hyphenation (“co-relation”), though some people hate that. This would work better if software wouldn’t put line breaks after hyphens.

Unfortunately the term “corelation” is reasonably well established, and none of the people using it have any desire to stop!

I also support co-relation (with the hyphen).

Hyphen, no-hyphen; mox nix to me

Who thought like me that “corelation” was a typo and then felt a bit stupid…? :D

I became a big fan of the term because it taught me something: 1) read carefully before thinking someone’s wrong and 2) beware of “co”s in category theory!

I enjoyed reading the post. I also appreciate the links to various references. I presume Brendan and you have plans for this technology. Or am I being presumptuous?

You’re not being presumptuous—at least, not incorrectly presumptuous. Brendan and I already needed corelations in our paper on a compositional framework for passive linear networks, but this ‘generators and relations’ description of a PROP equivalent to the symmetric monoidal category of corelations will play a part in a new paper we’re writing with Brandon Coya and Franciscus Rebro. Jason Erbele’s thesis on control theory will also use PROPs. The overall strategy is to describe various kinds of networks showing up in applied mathematics as morphisms in decorated cospan categories, but also give general and relations descriptions of PROPs equivalent to these decorated cospan categories.

This post has the same effect on me as the one on operads and phylogenetic trees. It looks familiar but I don’t understand it because I don’t understand category theory.

The most important partitions that occur in my work are partitions of individual organisms into sets called ‘species’. I often think of these partitions in terms of trees. In the diagram of the lattice of partitions of a set, each path from any node X up to the top represents a binary tree whose tips are the subsets in the partition at X.

Dear John, nice blog entry. You might be interested to the fact that we investigated which algebraic laws hold for spans and cospans with respect to cartesian product and disjoint union, tracing the connection with various kinds of relations, in two old articles, namely

[1] R. Bruni, F. Gadducci: Some algebraic laws for spans. RelMiS 2001, ENTCS 44(3), 175-193

[2] R. Bruni, F. Gadducci, U. Montanari: Normal forms for algebras of connections. TCS 286(2): 247-292 (2002)

[1] discusses the interplay between the two monoidal operators and the span/cospan dichotomy over Set, while [2] basically discusses the same situation, yet wrt. Graph.

More to the point, it seems to me that in [1] we call equivalence relations what you call corelations, and we have the same extra and special laws. Check e.g. Table 1, axioms 1 and 5.

I will try and better understand your results, in order to trace a precise comparison. Best, Fabio

Thanks! I’ll take a look at your papers. Actually Brendan and Brandon’s paper cites the first of the two papers you mentioned here. I talked to Brendan and he said you list all the laws implicit in the phrase ‘extraspecial commutative Frobenius monoid’, and prove that obeys these laws, but don’t prove that all the laws obeyed by can be derived from these. If so, you essentially got a symmetric monoidal functor from the PROP for extraspecial commutative Frobenius monoids to but didn’t prove it’s an equivalence.

Indeed, in [1] we just proved the soudness of those laws, so to say, as part of a taxonomy of span/cospan categories over Set. A more precise correspondence statement is in [2], even if the notation there is admittedly a bit unwieldy: see Propositions 4.8 and 4.9, the latter being the completeness bit, which is actually just exploiting the older paper

[3] V.-E. Cazanescu, Gh. Stefanescu: Classes of finite relations as initial abstract data types I. Discrete Mathematics 90: 233–265 (1991)

I am very excited by the novel applications and connections that you are pushing, and looking forward to more results in the future.

At some point I gave Brendan Fong a project:

describe the category whose morphisms are electrical circuits. He took up the challenge much more ambitiously than I’d ever expected, developing powerful general frameworks to solve not only this problem but also many others. He did this in a number of papers, most of which I’ve already discussed […]