Prequantization in Cohesive Homotopy Type Theory

February 27, 2012

Prequantization in Cohesive Homotopy Type Theory

Posted by Urs Schreiber

$MathML-enabled post (click for more details).$

Chris Rogers and myself are studying structures in higher (meaning: ∞-categorified) geometric (pre)quantization. Later this year I may post something about the higher structures that appear in this context, but right now I will highlight something else.

Our constructions proceed in two steps. First we give a general abstract axiomatic definition of geometric (pre)quantization internal to any cohesive ∞-topos. In the next step we pass to suitable models of the axioms and work out how there this reproduces the traditional notions as well as various generalizations of these that have been proposed, and usefully generalizes all this in various way.

In other words, we formulate geometric prequantization in cohesive homotopy type theory and then study its models. Since here in the $n$ Café we had, in the last months, discussed most of the relevant ingredients before, I thought it would be fun to highlight just this step.

See Prequantum physics in a cohesive ∞-topos for more exposition.

Technical details on what I say below are in section 2.3.24 (general definitions) and section 3.3.17 (models in smooth cohesion).

$MathML-enabled post (click for more details).$

So we set ourselves up with the axioms of cohesive homotopy type theory. (Myself, I’ll be talking here in the pseudocode formerly known as traditional mathematics, but recall that Mike Shulman, in a heroic effort, had fully formalized all this, the code being here, the documentation being here. )

All we need to to set up geometric prequantization are the structures that we produced in HoTT Cohesion, exercise II. There, starting with a type $A$ equipped with abelian group structure, we produced for all $n \in \mathbb{N}$ types denoted $\mathbf{B}^{n+1} A$ , $\mathbf{B}^{n+1}A_{conn}$ and $\Omega^{n+2}_{cl}(-,A)$ , equipped with maps

$\array{ \mathbf{B}^{n+1} A_{conn} &\to& \Omega^{n+2}_{cl}(-,A) \\ \downarrow \\ \mathbf{B}^{n+1} A } \,.$

Here the bottom type is to be thought of as the moduli $\infty$ -stack of $\mathbf{B}^n A$ -principal bundles, the top left type as the moduli $\infty$ -stack of $\mathbf{B}^n A$ -principal connections, and the top right as the coefficient type for closed $(n+2)$ -forms with values in $A$ .

Let now $X$ be any other type. We say a higher presymplectic structure ( pre-(n+1)-plectic structure ) on $X$ is a term of function type

$\omega : X \to \Omega^{n+2}_{cl}(-,A) \,.$

A prequantization of $\omega$ to a prequantum $\infty$ -bundle is a lift $\hat \omega$ in

$\array{ && \mathbf{B}^{n+1} A_{conn} \\ & {}^{\mathllap{\hat \omega}}\nearrow & \downarrow \\ X &\stackrel{\omega}{\to}& \Omega^{n+2}_{cl}(-,A) } \,.$

In general a prequantization need not exist, and if it exists, it need not be unique. Both existence and non-uniqueness can be cleanly characterized, but let’s not get into this right now. Instead, assume that a choice can and has been made.

Then the following further structure is canonically induced.

Regard $\hat \omega$ as a dependent type over $\mathbf{B}^{n+1} A_{conn}$ . As such, let

$\mathcal{P} := Aut_{/\mathbf{B}^{n+1}A_{conn}}(\hat \omega)$

be its group type of auto-equivalences. Call this the Poisson $\infty$ -group of the given presymplectic structure.

While we haven’t talked about $\infty$ -Lie algebra types in cohesive homotopy type theory before, I mention just for completeness that there is such a thing associated with $\mathcal{P}$ , and it is to be called the Poisson $\infty$ -Lie algebra (or $\infty$ -Lie algebra underlying the $\infty$ -Poisson algebra ) of $\omega$ .

We need now one more choice, the choice of a representation of the group type $\mathbf{B}^n A$ . This is simply any term

$\rho : V//\mathbf{B}^n A \to \mathbf{B}^{n+1}A$

with the codomain as indicated. For $V$ the homotopy fiber type of $\rho$ , we say this defines a representation of $\mathbf{B}^n A$ on $V$ , and that the fiber sequence

$V \to V//\mathbf{B}^n A \to \mathbf{B}^{n+1}A$

is the $V$ -bundle $\rho$ -associated to the universal $\mathbf{B}^n A$ -principal $\infty$ -bundle.

With $g$ the composite

