Schreiber Erlangen2012

These are expanded notes for a talk that I gave at the workshop

• From Poisson to String Geometry, Erlangen (2012)

on a topic in the context of differential cohomology in a cohesive topos.

---

Motivating question

The phase space of a mechanical system is essentially a symplectic manifold, and geometric quantization is a process that sends this to the corresponding quantum mechanical system. On the other hand, the extended phase space of an $n$-dimensional classical field theory is an n-plectic manifold, and we expext that some form of higher geometric quantization takes this to the corresponding extended quantum field theory.

Here we consider a conceptual question in this generalization of symplectic geometry and its geometric quantization to n-plectic geometry and its higher geometric quantization.

So consider a symplectic manifold $X$ with symplectic form $\omega \in \Omega^2_{cl}(X)$. For the following we want to view this in terms of sheaves: closed differential 2-forms naturally form a sheaf $\Omega^2_{cl}(-) : SmthMfd^{op} \to Set$ on the site SmthMfd of smooth manifolds, as does of course $X$ itself, via $C^\infty(-,X) : SmthMfd^{op} \to Set$.

Then by the Yoneda lemma, a symplectic form $\omega \in \Omega^2_{cl}(X)$ is equivalently a morphism in the sheaf topos $Sh(SmthMfd)$ of the form:

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

There is also a (2,1)-sheaf or stack of groupoids $\mathbf{B} U(1)_{conn}$ on $SmthMfd$ such that a morphism

$$\nabla : X \to \mathbf{B} U(1)_{conn}$$

in the (2,1)-topos of (2,1)-sheaves is equivalently a circle bundle with connection (and such that a homotopy between two such morphisms is a smooth gauge transformation of these bundles). This comes with a morphism, of (2,1)-sheaves $F_{(-)} : \mathbf{B}U(1)_{conn} \to \Omega^2_{cl}(-)$, sending a connection to its curvature 2-form $\omega = F_{\nabla}$, expressed the the commutativity of the diagram

$$\array{ && \mathbf{B}U(1)_{conn} \\ & {\nabla}^{\mathllap{}}\nearrow & \downarrow^{F_{(-)}} \\ X &\underset{\omega}{\to}& \Omega^2_{cl}(-) } \,.$$

If on the other hand $\omega$ is given (and symplectic, hence non-degenerate), then the lift $\nabla$ is called a prequantum circle bundle for $\omega$. In geometric quantization one tries to obtain the quantum mechanics of $(X,\omega)$ regarded as a phase space by constructions on such a prequantum bundles.

But ordinary geometric quantization is fully well suited only for quantum mechanics, hence for 1-dimensional quantum field theory. More generally, the extended phase space of an $n$-dimensional quantum field theory naturally carries a closed differential form of degree $(n+1)$. A natural question to ask is therefore if there is a higher-degree analog of geometric quantization usefully adapted to these higher degree forms on extended phase spaces. In other words: What is higher geometric quantization?

This question reaches into largely unexplored territory with currently only a few hints giving orientation. Accordingly, different people have made different proposals for how the theory should proceed.

For instance in the context of multisymplectic geometry, Kanatchikov observed that an n-plectic manifold carries a graded Leibniz algebra generalizing the Poisson bracket Lie algebra of an ordinary symplectic maniifold, and Hrabak made proposals (see here) for how to extend BV-BRST formalism to such a situation, crucial for the quantization of gauge theories. There is however no analog of the prequantum circle bundle in this work so far and hence the nature of geometric quantization is not retained.

It is noteworthy that Kanachikov’s construction involves dividing out certain Hamiltonian forms: the straightforward generalization of the definition of the Poisson bracket from symplectic forms for $n$-plectic forms fails to satisfy the Jacobi identity by an exact form. Quotienting out these Jacobiators Kanatchikov enforces a binary bracket structure.

