The n-Category Café

Time for a Polymath project?

Urs wrote:

One mystery, therefore, that remains is why these four are enjoying such a productive collaboration on this subject, while so many contributors on this blog keep each fiddling around with this with their local crowd without getting an organized blog-based attack going.

As for me, the reason is that I have a lot more fun talking to Jim Dolan than working collaboratively on a blog.

You may consider this ‘fiddling around’ — and indeed it’s probably not the most efficient method of developing a large theory. But I find that as soon as I start thinking of math as a business where teams of researchers try to efficiently maximize production, I also start thinking it’s… not fun anymore.

Jim and I started thinking about groupoidification around 1998 when I realized that an $n$-element set mod the action of a $m$-element group should give a groupoid with $n/m$ elements, and he realized this gave a new outlook on how Joyal’s species form a categorified version of the Hilbert space for a harmonic oscillator. That was a lot of fun, because these ideas seemed almost crazy, and nobody was talking about them.

Now groupoidification is becoming a small part of a much vaster program, and lots of very good people are working on this program. For example: you, Ben-Zvi, Freed, Hopkins, Lurie, and Teleman. So now I don’t feel that same sense of freedom, of exploring an unknown and unoccupied wilderness. Instead, it feels like a race where I’d need to keep up with what other people are doing. I get tired just thinking about it! So, I prefer to think about other subjects now… even though it will take a year or two to finish off HDA7, HDA8 and HDA9.

But as for you, Urs: why don’t you try to collaborate with Ben-Zvi, Freed, Hopkins, Lurie, or Teleman? I’m sure the results would be amazing!

I should add that while I personally am not interested in joining any ‘massive blog collaborations’, I think it would be great if such a collaboration developed on the $n$-Café.

From what I’ve seen, it seems that a big project like this require a charismatic leader who works tirelessly keep it on track, but lets other people take a lot of initiative and get a lot of credit for their work.

When you think of the Polymath projects you think of Tim Gowers and Terry Tao. When you think of Wikipedia you think of Jimmy Wales, and when you think of Linux you think of Linus Torvalds.

Torvalds seems to have put forth the most thoughtful comments about running such large projects. For example:

Nobody should start to undertake a large project. You start with a small trivial project, and you should never expect it to get large. If you do, you’ll just overdesign and generally think it is more important than it likely is at that stage. Or worse, you might be scared away by the sheer size of the work you envision.

So start small, and think about the details. Don’t think about some big picture and fancy design. If it doesn’t solve some fairly immediate need, it’s almost certainly over-designed. And don’t expect people to jump in and help you. That’s not how these things work. You need to get something half-way useful first, and then others will say “hey, that almost works for me”, and they’ll get involved in the project.

And if there is anything I’ve learnt from Linux, it’s that projects have a life of their own, and you should not try to enforce your “vision” too strongly on them. Most often you’re wrong anyway, and if you’re not flexible and willing to take input from others (and willing to change direction when it turned out your vision was flawed), you’ll never get anything good done.

In other words, be willing to admit your mistakes, and don’t expect to get anywhere big in any kind of short timeframe. I’ve been doing Linux for thirteen years, and I expect to do it for quite some time still. If I had expected to do something that big, I’d never have started. It started out small and insignificant, and that’s how I thought about it.

Also:

While it turns out that most people are idiots, the corollary to that is sadly that you are one too, and that while we can all bask in the secure knowledge that we’re better than the average person (let’s face it, nobody ever believes that they’re average or below-average), we should also admit that we’re not the sharpest knife around, and there will be other people that are less of an idiot that you are.

Some people react badly to smart people. Others take advantage of them. Make sure that you, as a [manager], are in the second group. Suck up to them, because they are the people who will make your job easier. In particular, they’ll be able to make your decisions for you, which is what the game is all about.

So when you find somebody smarter than you are, just coast along. Your management responsibilities largely become ones of saying “Sounds like a good idea - go wild”, or “That sounds good, but what about xxx?”. The second version in particular is a great way to either learn something new about “xxx” or seem extra managerial by pointing out something the smarter person hadn’t thought about. In either case, you win.