$g : X \stackrel{\hat \omega}{\to} \mathbf{B}^{n+1}A_{conn} \to \mathbf{B}^{n+1}A$

define

$\Gamma_X(E) := [g, \rho]_{\mathbf{B}^{n+1}A}$

to be the type of functions from $X$ to $V//\mathbf{B}^{n+1}A$ over $\mathbf{B}^{n+1}A$ . We call this the type of sections of the prequantum $\infty$ -bundle or equivalently the prequantum space of states.

Looking at these definitions, one finds that there is a canonical action

$\mathcal{P} \times \Gamma_X(E) \to \Gamma_X(E)$

of the Poisson $\infty$ -group on the prequantum space of states. Write $\exp(q)$ for some term of type $\mathcal{P}$ . The image $\exp(\hat q)$ of a term $\exp(q)$ under the corresponding map

$\mathcal{P} \to End( \Gamma_X(E) )$

we call the prequantum operator associated with $\exp(q)$ .

That’s it. That’s prequantization. Or, in fact, homotopy prequantization.

Proposition. Let $(X, \omega)$ be an ordinary smooth symplectic manifold. Then when regarded, canonically, as an object in the model Smooth∞Grpd for cohesive homotopy type theory, its traditional prequantizations are equivalent to those induced from the above axiomatics.

In particular, the $\mathcal{P}$ from above is equivalent to the group that integrates the Lie algebra underlying the Poisson algebra of $(X, \omega)$ .

This is shown in section 3.3.17

In order to get axiomatics for genuine quantization all that remains to axiomatize are suitable choices of subtypes of $\Gamma_X(E)$ (by “polarization”), to be called the genuine spaces of quantum states. Let’s leave this for another time.

Posted at February 27, 2012 6:43 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2503

13 Comments & 1 Trackback

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

Just to clarify the record: my memory is that we started with a type denoted $\mathbf{B}^{n+2} A$ , merely intended to be thought of as the $(n+2)$ -fold delooping of a “type $A$ with abelian group structure”, and postulated a map $\Omega_{cl}^{n+2}(-,A) \to \flat_{dR} \mathbf{B}^{n+2} A$ , about the domain of which nothing was said except that it was supposed to be 0-truncated. I don’t think we know yet (in homotopy type theory, as opposed to $(\infty,1)$ -topos theory) how to produce $\mathbf{B}^{n+2} A$ from $A$ , and I don’t recall anything being said about how to construct $\Omega_{cl}^{n+2}(-,A)$ . Am I misremembering?

Posted by: Mike Shulman on February 28, 2012 2:32 AM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

we started with a type denoted $\mathbf{B}^{n+2}A$ , merely intended to be thought of as the $(n+2)$ -fold delooping of a “type $A$ with abelian group structure”,

True, I am using a bit more $\infty$ -topos lingo here than we had strictly related to Coq-code before, just so as to be able to speak more freely.

In an $\infty$ -topos the statement that $A$ has $n+2$ -tuply group structure is of course equivalent to there being a pointed $(n+1)$ -connected object $\mathbf{B}^{n+2}A$ looping to it, so the latter may be taken as the definition here. (We don’t need that $A$ is even further deloopable here, I just said this out of habit.)

and postulated a map $\Omega_{cl}^{n+2}(-,A) \to \flat_{dR} \mathbf{B}^{n+2}A$ , about the domain of which nothing was said except that it was supposed to be 0-truncated.

And the map was required to be an effective epi. So it’s required to be an “atlas” for $\flat_{dR} \mathbf{B}^{n+2}A$ .

Posted by: Urs Schreiber on February 28, 2012 6:35 AM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

Urs, this might be off-topic, but I’m reminded of some discussions we had about the relation of geometric quantization to deformation quantization. I’m mostly interested in figuring out whether the two can be shown to either agree or disagree in interesting cases.

For example, the nLab page on geometric quantization says that the symplectic form $\omega$ must belong to a certain integral cohomology class. Otherwise, the desired pre-quantum $U(1)$ -line bundle with connection just doesn’t exist. On the other hand, the Fedosov deformation of a symplectic manifold also requires a connection. But this connection is defined on tensor bundles such that the symplectic form is constant. Apparently such a symplectic connection exists for an arbitrary symplectic manifold.

Now, it looks to me like for symplectic manifolds with a symplectic form of a non-integral cohomology class, the geometric quantization construction yields nothing, while deformation quantization yields something. Is this enough to conclude that the two constructions yield different outputs in general? Are there important cases where one would want to apply geometric quantization but the integrality condition just doesn’t hold?