But the appearance of nontrivial Jacobiators is of course the hallmark of Lie theory generalized to homotopy theory: of L-∞ algebras. Indeed, Chris L. Rogers observed that if not dividing out anything, then the evident Poisson bracket of an $n$-plectic form on a smooth manifold extends to a Lie n-algebra. He also considers circle n-bundles with connection as the natural higher generalization of prequantum circle bundles. What has however not been clarified yet is how the BV-BRST formalism would generalize to this approach.

In summary these two proposals for how to start the theory of higher geometric quantization are:

• Kanatchikov, Hrabak (1999): Poisson bracket graded Leibnitz algebra + BRST, but no prequantum bundle (see here).

• Chris L. Rogers (2011): Poisson bracket Lie n-algebra and prequantum circle n-bundle with connection, but no BRST (see here).

At the moment it is not clear how these two approached would be usefully related, and therefore one is left wondering what the right direction to proceed would be. Evidently it is difficult and dangerous to proceed just by guesswork and intuition. One needs more guidance from

1. concrete particular phenomena (examples)

2. abstract general phenomena (theory).

The purpose of the present note is to consider guidance from abstract generals. The theorem presented below states that a notion of higher Poisson bracket Lie algebras – and in fact even of the higher Heisenberg group/quantomorphism group that Lie integrates it – is automatically induced by a formalization of the foundations of differential geometry/differential cohomology in the formal language of cohesive homotopy type theory (Schreiber-Shulman). And when interpreted in the relevants models, we show that it reproduces Chris Rogers‘ proposal for Poisson Lie $n$-brackets, and thereby generalizes this from smooth manifolds to more general geometric objects.

Here we indicate this natural general abstract formalization of the notion of higher quantomorphism groups. The actual proof of the main theorem below, that this subsumes Rogers’ construction, comes down to a lengthy computation in differential geometry, which the reader may find spelled out in (Schreiber, section 4.4.17). This is joint work with Chris Rogers. A writeup should appear later this year.

Homotopy type theory

Since our goal is to see how deep in the grand scheme of things we can root the notion of higher geometric quantization, we consider here a formalism that reaches deep to the foundations of mathematics and at the same time provides a natural foundation for many aspects of quantum field theory (namely cohesive homotopy type theory, the relevant aspects of which we briefly introduce now).

So: consider an∞-topos_ $\mathbf{H}$. That means:

• there is a site (or rather: (∞,1)-site) $C$ (for instance that of smooth manifolds, mentioned above) and $\mathbf{H}$ is the (∞,1)-category of (∞,1)-sheaves hence of higher stacks over $C$, $\mathbf{H} \simeq Sh_\infty(C)$.

One concrete way to think of this is as follows: if $C$ is a site with enough points, then $\mathbf{H}$ is obtained from the category of simplicial presheaves $Func(C^{op}, sSet)$ by simplicial localization, by universally sending stalkwise weak homotopy equivalences to homotopy equivalence:

$$\mathbf{H} \simeq L_{local\;whe} Func(C^{op}, sSet) \,.$$

For instance

• for $C = *$ we have $\mathbf{H} \simeq$ ∞Grpd, which geometrically is to be thought of as Disc∞Grpd, the collection of discrete ∞-groupoids;

• for $C =$ SmthMfd or CartSp${}_{smooth}$, an object of $\mathbf{H} \simeq$ Smooth∞Grpd is a smooth homotopy type, a joint generalization of smooth manifolds, orbifolds, Lie groupoids and differentiable stacks.

But it is noteworthy that apart from this sheaf-theoretic description, ∞-toposes also have an entirely abstract characterization by just a handful of general properties that do not mention any notion of stack explicitly. Our theorem below can be and will be stated entirely in terms of these abstract properties only. This way of speaking about ∞-toposes – or rather: internal to ∞-toposes – has come to be known as homotopy type theory, a system of formal logic that captures modern homotopy theory. Since we are after a fundamental theoretical justification of notions of higher geometric quantization, this seems to be a suitable framework to base our discussion on, and hence we spend here a few introductory words on the basics that we need below.

