Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
at species it says that this is a presheaf of sets on . At structure type this then makes me expect the words “is a presheaf of groupoids” on . Is there a deeper reason why it does not say that?
It seems clear that the Gepner-Kock homotopical species are precisely the -presheaves on , i.e. the -groupoid valued ones.
I’d think it would be good to emphasize this presheaf-point of view in our entries.
Hold on. ’Species’ is synonymous with ’stucture type’ (Joyal vs Baez-Dolan). So there shouldn’t be separate pages. Wouldn’t it be stuff types that are presheaves of groupoids?
David wrote:
’Species’ is synonymous with ’stucture type’ (Joyal vs Baez-Dolan). So there shouldn’t be separate pages.
Well, maybe there shouldn’t be and maybe there should…. but you’re right that in their narrowest sense, both species and structure types are the same thing: presheaves of sets on the groupoid of finite sets and bijections.
Wouldn’t it be stuff types that are presheaves of groupoids?
Yes, with ’presheaf’ taken in a suitably weakened sense: they are pseudofunctors, or weak 2-functors, from the groupoid of finite sets and bijections (or its opposite!) to Gpd.
And in our vocabulary we can go on to talk about -stuff types or -stuff types. I’m guessing that -stuff types are the same as ’homotopical species’.
I’ve done a little work trying to fix up structure type, and I added entries on stuff type and stuff. These would have to be expanded to be really comprehensible.
So i edited species:
inluded the defintion of 2-species (aka stuff types )
included the definition of -species
included a paragraph on cardinality of tame -species
I edited species a tiny bit more.
added to species some comments on addition and multiplication operations after it occurred to me while glancing over the Wikipedia-entry that the product of species is nothing but Day convolution.
Then I added to the discussion on cardinality a remark on how this Day convolution does decategorify to the product of power series.
I also added some references to the entry … but didn’t look at any of them yet. Unless I got my combinatorics mixed up (please check) the relation to Day convolution is probably in there somewhere. If somebody knows reference and page, please add a remark on that.
Ah, Google luckily remembers that Todd said this before! :-)
I don’t know who first discovered that multiplication of species is an example of Day convolution, but it’s true (in case you were wondering), and we have a fair amount of information about this at Schur functor in the special case of “linear” species, i.e. -valued presheaves on .
In my dream world, there would be a huge article on ordinary “set-theoretic” species and then a parallel huge article on linear species, and something that explained properties of the map from the former to the latter. But this may happen only if and when I use the Lab to write my dreamt-of book Categorified Arithmetic.
Anyone who wants to really get into linear species has got to look at this. While categorically sophisticated, it alas does not mention Day convolution.
I see, thanks, John.
Hopefully you plug these remarks also into the relevant nLab entries.
I spent my Christmas break getting acquainted with species and playing around with them in HoTT. I updated the page with a some comments, and in the references I linked longer notes along with a github repo containing the code I wrote while learning. I hope this is okay; neither the notes nor the code is at all polished, but with my academic term restarting tomorrow I don’t know whether I’ll have much time to improve on them soon.
I have added in the first line a few hyperlinks for the sake of readers coming across this who may not already know what “homotopy type theory” and the “type of finite sets” is.
Has the excitement surrounding species died down in recent years? Gian-Carlo Rota portrayed them as providing a revolutionary framework for combinatorics:
Joyal’s definition of “labeled object” as a species discloses a vast horizon of new combinatorial constructions, which cannot be seen if one holds on to the reactionary view that “labeled objects” need no definition. The simplest, and the most remarkable application of the definition of species is the rigorous combinatorial rendering of functional composition, which was formerly dealt with by handwaving – always a bad sign. But it is just the beginning.
Then Joyal endorsed Monoidal Functors, Species and Hopf Algebras
The book of Aguiar and Mahajan is a quantum leap toward the mathematics of the future. I strongly recommend it to all researchers in algebra, topology and combinatorics.
What of the link to physics? There was all that work by Baez, Dolan and Morton. Then there was linear logic meets generalized species meets Fock space as here
The present axiomatisation of creation maps has been directly influenced by and developed through a thorough analysis of the differential structure of generalised species of structures [10, 11], which is a bicategorical generalisation of that of the relational model of linear logic.
Is there still reason to be excited?
Not an answer to your question, but a related comment: the Cauchy product of species is equivalently their phased tensor product when regarded as objects in the slice over the symmetric monoidal internal category object (which here happens to be a groupoid object).
Hence to the extent that one cares about species equipped with the Cauchy product, one is looking at a special case of an FQFT-type formalization of local prequantum field theory. And of a substantial formalization, in that it connects to genuine QFT.
(I suggest that this is interesting, but would caution about excitement. Excitement is a bit like steam: it produces work when contained but just heat when released. ;-)
I have edited the section Species – In homotopy type theory a bit more. Just tried to beautify a bit more, adding formatting, hyperlinks, and more pointers to references (in the section on the Cauchy product).
John Dougherty, please have a look when you find a minute, to check if you are happy with what I did.
I added the variant ’generalised species’ to Species – variants.
I have added a link to the thesis of Yorgey. He treats species in HoTT, I’ve read parts of it and it looks very natural.
I see he has a whole chapter on ’Species variants’.
Nice! The definition of the coproduct of species in HoTT doesn’t look right to me; should it instead be the copairing of and ?
please have a look when you find a minute, to check if you are happy with what I did.
Yes, thank you, it is much more readable now.
The definition of the coproduct of species in HoTT doesn’t look right to me; should it instead be the copairing of and ?
It should be, and I corrected it. I’m not sure what happened; I had it right in the original version of the notes, and it’s right in the Coq code. Odd.
Coming back to the discussion starting at #1, in the meantime Kock et al. have brought out an article Homotopic linear algebra. Here the role of the category of (finite) vector spaces is played by various -categories of slices of finite -groupoids and spans.
Wouldn’t this kind of thing make for a more interesting codomain than plain -groupoids for homotopical species?
(This is in the context of the recent paper on as the free 2-rig on one generator by John, Joe and Todd. There is shown to be equivalent to , the category of polynomial species from to .)
But then homotopical species are defined in ∞-Operads as Analytic Monads as we have it already (Definition 3.2.9). I’ll add that in.
1 to 22 of 22