The n-Category Café

What can be said about when it’s possible to find a prequantum circle n-bundle for a given n-plectic manifold with integral form? Can they be classified?

Did you give this talk with the cohesive homotopy type theory prominent? I wonder what people make of it.

In view of this section, should representation theorists be learning this stuff?

Do you have an analogue of polarization for higher geometric quantization?

I see in answer to my question above about existence and uniqueness of lifts to circle bundles, that in the ordinary case bundle and connection exist and are determined up to isomorphism, but not canonically.

Did you give this talk with the cohesive homotopy type theory prominent? I wonder what people make of it.

So the idea of the thrust of this talk was to highlight at the beginning that there is a major problem in the community:

there are at least two proposals out there for how to formalize higher extended geometric prequantum theory. It is clear that both involve guesswork, since the examples to check against have not yet been worked out in much detail. Also, it is unclear how the two proposals would be related, how they might be equivalent.

So that’s a major problem. As I say at the beginning, there are two ways to improve on this situation:

1. explore the examples further, check wich formalism makes these examples match the consistency checks that we know have to be matched.

2. explore the general abstract theory further, figure out what general formal consistency and naturality conditions are.

Then I branched and said: the first point I discussed elsewhere. Here I want to focus on the second.

So then I argued that the next goal is to try to root geometric quantization as deeply as possible in general abstract foundational theory such that this automatically spits out the homotopy-theoretic improvement.

From this the next further steps:

1. by the motivating diagram at the beginning of the talk, it is clear that whatever we do we need to work in $\infty$-categories of $\infty$-stacks.

2. But to “root that more deeply” in general abstarct theory, we notice that such $\infty$-toposes are characterized entirely by just two or three general abstract properties (hi Charles!, if you are reading this here). Hence we should not worry too much about the definition of stacks as presheaves of something satisfying something in the present context, as usual. Insetad. we should go to that abstract root to find the structural origin of geometric quantization.

3. So I stated 2/3rds of these formal characteristics. The existence of the object classifier and local cartesian closure.

4. At that point, by just changing the notation just a tad, by passing from the symbols

   $$X \stackrel{\vdash E}{\to} Type$$

   for a morphism into the classifying $\infty$-stack of small fibrations to

   $$x : X \vdash E : Type$$

   we notice that we are much deeper at the absolute bottom of things than it might have seemed so far, because that’s a hypothetical judgement in natural deduction. And natural deduction is precisely what we are after here!

   If we can formulate our geometric quantization in $\infty$-stacks using really just those abstract properties of the collection of all these $\infty$-stacks, we have actually reduced to just pure logic. To something more basic than pure logic, even.

   And since that’s what we are after concerning point 2 of the motivation above, and since it is no extra work except changing the notation (which you can just as well ignore, hence), we’ll do it.

5. This is then finally nicely amplified by the form the main theorem takes in this notation. A prequantum $n$-bundle now reads

   $\nabla : \mathbf{B}^n U(1)_{conn} \vdash X(\nabla) : Type$

   and the first thing this makes you want to do is form its automorphism group

   $$\vdash \prod_{\nabla : \mathbf{B}^n U(1)_{conn}} X(\nabla) \stackrel{\simeq}{\to} X(\nabla) : Type \,.$$

6. Show that this structure, which is just two lines of code away from the very foundation of all of mathematics and homotopy theory subsumes one of the two proposals of how to do higher prequantum theory, but not the other. Namely Chris Rogers’. And it at the same time provides a bunch of further information.

7. So in conclusion the point of highlighting the type theory syntax: to highlight that we have achieved a general abstract justification of some proposal to a considerable “depth”, thereby strengthening the relevance of the argument.

That, anyway, was the idea and strategy of the talk. I think this should be a reasonable and reasonably interesting argument for somebody with the background in higher geometry and higher stacks that one needs in order to take about “string geometry” in the first place. So I thought it would be worth a try. I am of course aware that it may be perceived as pushing some boundary too far. But then, that’s what research talks are about: to show what happens when we push some boundary that hasn’t been pushed before. Right?