You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
I want to draw attention and start a discussion thread on @David Spivak's new preprint https://arxiv.org/abs/2005.01894 on the category of polynomial functors
I suspect this category might be very folkloric, I wonder if anyone's seen it in anything old? (There's a cluster of literature beginning with https://www.cs.nott.ac.uk/~psztxa/publ/fossacs03.pdf and Michael Abbott's thesis, which I already told David about, which studies this category)
Bob Atkey also wrote me this: "There's even more structure in Poly! Tamara von Glehn's thesis shows that it is a model of dependent types with an equality type that refutes functional extensionality. Also, there's an interesting skew-monoidal product related to selective functors."
David told me about this category over a year ago, and explained it as "it's like locally ringed spaces, except you replace local rings with sets and also replace topological spaces with sets". So for a while we called it "setted sets". So I wonder if it already appears in Grothendieck or something equally old and in French?
(Since it looks like I'm just bashing it, I should add that I'm extremely excited about this paper)
@Joachim Kock 's notes on polynomial functors has a section of historical remarks, and probably knows much more about the history of this category.
http://mat.uab.es/~kock/cat/polynomial.pdf (long pdf!)
Part of the difficulty with finding references to properties of polynomial functors is that they're spread across both category theory (as "polynomial functors") and computer science (as "indexed containers").
Another thing to be aware of is that sometimes results are stated just for polynomials in , like in @David Spivak's new preprint, and some for arbitrary categories with pullbacks. Some of the properties stated in the preprint are not true for the category of polynomials in an arbitrary category.
This is the same one in 2.5 of Kock's notes, I take it?
Nathanael Arkor said:
Part of the difficulty with finding references to properties of polynomial functors is that they're spread across both category theory (as "polynomial functors") and computer science (as "indexed containers").
Over on the category-theoretic side, there are some interesting applications of polynomial functors (and monads) to topology. It'd be interesting to see how they can be interpreted through this lens (pun somewhat intended).
Rongmin Lu said:
This is the same one in 2.5 of Kock's notes, I take it?
I believe it's the category defined in §2.1 of the notes. of Kock's notes restricts to cartesian natural transformations.
Nathanael Arkor said:
Rongmin Lu said:
This is the same one in 2.5 of Kock's notes, I take it?
I believe it's the category defined in §2.1 of the notes. of Kock's notes restricts to cartesian natural transformations.
Thank you. I think restricting to Cartesian natural transformations can be useful. In the case of lenses, which can be viewed as an optic associated to a special case of polynomial functors, I think this gives you lawful lenses. (I haven't verified this, this is something I've heard in a seminar somewhere.)
Woah, that would be really amazing if that's true
I'm not sure the claim typechecks though, it doesn't make sense to talk about lawful lenses between arbitrary objects of the category
This was from a seminar at Macquarie by Mike Johnson pre-Covid. I have notes somewhere that I need to dig up.
In the context of data manipulation, lawfulness is desirable for safety purposes. Even there, however, there are also instances where you want lenses to be less lawful.
Anyway, all I'm trying to say is that Cartesian natural transformations came up in the discussion of lawfulness during Mike's seminar. It's 3 in the morning here and I'll look at this in more detail later.
Rongmin Lu said:
It's definitely more restrictive, but I'm not sure what you mean by "arbitrary objects of the category" and why it doesn't "typecheck".
Not totally sure, I was kinda thinking out loud, but in the case of the category I call "bimorphic lenses" (which is apparently equivalent to the full subcategory of monomials) has objects of the form (corresponding to the monomial ), but you can only write the definition of lawful lenses for lenses of the form
Right. And since I can't sleep without correcting my mistake...
I think in Kock's notes, it's stated in 2.1 that "every natural transformation between polynomial functors factors as a representable one followed by a cartesian." In the case of lenses, the Cartesian thing is the put. Often, though, you want to relax the Cartesian assumption. That got garbled into the "amazing" thing that's surely not true.
Still very much shooting from the hip here, but it sounds like how every lens factors in the form which comes from the fact that lenses are fibred over sets, so that's a vertical and a cartesian morphism. I'm not sure it's the same sense of "cartesian" or not!
The sense in which Kock means "Cartesian morphisms" (actually, "Cartesian natural transformations") is defined in between Lemma 2.1.5 and Remark 2.1.6. It looks like the same definition as the one in the nLab.
Somewhat off-topic, but re. your musings on quantum machine learning, this is actually an emerging research area.
It is indeed not so easy to trace the origin of the theory of polynomial functors. Joyal had them in the 1980s in connection with his discovery of combinatorial species and analytic functors, but did not really develop the theory because it is not rich enough to cover species and operads. Joyal himself claims that the notion should be attributed to Grothendieck :-) (I don't know exactly what this means...)
At the CT2010 in Genova, Peter Johnstone helped me draw a very interesting map of precursors to the notion of polynomial functors. I remember there were dozens of them, but unfortunately I don't have the map anymore :-( There are polynomial functors already in Arbib and Manes, but they did not see the pleasant representation of them in terms of maps E -> B.
For me the really cool feature of polynomial functors is their representability feature --- how they can be manipulated in terms of E -> B. The first printed evidence of this viewpoint that I am aware of is [Bisson-Joyal (1995): The Dyer-Lashof algebra in bordism (extended abstract), 1995]. That's some very grown-up algebraic topology they are up to, and their E -> B is really a covering space! They don't have time to talk much about polynomial functors, though. In logic, I believe the first explicit appearance is [Moerdijk-Palmgren (2000): Wellfounded trees in categories], where they show that Martin-Löf's W-types are initial algebras for polynomial endofunctors. The really nice many-variable formalism I believe was introduced by [Gambino-Hyland (2003): Wellfounded Trees and Dependent Polynomial Functors]. It is very curious though, that this shape of diagram,
I <- E -> B -> J was studied by Tambara already in 1993 --- yes! it is the same Tambara as in Tambara modules! Tambara essentially proved (without noticing it) that finite polynomial functors are the Lawvere theory theory for commutative semirings. See [Gambino-Kock (2013): Polynomial functors and polynomial monads] for this result.
Generally in [GK] we made a big effort to collect history and to unify the various developments, and in particular to bring all the container stuff into more mathematical language. I recommend that paper as a basic reference :-)
Joachim wrote:
The first printed evidence of this viewpoint that I am aware of is [Bisson-Joyal (1995): The Dyer-Lashof algebra in bordism (extended abstract), 1995]. That's some very grown-up algebraic topology they are up to [...]
Yeah, sounds like it! I hope I understand that stuff when I grow up!
Another big source of confusion is that there is something else which is also called polynomial functor: they are endofunctors F: Vect -> Vect such that for every pair of vector spaces the the map on hom spaces is given by polynomials. Such functors come up in representation theory, for example in connection with Schur functors. The appeared in Macdonalds book Symmetric Functions and Hall Polynomials, but in fact they were first studied in the 1950s (or even 1940s?) by Eilenberg and Mac Lane in connection with group cohomology. It's a very active area of research in representation theory and algebraic topology, for example in connection with functor cohomology.
The two theories of polynomial functors --- the one in cartesian contexts (such as logic and geometry), and the one in linear contexts -- do not seem to have so much in common at this point. For example, there are no representability features in the linear case. Adamek and Velebil show that the only pullback-preserving endofunctors of Vect are 'tensoring with a fixed vector space'.
Regarding my Notes on polynomial functors I should apologise for them being so messy and unprocessed.
I learned about polynomial functors when I was a postdoc with André Joyal in 2003-2004. We used polynomial functors to give a combinatorial version of the Baez-Dolan construction, and they have been a central topic in my research ever since.
Since there was not much literature available, I started to write notes at that time. By 2009, when the manuscript had over 400 pages, a huge mess (and containing mistakes), I put it on hold (that's its present state), because I realised I needed to upgrade everything from sets to groupoids, in order to cover the applications I had in mind in combinatorics and operad theory. Since then I have been learning about groupoids (and infinity-groupoids).
Groupoids really make a huge difference. With David Gepner and Rune Haugseng we showed that polynomial functors over groupoids are expressive enough to cover species, analytic functors, and operads. In fact with polynomial monads over infinity-groupoids we give a neat model for infinity-operads.
I think I am now in a position where I could go back to the manuscript and finish it -- with groupoids. But meanwhile, as you all know: each research project creates a number of new research projects, so it is not clear when I will actually come around to this.
However, the remarkable recent work of David Spivak and his collaborators is very motivating, and it is enjoyable to see how powerful the polynomial-functor toolbox is even in the case of one-variable polynomial functors over Set! Congratulations, David!
(Sorry for telling about myself. Maybe I should move this post to the present-yourself section.)
@Joachim Kock: one thing I was always curious about was how generalised species had an entire chapter dedicated to them in the table of contents for the notes (though sadly the chapter appears unwritten). Is this still a topic you would reserve a chapter for in the eventual updated book?
Jules Hedges said:
Still very much shooting from the hip here, but it sounds like how every lens factors in the form which comes from the fact that lenses are fibred over sets, so that's a vertical and a cartesian morphism. I'm not sure it's the same sense of "cartesian" or not!
Yes, that's right, it's the same.
Joachim Kock said:
The two theories of polynomial functors --- the one in cartesian contexts (such as logic and geometry), and the one in linear contexts -- do not seem to have so much in common at this point.
I'm probably asking for too much, but I've always wondered how Goodwillie calculus can be related to these.
Nathanael Arkor said:
Joachim Kock: one thing I was always curious about was how generalised species had an entire chapter dedicated to them in the table of contents for the notes (though sadly the chapter appears unwritten). Is this still a topic you would reserve a chapter for in the eventual updated book?
I don't know if I would get around to this. The generalised species stuff (Fiore-Gambino-Hyland-Winskel) is really a different brand of polynomial functors (as you surely know) than the slice-category brand I mostly work with. The generalised-species stuff is about categories instead of groupoids -- very scary! It is closely related (is equal to?) the familial functors that Todd talked about in another thread, studied deeply by Mark Weber. And which Spivak uses for data migration. I would love to know more about that, but maybe it is not my highest priority right now -- and in any case my priorities tend to get overridden...
Rongmin Lu said:
I'm probably asking for too much, but I've always wondered how Goodwillie calculus can be related to these.
I think the Goodwillie calculus is more closely related to the Vect-based notion of polynomial functor that I mentioned a few posts back.
not sure if i should necropost this here or start a new thread but i have been trying to think about polynomial functors of this kind and i am a bit stuck
in particular: if is some polynomial functor, i understand that i can recover the set of "positions" of by just evaluating or equivalently by taking , but given a position , how do i get the set of directions ?
the paper linked at the beginning of the thread seems to just take for granted that you can do so, in a way that only makes sense to me if either a) a polynomial functor is defined as a kind of "presentation" rather than a functor with a given property, or b) we use choice to fix once and for all a pseudoinverse to the functor from such presentations to polynomial functors
or to turn it around: my question essentially is: is there a nice, choiceless construction for defining such a pseudoinverse?
uh, maybe "pseudoinverse" is a term i invented in my head, sorry—i just meant the other direction of the equivalence. "homotopy inverse"?
@Todd Trimble has written "pseudo-inverse" in a paper of ours, expecting me to understand it, and I did. So I think it's fine. Personally I'd tend to say "weak inverse", or "homotopy inverse" if I were trying to evoke sensations of homotopy theory.
I think I've seen other people use the term "quasi-inverse", but I used pseudo-inverse because of the use of the word "pseudo" elsewhere to suggest "up to isomorphism", as opposed to "strict" or on-the-nose.
Indeed I like "pseudo-" here better than "quasi-", for exactly that reason: we also have pseudofunctors, pseudonatural transformations, pseudomonads, etc., so you can stick "pseudo" in front of almost anything and I'll get it.
This is a very good question. First, how do you recover the set of directions of a monomial ? Well, the monomials are the image of under Yoneda, which is fully faithful, so in a non-constructive sense we know that non-isomorphic sets give non-isomorphic monomials. Can't we just evaluate on some nice set to actually get out? Well...no, not really. The smallest set that would make sense is and in fact it's consistent with ZFC that could be isomorphic to without being isomorphic to (this doesn't quite contradict Cantor's theorem, though they sound similar.) Of course this is an infinities problem, and if you're only looking at finitary polynomials, you can readily recover as
For general polynomials, you can somewhat analogously prove that the only way they could be isomorphic is if there's a bijection between the positions inducing bijections at all the corresponding directions. This is an example of the behavior of free coproduct completions, in general: in free coproduct completions, the "presentation" you ask about is unique up to permutation of the coproduct indices. But all the moreso, there's no simple way to compute the directions just by plugging in, if you're handed a polynomial you only know how to evaluate.
right, i figured this much out and wondered if i was missing something clever, like if evaluating some sort of limit or colimit can recover the directions
actually, i would note that even for the finitary case we still have a problem—your is a decategorification of what i actually want, and by performing that decategorification you lose information
like, if you take the subcategory of of functors that can be written as coproducts of representables, i don't think the construction actually defines the pseudo-inverse i was talking about
Let's be a bit more precise: Say is defined to be the subcategory of on those functors for which there merely exists some way to write them as a coproduct of representables, is defined to be the category whose objects are maps of sets understood as bundles and whose morphisms are pairs.
define also to be the subcategory of on coproducts of reps and to be the subcategory of on finite-fibered bundles
then there are evident functors and that are easy to write down explicit formulae for
we can show that these functors are ff and eso so choice says we have pseudo-inverses, but i want explicit formulae for those pseudo-inverses
the construction defines an object mapping but since you decategorify in the process i'm super skeptical that you can easily make it an actual functor
if there were a way to recover the order structure on the subsets then it would be easy, but I don't see any clear way of doing that
um. hm. actually i think in a HoTT setting these categories are all univalent so the HoTT proof that constructs a pseudoinverse from ff+eso w/o using choice might apply here...
i don't know how that proof goes though :sweat_smile: i'm looking at the hott book rn to see if i can parse anything out
oh right this doesn't give you a formula the way i want it just tells you that it's licit to talk about the stuff hidden inside the "merely exists". that's sort of unsatisfying though... i guess in my gut i want a construction that only uses the interface of "a functor " and which happens to give the right result in the case that the input is actually polynomial
Well, once you have the object mapping of the pseudo-inverse of a functor, the functoriality is uniquely defined since the hom mappings are bijections.
hmmmmm
i think you actually also need one of the natural isomorphisms witnessing the fact that it's a pseudoinverse unless your object mapping is an inverse on the nose?
say we have ff and eso and we define an object mapping . say ; then you're saying to invert some map . but to get my hands on such an invertible map, i either need to
This does rephrase the problem to "show a natural isomorphism of with "
Another possibility is to use the derivative. I believe is the set of all directions.
i'm not sure what kind of derivative you mean
that said, i want to get the set of directions at a given position, not just the set of all directions
sarahzrf said:
This does rephrase the problem to "show a natural isomorphism of with "
I'm having trouble seeing how your question doesn't reduce to "show a natural isomorphism of to when are sets of the same cardinality."
Just the ordinary derivative of a polynomial. There is a canonical map from the base of into the base of that will allow you to recover the fibers.
Kevin Carlson said:
sarahzrf said:
This does rephrase the problem to "show a natural isomorphism of with "
I'm having trouble seeing how your question doesn't reduce to "show a natural isomorphism of to when are sets of the same cardinality."
sorry, clarification: i mean an isomorphism natural in actually, wait, the rhs isn't a functor in so now I'm not sure what I'm asking for—I guess I mean "an explicit, general formula that gives an isomorphism for each without invoking choice". so in that sense, it is essentially similar to what you wrote indeed—there is no nice general formula giving an isomorphism as a function of finite sets of the same cardinality! you have to invoke some kind of choice
Spencer Breiner said:
Just the ordinary derivative of a polynomial. There is a canonical map from the base of into the base of that will allow you to recover the fibers.
okay, but if I have the data of a functor and not a polynomial, how do I do this?
To narrow in on a claim that's at least quite clear although it may be off target of your exact question, I do not agree that you need any kind of choice to get from an isomorphism an isomorphism . For one thing, the Yoneda embedding is fully faithful, so the choice is unique. For another, you have an explicit formula for it given by evaluating at the identity map of
you certainly don't need choice to pass between isomorphisms and , but the knowledge that is not the data of an isomorphism , it's the propositional truncation thereof
that's what i meant about decategorification
in general, if i know that for example, that furnishes me with no choice of a bijection , it only tells me that one exists. There will in fact be six possible bijections, none of which are preferred without further structure on or
Sorry I'm late to the party, but I was really delighted to find @Joachim Kock 's lecture, "Polynomial functors — from elementary arithmetic to infinity-operads" where he explains the link between the Poly he works on and @David Spivak and all's at about 32:00 minutes.
There seems to be also another category Poly, which is a left-additive one that I first met in @Bruno Gavranović 's dissertation, which is also different. So if I understand it well, there are 4 different "kinds" of Poly, is that right? (These 3, of which I think one is a "sub-concept" of another but I'm not sure which way it goes, and the Vect-related Poly that Joachim mentioned above.)
I've been trying to do a "descent" on each of these Polys and have been getting pretty confused on the "gluing". (Sorry for all of the ""'s, it's hard to talk in normal language now that I've discovered that there are precise and agreed-upon definitions of particular things). To help keep the different Polys separate in my mind, I'm using the following names:
(I thought to post these questions here to keep it close to Joachim's and other's references, and to maybe clarify future discussion on it, but now I'm wondering whether I should have put it on learning channel -- please let me know whether these questions should have gone there, thank you)
If someone from ACT/Topos-sphere mentions Poly I usually assume they mean polynomial functors over Set of one variables, but otherwise most category theorist mean polynomials à là Gambino-Kock, which are defined on any LCCC category and strictly related to the first for . There are also Ghani-Abbott containers, and Spivak dependent lenses, which are again equivalent presentation of polynomial functors Set of one variables.
Like Bob Dylan going electric, are there signs people like @David Spivak are going homotopic?
It's... ineluctable
There is, needless to say, also a theory of -polynomials, as worked out e.g. here