One thing to look out for is to realize that greatness in one area does not necessarily translate to other areas. So you might prod people in specific directions, but let’s face it, they might be good at what they do, and suck at everything else. The good news is that people tend to naturally gravitate back to what they are good at, so it’s not like you are doing something irreversible when you do prod them in some direction, just don’t push too hard.

Why not turn the journal club into the beginnings of this blog-based attack?

I think following Torvalds’ advice and starting very small is a good idea.

I don’t think the initial goal has to be to compete with anyone. A better initial goal might be to see if we can successfully produce a piece of work.

Alex wrote:

Why not turn the journal club into the beginnings of this blog-based attack?

I think that’s a great idea. If you ‘journal club’ folks tried to prove a theorem or two, it might boost your energy level a notch or two. I get the feeling you were just trying to understand David Ben–Zvi’s work. That’s great, but mathematicians always seem to get more excited when they’re trying to prove stuff. Maybe there’s an easy extension of David’s work that you guys could try, just for starters. I’m sure Urs and David are brimming with ideas; the trick will be to find a bite-sized one.

Why not turn the journal club into the beginnings of this blog-based attack?

I think that’s a great idea. If you ‘journal club’ folks tried to prove a theorem or two, it might boost your energy level a notch or two. I get the feeling you were just trying to understand David Ben–Zvi’s work. That’s great, but mathematicians always seem to get more excited when they’re trying to prove stuff. Maybe there’s an easy extension of David’s work that you guys could try, just for starters. I’m sure Urs and David are brimming with ideas; the trick will be to find a bite-sized one.

I tried to initiate this investigation here recently as an outgrowth of the Journal Club activity.

This contains some bite-sized qustions, as indicated.

In the bigger picture, this is to be merged with the other thing I was hoping we might have a collaborative discussion about, you know, that exercise in groupoidification.

Quiz 1: $K$ for Kleisli.

Quiz 2: I was suggesting presheaves of groupoids above. Given that a profunctor $F:PA\to B$ is a functor $PA\times B^{\mathrm{op}}\to \mathrm{Set}$, we could have a functor $PA\times B^{\mathrm{op}}\to \mathrm{Groupoid}$.

David wrote:

Quiz 1: K for Kleisli.

Right, the idea of defining a morphism from $A$ to $B$ to be a profunctor

$$PA⟶B$$

should remind us of the Kleisli construction, especially if we don’t worry much about which way the arrow is pointing… which is okay here, since a profunctor

$$X⟶Y$$

is the same as a profunctor

$$Y^{\mathrm{op}}⟶X^{\mathrm{op}}$$

And the resemblance is even clearer when we realize that $P$ is a kind of monad: the ‘free symmetric monoidal category on a category’ monad.

But there’s some serious technical work to be done here, which that paper goes ahead and does. First of all, $P$ starts out life as a categorified monad, or ‘pseudomonad’, on $\mathrm{Cat}$. Second of all, we need to enhance it to become a pseudomonad on $\mathrm{Prof}$. Third of all, we need to check that this pseudomonad on Prof really does have a kind of ‘Kleisli bicategory’.

Quiz 2: I was suggesting presheaves of groupoids above. Given that a profunctor $F:PA\to B$ is a functor $PA\times B^{\mathrm{op}}\to \mathrm{Set}$, we could have a functor $PA\times B^{\mathrm{op}}\to \mathrm{Groupoid}$.

Right. All this should work, in principle. If this is what you meant all along, I apologize for my elementary remarks before. But you’ll note that implementing your suggestion demands that we categorify the setup even more: instead of the 2-category $\mathrm{Prof}$ where an object is a category and a morphism is a functor

$$A\times B^{\mathrm{op}}\to \mathrm{Set}$$

you are suggesting that we work with some sort of 3-category where an object is a category (or 2-category) and a morphism is a weak 2-functor

$$A\times B^{\mathrm{op}}\to \mathrm{Gpd}$$

So, to actually implement this idea, you’d need to take the theory of monads and Kleisli categories and push it up to the 3-category level. And this is too much work for anyone to actually do, right now!

And this is roughly why Fiore and company say one cannot ‘directly recast’ the theory of stuff types into the language of generalized species.