The abstract properties of an ∞-topos that we need are

1. it has an object classifier;

2. it is a locally cartesian closed (∞,1)-category, equivalently: it has base change geometric morphisms over all its morphisms,

which we turn to now.

Object classifier

In $\mathbf{H}$ there is an object $Type \in \mathbf{H}$ called the small object classifier, which is the internal universe of small objects, in that it is the representing object for the core of the small codomain fibration:

The corresponding equivalence of ∞-groupoids

$$name : Core(\mathbf{H}_{/X})^{small} \stackrel{\simeq}{\to} \mathbf{H}(X,Type)$$

sends an $X$-family of objects $(E \to X) \in \mathbf{H}_{/X}$ to its “name”:

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

defined by fitting into an ∞-pullback diagram of the form

$$\array{ E &\to& \widehat{Type} \\ \downarrow &\swArrow_{\simeq}& \downarrow \\ X &\underset{\vdash E}{\to}& Type } \,.$$

=–

Since this way the $\infty$-topos $\mathbf{H}$ “reflects on itself” via $Type$, it is useful to consistently speak of all objects in a slice $\mathbf{H}_{/X}$ entirely in terms of their “names” this way (the “internal language” of $\mathbf{H}$). This equivalent point of view is highlighted with a slight change of notation, adopted from formal logic:

instead of drawing the symbols for a morphism

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

we will draw symbols like this:

$$x : X \vdash E(x) : Type \,,$$

called a sequent, but meaning precisely the same as the morphism-notation before.

Similarly, instead of the symbols

$$X \stackrel{t}{\to}_X E$$

for a morphism in the slice $\mathbf{H}_{/X}$ – a generalized element of $E$ – , we may equivalently write the sequent symbols

$$x : X \vdash t(x) : E(x)$$

to express the same state of affairs (behind all this is the relation between type theory and category theory).

In summary we have the following dictionary

morphisms to sequents

$\,$	types	terms
∞-topos theory	$\;\;\;\;X \stackrel{\vdash \;\;\;\;E}{\to} \;\;\Type$	$\;\;\;\;X \stackrel{\vdash \;\;\;t}{\to} {}_X \;\;E$
homotopy type theory	$x : X \vdash E(x) : Type$	$x : X \vdash t(x) : E(x)$

While nothing changes about our statements whether we use symbols as on the top or on the bottom of this disctionary, the top row is more closely related to the higher geometry that we want to describe, whereas the bottom row is more closely related to the type theoretic foundations of mathematics. It turns out that the general definition of the quantomorphism n-group is simplest actually in the latter formulation, and so we amplify that one here as support for our claim that we give a deep theoretical justification for Chris Rogers‘ definition of n-plectic geometry.

Local cartesian closure

The other crucial general abstract property of ∞-toposes which we need is that they are locally cartesian closed ∞-categories.

This means that for each $X \in \mathbf{H}$, hence $\vdash X : Type$, the slice ∞-topos $\mathbf{H}_{/X}$ is a cartesian closed ∞-category: for each $(E \stackrel{e}{\to}X ) \in \mathbf{H}_{/X}$, hence for each $x : X \vdash E(x) : Type$, there is a pair of adjoint ∞-functors

$$(e \times (-) \vdash [e,-]) : \mathbf{H}_{/X} \to \mathbf{H}_{/X} \,,$$

given by cartesian product and internal hom in the slice. (In the language of stacks one calls $[e,f]$ here the relative mapping stack.)

Since this is by definition internal to the slice, if follows that an internal hom $[e,f]$ is again given by a morphism $([e,f] \to X)$ over $X$. This means by the above that there should be notation of the form $x : X \vdash \cdots$:

given an $x : X \vdash E(x) : Type$ and $x : X \vdash F(x) : Type$ we write $[e,f] \in \mathbf{H}_{/X}$ as the “dependent function type”