Posted by: Igor Khavkine on February 28, 2012 11:42 AM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

Hi Igor,

thanks, very good question. Here a lightning reply, since I have to run:

Yes, if we set $A = U(1)$ in the above, then that existence condition which I alluded to is that $\omega$ has to be integral, which is the condition that it is the curvature of some connection.

I will comment on the rest that you said later. I have to urgently run now, there is some activity that needs all my attention, today and most of tomorrow. I’ll get back to you on this on Thursday!

Posted by: Urs Schreiber on February 28, 2012 11:54 AM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

Hi Igor, okay, I have now found a minute (or rather, I stole it).

You write:

Now, it looks to me like for symplectic manifolds with a symplectic form of a non-integral cohomology class, the geometric quantization construction yields nothing, while deformation quantization yields something. Is this enough to conclude that the two constructions yield different outputs in general?

I wouldn’t think so. I think the way to look at is this:

geometric quantization emphasises the space of states and has “problems” with the algebra of observables,

while

deformation quantization emphasizes the algebra of observables and has “problems” with the space of states.

If the former does not exist, it means that certain nice constructions of state spaces don’t exist. But if the former, and hence both quantizations exist, they are – or at least can be – closely related. There is discussion of this in

Christoph Nölle, Geometric and deformation quantization (arXiv:0903.5336) .

We talked about the following before, but let me add a few remarks on why I happen to be interested in geometric quantization here.

a) Geometric quantization is naturally adapted to quantization of Chern-Simons theory (standard references are here), and – in view of the above dichotomy “state space $\leftrightarrow$ observable algebra” – generally to that of topological quantum field theories. As you know, the kind of discussion as in the above entry is aiming, among other things, at quantization of infinity-Chern-Simons theories.

b) In this context we found that the issue of choosing a prequantum line bundle for a given symplectic structure is a red herring. The action functionals of (higher) Chern-Simons theories that we construct via infinity-Chern-Weil theory automatically and naturally come not just with their prequantum circle bundles, but even naturally come with their prequantum circle $n$ -bundles on the fully extended configuration space (of which the ordinary prequantum circle bundle is just the transgression to codimension 1).

For instance the action functional of ordinary Chern-Simons theory naturally derives from the “differential first fractional Pontryagin class”

$\frac{1}{2} \hat {\mathbf{p}}_1 : \mathbf{B}G_{conn} \to \mathbf{B}^3 U(1)_{conn} \,,$

which is already a prequantum circle 3-bundle (2-gerbe) on the moduli stack of Chern-Simons field configurations.

Or for instance for 7d String-Chern-Simons theory the action functional naturally derives from

$\frac{1}{6} \hat {\mathbf{p}}_2 : \mathbf{B}String_{conn} \to \mathbf{B}^7 U(1)_{conn} \,,$

which is already a prequantum circle 7-bundle (6-gerbe) on the moduli 2-stack of field configurations.

So I am faced with a large zoo of quantum field theories for which not only the geometric prequantization exists, but is naturally given and naturally extended to full codimension. That makes the use of geometric quantization here very suggestive, if not compelling.

Finally a question for you, also related to something we talked about before:

by what I just said, what I actually have is prequantization bundles already off-shell. In fact, if you look at the discussion of the above entry, there is a little bonus hidden there:

no-where do I need to assume that the form $\omega$ is non-degenerate, i.e. that it is symplectic in the ordinary case, or $n$ -plectic in the higher cases. The above formalization of geometric quantization among other things also generalizes it to presymplectic / pre- $n$ -plectic forms.

So what would seem most natural in view of what the machinery gives us is to consider off-shell quantization here – “off-shell geometric quantization”, to coin a term (?).

I still need to further chew on this to see what it wants to do with me, but I thought I’d mention it. Since you thought about off-shell quantization (from the deformation quantization perspective) much more than I have, you might have some useful insight for me at this point.

Posted by: Urs Schreiber on February 28, 2012 6:57 PM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