In fact, I bet there’s a simpler reason they said this. I bet they just mean that stuff types aren’t examples of generalized species. I thought you didn’t understand this, so I thought I had to explain generalized species to you!

Remember, these are guys who don’t idly speculate in print about things they can’t do yet.

Remember, these are guys who don’t idly speculate in print about things they can’t do yet.

Perhaps they should visit us here sometime. Then we could ask what generalized species are good for.

Already we saw Fiore’s say

…generalised species encompass and generalise various of the notions of species used in combinatorics. Furthermore, they have a rich mathematical structure (akin to models of Girard’s linear logic) that can be described purely within Lawvere’s generalised logic. Indeed, I will present and treat the cartesian closed structure, the linear structure, the differential structure, etc. of generalised species axiomatically in this mathematical framework. As an upshot, I will observe that the setting allows for interpretations of computational calculi (like the lambda calculus, both typed and untyped; the recently introduced differential lambda calculus of Ehrhard and Regnier; etc) that can be directly seen as translations into a more basic elementary calculus of interacting agents that compute by communicating and operating upon structured data.

You may also be interested to read him say

I started working in domain theory, with my thesis Axiomatic Domain Theory in Categories of Partial Maps. There are many different categories of domains in which the same results hold–importantly adequacy theorems–and I wanted to show that these followed from general abstract principles. Thus, it was natural to axiomatize and investigate domain-theoretic models in this light. Along the way, and in enjoyable collaboration with various colleagues, I applied the axiomatic approach in different computational scenarios. In particular, with Eugenio Moggi and Davide Sangiorgi we constructed a denotational model of the $\pi$-calculus for which we established full abstraction axiomatically. Not much later, it was pointed out to me (at a PSSL meeting, if I remember correctly) that the constructor that we use for modeling bound output had been considered by André Joyal in the different setting of combinatorial species of structures as a differentiation operator. Ever since I’ve been interested in understanding and deepening the connection. Yet another piece was added to the puzzle by my work with Gordon Plotkin and Daniele Turi on algebraic theories with variable-binding operators. There an operator of context extension (again similar to that of differentiation) serves for modeling variable-binding. The first part of my contribution to the FOSSACS conference proceedings gives an outline of the unifying technical themes underlying these developments.

David wrote:

Then we could ask what generalized species are good for.

To me they’re just obviously good.

You should think of $\mathrm{Set}$ as a categorified version of a commutative ring, or rig.

So, you should think of a profunctor $A⟶B$ as a categorified version of a linear operator.

So, you should think of a profunctor $A⟶PB$ as a categorified version of a linear operator from a vector space to a polynomial algebra. You can also think of this as a polynomial function from one vector space to another.

(You’ll notice now I’m writing $A⟶PB$ instead of $PA⟶B$. I keep wanting to do that — you caught me doing it in my first comment, which I then corrected. This time I think I’m right to do so, but I could still have it backwards. In any case it’s easy to fix.)

So, I think it’s just obviously good to study these ideas, just like it’s obviously good to study vector spaces and polynomials.

But thanks for quoting Fiore about his motivations! Indeed, there’s a lot of cool but mysterious stuff going on in linear logic and now the differential lambda calculus, which suggests that logic is hybridizing first with linear algebra and now calculus. And this should be very related to the paper by Fiore, Gambino, Hyland and Winskel. After all, profunctors bring linearity into category theory, and generalized species bring in derivatives.

I know that Hyland is very much involved in this line of thought: when I was last in Cambridge, a few years ago, he organized a little micro-conference where Ehrhard explained the differential lambda calculus and I explained stuff types. I talked some more to Ehrhard this summer and we realized that he really is extending linear logic, which already includes an analogue of Fock space (= polynomial algebra), to also include annihilation and creation operators (= differentiation and multiplication operators)!

Feynman diagrams are sure to follow. Unfortunately there was still enough of a communication barrier that we weren’t able to fully comprehend the significance of it all. I barely understand linear logic, while he barely understands quantum field theory.

I think there should be some conferences where they take 4 or 5 people, throw them into a dungeon, and only let them out when they figure out what’s going on.