$$x : X \vdash E(x) \to F(x) : Type \,.$$

Even if this is just notation, it is in fact more suggestive and more illuminating than the standard category theoretic notation: it expresses manifestly that the internal hom in a slice ∞-topos is given by forming the collection of morphisms $E(x) \to F(x)$ homotopy fiber-wise over generalized elements $x \in X$.

Often one is interested in the subobject $[e,f]_{\simeq} \hookrightarrow [e,f]$ of the internal hom on only those morphisms that are equivalences. This is written in homotopy type theory-notation suggestively as

$$x : X \vdash E(x) \stackrel{\simeq}{\to} F(X) : Type \,.$$

In particular, this means that the expression

$$x : X \vdash E(x) \stackrel{\simeq}{\to} E(X) : Type \,.$$

gives an ∞-group or group-∞-stack: the automorphism ∞-group of $E$ over $X$. The quantomorphism ∞-group below is obtained from such an relative automorphism ∞-group.

Base change

We need one last notational ingredient to be able to formulate quantomorphism n-groups in the foundational internal language of homotopy type theory, namely for base change geometric morphisms. (Their existene is actually equivalent to the internal homs discussed before, see at locally cartesian closed category).

For $(X \stackrel{f}{\to} Y)$ any morphism in the ∞-topos $\mathbf{H}$, there is an adjoint triple of ∞-functors called and denoted as follows:

(dependent sum $\dashv$ base change $\dashv$ dependent product)= $(\sum_f \dashv f^* \dashv \prod_f) \;:\; \mathbf{H}_{/X} \stackrel{\overset{\sum_f}{\to}}{\stackrel{\overset{f^*}{\leftarrow}}{\underset{\prod_f}{\to}}} \mathbf{H}_{/Y}$.

For instance if

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

is a morphism $(E \stackrel{e}{\to} X)$ in $\mathbf{H}$ over $X$, then we obtain from this the object $\prod_{X \to *} (E \stackrel{e}{\to} X) \in \mathbf{H}$, which in homotopy type theory notation is just

$$\vdash \prod_{x : X} E(x) : Type \,.$$

This is the object of sections of $E \to X$.

The Theorem

Using the foundational internal language of homotopy type theory indicated above, we now

1. express a conceptually simple and natural construction in the internal language of any ∞-topos that is cohesive

2. claim that when interpreted over smooth manifolds this structure

   1. reproduces Chris Rogers‘ definition of Poisson-bracket Lie n-algebras,

   2. generalizes it to arbitrary smooth ∞-stacks,

   3. gives its Lie integration to the quantomorphism n-groups

   4. and provides its ∞-action on the higher space of states (in geometric quantization).

Cohesion

The extra axiom needed for all matters of differential geometry/differential cohomology on those of plain homotopy type theory is cohesion, and expression of the fact that in a context of higher geometry the points of a space “hand togther” or “cohere” in a geometric way, as the points in an open ball do in topology (continuously) and in differential geometry (smoothly).

The details of this extra axiom are described

Here we just need that this axiom implies in particular that for every object $X \in \mathbf{X}$ there is an object $\flat X$

$$X : Type \vdash \flat X : Type$$

which behaves as the moduli ∞-stack of flat coefficients in $X$. Notably if $X = \mathbf{B}\mathbb{G}$ is the moduli ∞-stack of an ∞-group $\mathbb{G}$, the $\flat \mathbf{B} \mathbb{G}$ is the moduli for flat $\mathbb{G}$-principal ∞-connections. So for $X \in \mathbf{H}$ we have that an object

$$X \stackrel{\nabla}{\to} \flat \mathbf{B}\mathbb{G} \;\;\; \in \;\;\; \mathbf{H}_{/X}$$

hence

$$\nabla : \flat \mathbf{B}\mathbb{G} \vdash X(\nabla) : Type$$

is a flat $\mathbb{G}$-principal $\infty$-connection on $X$. With $\flat$ comes a canonical morphism