Urs, thanks for your comments and the reference to Nölle’s paper. I wanted to look it over before following up. Now I have, at least superficially. I have to say that I did not spend enough time on it to follow the main construction, but I’m more or less convinced that one in fact can relate geometric and deformation quantizations if they both exist. Still a couple of remarks about that paper. First, it’s interesting that Fedosov’s construction for symplectic manifolds also has a topological obstruction: the second Stiefel-Whitney class must vanish. Unfortunately, I don’t have a good grasp on what that means in terms of practical difficulties in examples of interest. Second, while Nölle gives the physically and mathematically correct condition for equivalence of quantizations (his eq. 7.1), he then go out of his way to argue the opposite, based on what seems to me like misplaced physical intuition. This leads him, unfortunately, to concluded that there are many more inequivalent quantizations than there should be.

OK, I should say something about the “problem with states” in deformation quantization. Physically speaking, I think there is no real such problem. In fact Nölle already points this out in his introduction (though I’m sure the same thing is pointed out in many places). Namely, given a *-algebra of observables, the GNS construction gives all the Hilbert spaces one might want. One might ask where the positive states needed to initiate the GNS construction come from and how the notion of positivity should be translated to the context of formal power series. Both questions are attacked head on and solved, at least in my limited understanding of it, in Waldmann’s work on states in deformation quantization (arXiv:math/0408217). Essentially, classical sates (probability distributions on phase space) get deformed into perturbatively positive functionals on the deformed algebra of observables. Since both observables and states are functions or distributions on phase space, what one recovers this way is the perturbative version of the well known phase space picture of quantum mechanics, where states are represented by Wigner functions. In the case of the standard symplectic structure on $\mathbb{R}^{2n}$ , this picture is well known to be equivalent to either the Schroedinger or Heisenberg ones. The folks in the AQFT community have also done some work in on deforming states on a non-interacting field theory to states on an interacting one. I can dig up the references if needed.

Of course, the GNS construction may be a bit to abstract for some tastes and purposes. One may ask if the resulting Hilbert space can be isometrically identified with a Schroedinger-like $L^2$ space, like the ones constructed in geometric quantization. According to Nölle, that is indeed possible, with the same isometry mapping some observables to operators constructed in geometric quantization. Unfortunately, I didn’t quite get from his paper how complete this identification is. However, at least for me, conceptually, as far as the construction of a formal quantization of the algebra of observables as well as a representation of it on some Hilbert space, the connection to geometric quantization is purely a matter of convenience. The main advantage of having this connection made explicit that I can see is the possibility of making the deformation quantization strict, rather than just formal. Though, I also didn’t catch from Nölle’s paper how strong the chance of making that work is. On the other hand, if the results of deformation and geometric quantization agree in some case and the geometric construction is much simpler, then all the more power to it. Perhaps that is the case with the Chern-Simons theories you are dealing with.

Finally, perhaps I can add a few words about the “off-shell” business. I’m not sure that a degenerate (pre)symplectic form can be immediately identified with working off-shell. The off-shell picture that we’ve discussed before incorporates all possible field configurations, without restricting them by the equations of motion. While the covariant phase space method does provide a closed vertical 2-form/horizontal current density $\omega$ , it is not horizontally conserved (that only holds after imposing the equations of motion). Hence the closed vertical 2-form $\Omega$ obtained by integrating this current density $\omega$ over a codim-1 surface $\Sigma$ strongly depends on $\Sigma$ . Thus it is awkward to work with the space of all field configurations equipped with $\Omega$ as a (pre)symplectic manifold.

The way the off-shell picture is usually obtained is via Poisson structure, rather than the (pre)symplectic structure. First one restricts to the space of solutions, which is symplectic phase space in all the usual ways. Then the Poisson bracket is obtained by inverting the symplectic form. The Poisson bracket is then lifted the algebra of functions on the space of all field configurations. Thus one gets an off-shell Poisson algebra, wich can then be quantized via deformation quantization. The lift is of course not unique, but sometimes symmetries single out a particular one. The lift is discussed explicitly in the original papers of Marolf on this subject: arXiv:hep-th/9308141, arXiv:hep-th/9308150.

Posted by: Igor Khavkine on March 1, 2012 12:39 AM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

I’m not sure that a degenerate (pre)symplectic form can be immediately identified with working off-shell.

Sure. That’s also not what I meant. I didn’t say this well, I suppose. Let me try again:

the statement is that in the class of cases that I am thinking of, there naturally is an integral presymplectic / pre- $n$ -plectic form already on the full configuration space of fields (space of histories), not just on the phase space.

Posted by: Urs Schreiber on March 1, 2012 9:02 PM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

