### Prequantization in Cohesive Homotopy Type Theory

#### Posted by Urs Schreiber

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).

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.

## Re: Prequantization in Cohesive Homotopy Type Theory

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?