$$UnderlBdl : \flat \mathbf{B}\mathbb{G} \to \mathbf{B}\mathbb{G}$$

which sends such a flat connection to its underlying principal ∞-bundle

$$\mathbf{c} : \mathbf{B}\mathbb{G} \vdash \sum_{{\mathbf{c} =} \atop {UnderlBdl(\nabla)}} X(\nabla) : Type \,.$$

Using the formal properties of $\flat$ in cohesive homotopy type theory, one finds that for the case that $\mathb{G}$ is an abelian (E-∞) ∞-group and using a given notion of manifolds, there is canonically a refinement of $\flat \mathbf{B}\mathbb{G}$ to an object

$$\mathbf{B}^{n+1} \mathbb{G}_{conn} \in \mathbf{H}$$

(for each $n \in \mathbb{N}$) which is the moduli for non-flat $\mathbf{B}^n \mathbb{G}$-connections.

(Details on this are at structures in a cohesive ∞-topos – Differential cohomology).

In particular our motivating example $\mathbf{H} =$ $Sh_\infty($SmoothMfd$) =$Smooth∞Grpd is a cohesive (∞,1)-topos. If in there we choose

$$\mathbb{G} \coloneqq U(1)$$

the circle group, or

$$\mathbb{G} \coloneqq \mathbb{C}^\times$$

the multiplicative group in the complex numbers, then

• $\mathbf{B}^{n-1} \mathbb{G}$ is the corresponding circle n-group,

• a $\mathbf{B}^n \mathbb{G}$-principal ∞-bundle (for $n= 1$ a circle bundle, for $n = 2$ a bundle gerbe, for $n = 3$ a bundle 2-gerbe, etc.)

Hence in this case a circle n-bundle with connection is

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

This has a curvature $(n+1)$-form

$$\omega : \Omega^{n+1}_{cl} \vdash \sum_{\omega = F_\nabla} X(\nabla) : Type \,.$$

With that regarded as an n-plectic form, $X_\nabla$ is the corresponding prequantum circle n-bundle.

For this we now conside aspects of higher geometric quantization.

Quantomorphism group

Let

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

be a prequantum circle n-bundle.

Definition

The cohesive quantomorphism n-group of this is the ∞-group

$$\vdash \prod_{\nabla : \mathbf{B}^n \mathbb{G}_{conn}} X(\nabla) \stackrel{\simeq}{\to} X(\nabla) : Type$$

given as the dependent product over the moduli ∞-stack of circle n-bundles with connection of the automorphism ∞-group of the map that modulates the prequantum circle n-bundle.

(This construction is a differential refinement of that of $\mathbf{B}^{n+1}\mathbb{G}$-action homomorphisms, see the comments in General notion in representation theory below for more background on this.)

Theorem

Let $\mathbf{H} =$ Smooth∞Grpd, $\mathbb{G} = U(1)$ and $X \in SmthMfd \hookrightarrow \mathbf{H}$.

Then

• for $n = 1$ def. categorical semantics interprets as the Lie group that Lie integrates the Poisson bracket of the symplectic form $F_{\nabla}$.

• for $n = 2$ def. categorical semantics interprets as the Lie 2-group that Lie integrates the Poisson bracket Lie 2-algebra (Rogers) of the 2-plectic form $\omega$.

Proof

This is spelled out in (Schreiber, section 4.4.17).

Remark

The expected statement is true for all $n$, but the fully general proof is not written up yet. The full statement should appear in (RogersSchreiber).

The relevance of the ordinary quantomorphism group is that it acts on the space of prequantum states by prequantum operators. In particular if $X$ itself has abelian group-structure, then those quantomorphisms covering the $X$-action? on itself form the Heisenberg group.

The following additions to theorem say that all these structures are similarly reproduced form fundamental constructions in cohesive homotopy type theory. However, to appreciate the following statements the reader will need a little bit more background on ∞-actions of ∞-groups than we have mentioned so far. The relevant notions are briefly discussed below in Background on higher group actions.