I see. Well, that certainly unusual. Does this off-shell presymplectic form pull back to the standard symplectic form along the inclusion of solutions in the space of histories? If so, then you are in a special case of the constrained Hamiltonian formalism, where the phase space you are interested (the solution space) is realized as a subspace of a larger, extended phase space (the space of histories). Don’t know if that helps the picture you have at all.

Posted by: Igor Khavkine on March 1, 2012 9:58 PM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

Just two small comments regarding obstructions to geometric quantization. First, there is a way to relate a closed 2-form $\omega$ to a geometric object, regardless of whether [ $\omega$ ] is integral or not. Such a 2-form is a flat connection on the trivial $U(1)$ -gerbe. So perhaps “higher geometric quantization” could shed some light on the non-integral symplectic case…

Second, perhaps it is worth mentioning that there are symplectic manifolds which are not polarizable. So even if we had $[\omega]$ integral, in these cases, the usual recipe in GQ would be unable to produce a space of quantum states.

Posted by: Chris Rogers on March 2, 2012 11:49 PM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

How do you begin to guess which kind of elements of geometry are likely to belong to all geometries, i.e., are structures common to all cohesive $\infty$ -toposes, and which are part of a specific geometry? Should we expect, say, contact geometry to be general?

Posted by: David Corfield on February 28, 2012 9:33 PM | Permalink | Reply to this

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

How do you begin to guess which kind of elements of geometry are likely to belong to all geometries, i.e., are structures common to all cohesive ∞-toposes, and which are part of a specific geometry?

By trial and error.

At any time, I have a bunch of structures in mind of which I would like to know their most abstract formulation. I play around, talk to people, sleep over it, and at some point some answers reveal themselves. Others never do.

In this case, Chris Rogers had been visiting Utrecht, we chatted about his thesis, started drawing wild diagrams to the blackboard, and somehow the answer appeared.

That bit has to come by itself, it’s hard to force it. Once one has a good guess this way, the rest is effort working out what it comes down to in various examples, known ones, expected ones.

Should we expect, say, contact geometry to be general?

Good question. I don’t know.

What usually helps is to watch people try to generalize a concept, and see how it reacts, and if it reveals its inner secrets.

Sorry, I guess I am rambling. I am just using your question as a welcome excuse to procrastinate working on what I should really be working on right now.

Let me come back to this interesting question with more leisure tomorrow evening.

Posted by: Urs Schreiber on February 28, 2012 9:51 PM | Permalink | Reply to this

2-Plectic geometry and its prequantization

$MathML-enabled post (click for more details).$

In the above entry I stated that the general definition of Poisson bracket $\infty$ -Lie algebra in a cohesive $\infty$ -topos reproduces the ordinary such notion, and its prequantization, when modeled in the context of smooth cohesion.

But of course we care about this fact because, in consequence, it provides a machine to obtain higher / categorified analogs of these ordinary notions.

One higher analog of Poisson brackets has been proposed by Chris Rogers, in the context of n-plectic geometry for all $n \in \mathbb{N}$ . Here the base space $X$ is still a smooth manifold (instead of, more generally, an orbifold, Lie groupoid, …, smooth $\infty$ -groupoid), but the symplectic 2-form is replaced by a differential $(n+1)$ -form $\omega$ . Naturally, and in accord with the above general story, a choice of prequantization is now a choice of of circle n-bundle with connection, whose curvature is $\omega$ . The Poisson bracket $\infty$ -Lie algebra should now be one on Hamiltonian $(n-1)$ -forms, and Chris gives a natural proposal for such an L-infinity algebra structure (see n-plectic geometry and the references listed there).

Of course the natural claim is going to be: when an $n$ -plectic manifold is naturally regarded in the cohesive $\infty$ -topos Smooth∞Grpd, then the above homotopy type theoretic formulation of prequantization applied to it reproduces Chris’s $n$ -plectic prequantization.

For $n = 2$ the details of this statement and of its proof are now spelled out in section 3.3.17.2.

Posted by: Urs Schreiber on March 6, 2012 11:47 AM | Permalink | Reply to this

Read the post Flat Ehresmann connections in Cohesive HoTT
Weblog: The n-Category Café
Excerpt: The formalization of flat Ehresmann connections in higher geometry.
Tracked: June 28, 2012 6:37 PM

Re: Prequantization in Cohesive Homotopy Type Theory

$MathML-enabled post (click for more details).$

There is now a bit more related material appearing at nLab:higher geometric quantization

Posted by: Urs Schreiber on July 3, 2012 2:39 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

February 27, 2012