On the category of virtual species

Question

In Foncteurs analytiques et espèces de structures, Joyal defines virtual species, as a (quotient) of formal differences of functors $F,G:\mathbb{B}\rightarrow \mathsf{Set}$, and then proceeds to show that these form a (commutative) ring. The quotienting operation is that of equivalence of species.

Has anyone instead studied what might be best termed the category of virtual species, where the quotient is not carried out? The objects would be formal differences of species, and the arrows would be equivalences, basically "unpacking" the quotient groupoid.

As this seems relatively straightforward, I would expect that it has been carried out before. The point here is that various isomorphisms (like $A+B \simeq B+A$) have computational content, and thus it is useful to work in a setting where these are representable. When studying the computational content of $A+M=B+M$, one is quite naturally led to looking at virtual species as the right place to ask that question -- if only it were done categorically rather than algebraically!

Answer 1

I had tried to do something like this around 1994, and then again a little later as I will explain in a moment. The first time around, I had tried formalizing this in the context of species valued in a category of "virtual sets" (finite sets, to avoid an Eilenberg swindle), guided by Joyal's pretty observation that the implication "$A + C \cong B + C$ implies $A \cong B$" definitely has computational meaning as you say: starting with a given bijection $f: A + C \to B + C$, feed back the outputs of $f$ that land in $C$ as inputs, and iterate to obtain a bijection $g: A \to B$. This operation is natural in the sense fully explained in Joyal-Street-Verity's paper, Traced Monoidal Categories. (Essentially the same observation appears in Conway and Doyle's paper, Division by Three, if I remember correctly.)

One can categorify the taking of formal differences, starting with the category of finite sets and bijections and applying the tortile category construction in Traced Monoidal Categories. It's pretty simple in this case and one winds up with the compact closed category of oriented 1-cobordisms (so objects are oriented compact 0-manifolds, i.e., multisets of +'s and -'s, and morphisms are diffeomorphisms of oriented compact 1-manifolds with boundary). I tried developing a calculus of virtual species as functors from $\mathbb{B}$ to this category, but at some point the project petered out. Unfortunately I cannot recall exactly where it petered out at this remove in time, but I suspect it had to do with the fact that to get the full richness of the usual theory of species uses good properties of $\mathrm{Set}$ such as cartesian closure, and that some of these properties don't translate well to the category of virtual sets (the category of oriented 1-cobordisms). For example, taking the negative of a set should be a duality functor (a contravariant equivalence), but cartesian closed categories that are self-dual collapse to posets.

A few years later I had another crack at it (while I was hanging out as a visitor at U. Chicago, around 1996), but this time I was more interested in formalizing virtual linear species (i.e., differences of $\mathrm{Vect}$-valued species), since the primary application in the Joyal paper centered on linear species and particularly the structure of the Lie species. The basic idea was to use differential $\mathbb{Z}_2$-graded spaces modulo quasi-isomorphism as the receiving category, thinking of $(V_0, V_1, d)$ as representing a formal difference $V_0 - V_1$. This approach seemed much more promising, and is implicit in my Notes on the Lie Operad, which you can find here if you are interested. However, I was never satisfied with those notes and never tried to publish them -- I should return to this, and particularly the model category of $\mathbb{Z}_2$-graded chain complexes as an environment for virtual linear species. (Perhaps someone else has fleshed it all out in the meantime?)