Prequantum states

Definition

Let

$$* :\mathbf{B}^n \mathbb{G} \vdash V(*) : Type$$

be an ∞-action of $\mathbf{B}^{n-1}\mathb{G}$ on some $\vdash V : Type$. Tthe space of pre-quantum states of the prequantum circle n-bundle $\nabla : \mathbf{B}^n \mathbb{G} \vdash X(\nabla) : Type$ with respect to $V$ is

$$\vdash \prod_{\mathbf{c} : \mathbf{B}^n \mathbb{G}} \left( \left( \sum_{{\mathbf{c} =} \atop {UnderlBdl(\nabla)}} X\left(\mathbf{c}\right) \right) \to V\left(\mathbf{c}\right) \right) : Type$$

Remark

By construction, this comes with a canonical ∞-action of the quantomorphism group of def. .

Theorem

With the assumptions as in theorem and for $V = \mathbb{C}$ equipped with the canonical $U(1)$-action, the interpretation of def. in $\mathbf{H} =$ Smooth∞Grpd reproduces the ordinary notion of space of states (in geometric quantization).

The canonical action of remark interprets as the standard action of prequantum operators.

Proof

This is spelled out in (Schreiber, section 4.4.17.1).

Background: Higher group-stacks and their actions

General abstract

The ∞-groups (see there) in $\mathbf{H}$ are equivalently the pointed connected objects, the equivalence given by the delooping operation

$$Gpr(\mathbf{H}) \underoverset{\mathbf{B}}{\simeq}{\to} \mathbf{H}^{*/}_{\geq 1} \,.$$

The ∞-actions of an ∞-group $G$ are equivalently the objects in the slice $\mathbf{H}_{/\mathbf{B}G}$:

$$\mathbf{Act}_{\mathbf{H}}(G) \simeq \mathbf{H}_{/\mathbf{B}G} \,.$$

Under this equivalence the object $V \in \mathbf{H}$ that is being acted on is the homotopy fiber

$$\array{ V &\to& V \sslash G \\ && \downarrow \\ && \mathbf{B}G } \,.$$

This homotopy fiber sequence is the universal $\rho$-associated $V$-fiber ∞-bundle.

Therefore the syntax of an ∞-action in homotopy type theory is

$$\rho \coloneqq \;\; \mathbf{c} : \mathbf{B}G \vdash V(\mathbf{c}) : Type \,.$$

In other words: the moduli ∞-stack $\mathbf{B}G$ of $G$-principal ∞-bundles is the context (in the sense of formal logic) in which every object is equipped with a $G$-∞-action.

General notions in representation theory

From this immeditatel derive various standard notions in representation theory.

The invariants of an $\infty$-action as above are given by the dependent product

$$Invariants = \;\; \vdash \prod_{\mathbf{c} : \mathbf{B}G} V(\mathbf{c}) : Type \,.$$

The conjugation action on maps between two representations $V$ and $W$ is

$$\mathbf{c} : \mathbf{B}G \vdash V(\mathbf{c}) \to W(\mathbf{c}) : Type \,.$$

In particular, the type of $G$-action homomorphisms is the type of invariants of the conjugation action

$$\vdash \prod_{\mathbf{c} : \mathbf{B}G} V(\mathbf{c}) \to W(\mathbf{c}) : Type \,.$$

Example

For $\vdash \Sigma : Type$, its automorphism ∞-group is

$$\vdash \Sigma \stackrel{\simeq}{\to} \Sigma : Type$$

The canonical ∞-action of $\mathbf{Aut}(\Sigma)$ on $\Sigma$ is

$$\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma : Type$$

which interprets to

$$\array{ \Sigma &\to& \Sigma\sslash \mathbf{Aut}(\Sigma) &\to& \widehat{Type} \\ && \downarrow && \downarrow \\ && \mathbf{B}\mathbf{Aut}(\Sigma) &\hookrightarrow& Type }$$

