Over six years ago, I wrote a post explaining how virtual species are defined. Ever since then (time flies!) I’ve been meaning to write a follow-up post explaining a bit more about virtual species and how they actually suffice to give us not just additive inverses, but also (somewhat surprisingly) multiplicative inverses.
Recall that the intuitive idea of a combinatorial species is a family of labelled structures which are invariant under relabelling. If you’ve never seen the formal definition before, don’t worry: just think “data structures” or “algebraic data types” for now.
The basic idea of virtual species is to work with pairs of species where is considered “positive” and “negative”. Formally, we consider equivalence classes of such pairs under the equivalence relation defined by iff .1 This parallels the way one typically gives a formal definition of the integers starting from the natural numbers (the “Grothendieck construction”); see my previous post for more details.
How can we build intuition for virtual species, and for additive inverses of species in particular? To be honest I have been struggling with this question for many years.
Multiplicative inverses are much simpler to think about: they are like matter and antimatter. Having both an -structure and an structure is the same as having nothing; they annihilate each other. By “having nothing” we mean “having no information”, that is, having a unit value: .
What about additive inverses? Note first that the species does not correspond to having nothing; the word “nothing” corresponds to the (i.e. unit) species. Instead the (i.e. uninhabited) species corresponds to (logical) impossibility. So to interpret we have to imagine something where having either or is impossible.
…yeah, me neither. This seems deeply strange. If someone says, “I either have an or a ”, you can confidently call them a liar, because it is impossible to have either an or a ; that is, . But surely if you actually have an -structure, it should also be true to say “I have either an or a ”? Well, that works for normal, positive species—in which case we can define a canonical injection . But once we introduce negative species this completely breaks down. As another example, if someone truthfully says, “I have either a tree or a negative non-empty tree”, you should be able to say, “Aha! I know what you have—it must be an empty tree.” In general, it’s strange that expressing a disjunction can cause some possibilities to be ruled out. Normally, we are used to disjunctions only increasing the number of possibilities.
Inspired by James and Sabry’s really cool paper The Two Dualities of Computation: Negative and Fractional Types, I have thought a bit about whether there is some plausible interpretation involving travelling backwards in time, but I haven’t been able to come up with one. I can’t quite seem to make the formalism of the paper match up with my intuition about species (though this may just be a failure of my imagination or intuition).
In any case, let’s see why the ring of virtual species actually has multiplicative inverses—at least, all the ones we could possibly hope for. This is somewhat surprising, since when we build integers from natural numbers by considering equivalence classes of pairs, we certainly don’t get any multiplicative inverses, only additive ones. To get multiplicative inverses we have to do the same process a second time, building the rational numbers as equivalence classes of pairs of integers. But species already have enough extra structure that throwing in additive inverses is all it takes.
First, a caveat: we don’t get multiplicative inverses for all species, but only those species such that : that is, species with only a single structure of size zero, which are of the form . With any constant term other than , we clearly have no hope of finding another species such that , since the constant term of will be a multiple of ’s constant term.
So given such a , write , where denotes “non-empty -structures”. Then we can define the multiplicative inverse of as follows:
That is, a -structure consists of a list of nonempty -structures, except that even-length lists are considered “positive” and odd-length lists considered “negative”.
We can easily check that this indeed defines a multiplicative inverse for :
The infinite sums telescope down to leave only . Notice this really isn’t about species in particular, but really about infinite power series (of which species are the categorification): any infinite power series with integer coefficients and a constant term of has a multiplicative inverse which is also such a power series.
As an example, consider . We know this is “supposed” to be the species of lists (since it results from solving for ), but let’s see what happens. In this case and . So the inverse ought to be
And hey, look at that! Lists!
A field of species?
So what would we need to get a true field, i.e. a multiplicative inverse for every nonzero species? Well, for that we would need to throw in rational coefficients. I forget exactly where I read this—some paper by Baez and Dolan, most likely—but I believe the proper way to interpret this would be as groupoid-valued species, since there is a sense in which the “cardinality” of groupoids can be interpreted as rational numbers. But to be honest I have no idea where this leads.
Note that species sum is cancellative—that is, if then —so this is a coherent definition. This cancellative property is probably worth another post of its own since the reason for it is not entirely trivial.↩