General particulars: Groups of bisections and Lie algebroids

We mention some general classes of examples of the above notions of relevance in differential geometry and gauge theory.

Example

An atlas is

$$x : X \vdash U(x) : Type$$

such that

$$\vdash isAtlas : \prod_{x : X} isInhabited(U(x))$$

The higher group of bisections of a ∞-groupoid $X$ with atlas $U$ is

$$\vdash \prod_{x : X} U(x) \stackrel{\simeq}{\to} U(x) : Type$$

Hence the ∞-Lie algebroid of $(X,U)$ in its incarnation as a Lie-Rinehart pairt is the ∞-Lie algebra of this ∞-group together with its induced ∞-action on $U$.

Concrete particulars: Generally covariant configuration space of gravity

Example

In $\mathbf{H} =$ Smooth∞Grpd.

$$\mathbf{c}_1 : \mathbf{B} U(1) \vdash X(\mathbf{c}_1) : Type$$

is circle bundle on $X$.

The defining representation of $U(1)$

$$* : \mathbf{B} U(1) \vdash \mathbb{C} : Type$$

then

$$\vdash \prod_{\mathbf{c}_1 : \mathbf{B} U(1)} X(\mathbf{c}_1) \to \mathbb{C} : Type$$

is space of smooth sections of the associated complex line bundle

Example

$$* : \mathbf{B}^2 U(1) \vdash \mathbf{B}U(n) : Type$$

is canonical action of $\mathbf{B}U(1)$, then for

$$* : \mathbf{B}^2 U(1) \vdash (X, \mathbf{DD}_1) : Type$$

a B-field instanton configuration with Dixmier-Douady class $\mathb{DD}_1$ on $X$, then

$$\vdash \prod_{\mathbf{DD}_1 : \mathbf{B}^2 U(1)} X(\mathbf{DD}_1) \to \mathbf{B}U(n) : Type$$

is moduli stack of $\mathbf{DD}$-twisted $U(n)$-twisted bundles

Example

(generally covariant field of gravity)

Let

1. $\mathbf{H} \coloneqq$ Smooth∞Grpd $= Sh_\infty(SmthMfd)$

2. $\mathbf{orth} : \mathbf{B} O(n) \to \mathbf{B} GL(n)$ the delooping of the inclusion of the orthogonal group into the general linear group (inclusion of the maximal compact subgroup)

3. $\vdash \Sigma : Type$ a smooth manifold

Then

$$\vdash \prod_{* : \mathbf{B} GL(n)} T \Sigma\to \mathbf{orth} : Type$$

is the moduli stack of vielbein fields on $\Sigma$, hence the moduli of Riemannian metric structures on $\Sigma$. Therefore the ∞-action quotient by the diffeomorphism group

$$\vdash \sum_{T \Sigma : \mathbf{B}\mathbf{Aut}(T \Sigma)} \prod_{* : \mathbf{B} GL(n) } T \Sigma \to \mathbf{orth} : Type$$

is the generally covariant moduli of vielbein fields, hence the Lie integrated BRST complex of Einstein-gravity: $\pi_1$ is the integrated diffeomorphisms ghosts.

References

The Poisson bracket Lie n-algebra of an n-plectic manifold was introduced in

• Chris Rogers, Higher symplectic geometry PhD thesis (2011) (arXiv:1106.4068)

The computations going into the proof of theorem are spelled out in section 4.4.17 of

• Urs Schreiber, differential cohomology in a cohesive topos

A dedicated discussion of the result discussed here should appear as

• Chris Rogers, Urs Schreiber, Quantomorphism $n$-groups

Dedicated discussion of the syntax of cohesive homotopy type theory in the context of higher geometric quantization as used in the formulation of the above theorem is in

• Urs Schreiber, Mike Shulman, Quantum gauge field theory in Cohesive homotopy type theory