Schreiber Erlangen2012


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

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 nn-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 XX with symplectic form ωΩ cl 2(X)\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 Ω cl 2():SmthMfd opSet\Omega^2_{cl}(-) : SmthMfd^{op} \to Set on the site SmthMfd of smooth manifolds, as does of course XX itself, via C (,X):SmthMfd opSetC^\infty(-,X) : SmthMfd^{op} \to Set.

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

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

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

:XBU(1) conn \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 ():BU(1) connΩ cl 2()F_{(-)} : \mathbf{B}U(1)_{conn} \to \Omega^2_{cl}(-), sending a connection to its curvature 2-form ω=F \omega = F_{\nabla}, expressed the the commutativity of the diagram

BU(1) conn F () X ω Ω cl 2(). \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,ω)(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 nn-dimensional quantum field theory naturally carries a closed differential form of degree (n+1)(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 nn-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 nn-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:

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 nn-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_ H\mathbf{H}. That means:

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

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

For instance

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 H\mathbf{H} there is an object TypeHType \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(H /X) smallH(X,Type) name : Core(\mathbf{H}_{/X})^{small} \stackrel{\simeq}{\to} \mathbf{H}(X,Type)

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

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

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

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


Since this way the \infty-topos H\mathbf{H} “reflects on itself” via TypeType, it is useful to consistently speak of all objects in a slice H /X\mathbf{H}_{/X} entirely in terms of their “names” this way (the “internal language” of H\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

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

we will draw symbols like this:

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

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

Similarly, instead of the symbols

Xt XE X \stackrel{t}{\to}_X E

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

x:Xt(x):E(x) 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

∞-topos theoryXEType\;\;\;\;X \stackrel{\vdash \;\;\;\;E}{\to} \;\;\TypeXt XE\;\;\;\;X \stackrel{\vdash \;\;\;t}{\to} {}_X \;\;E
homotopy type theoryx:XE(x):Typex : X \vdash E(x) : Typex:Xt(x):E(x)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 XHX \in \mathbf{H}, hence X:Type\vdash X : Type, the slice ∞-topos H /X\mathbf{H}_{/X} is a cartesian closed ∞-category: for each (EeX)H /X(E \stackrel{e}{\to}X ) \in \mathbf{H}_{/X}, hence for each x:XE(x):Typex : X \vdash E(x) : Type, there is a pair of adjoint ∞-functors

(e×()[e,]):H /XH /X, (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][e,f] here the relative mapping stack.)

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

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

x:XE(x)F(x):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)F(x)E(x) \to F(x) homotopy fiber-wise over generalized elements xXx \in X.

Often one is interested in the subobject [e,f] [e,f][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:XE(x)F(X):Type. x : X \vdash E(x) \stackrel{\simeq}{\to} F(X) : Type \,.

In particular, this means that the expression

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

gives an ∞-group or group-∞-stack: the automorphism ∞-group of EE over XX. 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 (XfY)(X \stackrel{f}{\to} Y) any morphism in the ∞-topos H\mathbf{H}, there is an adjoint triple of ∞-functors called and denoted as follows:

(dependent sum \dashv base change \dashv dependent product)= ( ff * f):H /X ff * fH /Y (\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:XE(x):Type x : X \vdash E(x) : Type

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

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

This is the object of sections of EXE \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).


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 XXX \in \mathbf{X} there is an object X\flat X

X:TypeX:Type X : Type \vdash \flat X : Type

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

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


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

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

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

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

c:B𝔾 c=UnderlBdl()X():Type. \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 mathbG\mathb{G} is an abelian (E-∞) ∞-group and using a given notion of manifolds, there is canonically a refinement of B𝔾\flat \mathbf{B}\mathbb{G} to an object

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

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

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

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

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

the circle group, or

𝔾 × \mathbb{G} \coloneqq \mathbb{C}^\times

the multiplicative group in the complex numbers, then

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

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

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

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

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

For this we now conside aspects of higher geometric quantization.

Quantomorphism group


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

be a prequantum circle n-bundle.


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

:B n𝔾 connX()X():Type \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 B n+1𝔾\mathbf{B}^{n+1}\mathbb{G}-action homomorphisms, see the comments in General notion in representation theory below for more background on this.)


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



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


The expected statement is true for all nn, 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 XX itself has abelian group-structure, then those quantomorphisms covering the XX-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



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

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

c:B n𝔾(( c=UnderlBdl()X(c))V(c)):Type \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

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


With the assumptions as in theorem and for V=V = \mathbb{C} equipped with the canonical U(1)U(1)-action, the interpretation of def. in H=\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.


This is spelled out in (Schreiber, section

Background: Higher group-stacks and their actions

General abstract

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

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

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

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

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

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

This homotopy fiber sequence is the universal ρ\rho-associated VV-fiber ∞-bundle.

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

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

In other words: the moduli ∞-stack BG\mathbf{B}G of GG-principal ∞-bundles is the context (in the sense of formal logic) in which every object is equipped with a GG-∞-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= c:BGV(c):Type. Invariants = \;\; \vdash \prod_{\mathbf{c} : \mathbf{B}G} V(\mathbf{c}) : Type \,.

The conjugation action on maps between two representations VV and WW is

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

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

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

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

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

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

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

which interprets to

Σ ΣAut(Σ) Type^ BAut(Σ) Type \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.


An atlas is

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

such that

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

The higher group of bisections of a ∞-groupoid XX with atlas UU is

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

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

Concrete particulars: Generally covariant configuration space of gravity


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

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

is circle bundle on XX.

The defining representation of U(1)U(1)

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


c 1:BU(1)X(c 1):Type \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

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

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

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

a B-field instanton configuration with Dixmier-Douady class mathbDD 1\mathb{DD}_1 on XX, then

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

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


(generally covariant field of gravity)


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

  2. orth:BO(n)BGL(n)\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. Σ:Type\vdash \Sigma : Type a smooth manifold


*:BGL(n)TΣorth:Type \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

TΣ:BAut(TΣ) *:BGL(n)TΣorth:Type \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: π 1\pi_1 is the integrated diffeomorphisms ghosts.


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

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

A dedicated discussion of the result discussed here should appear as

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

Last revised on September 16, 2012 at 15:13:14. See the history of this page for a list of all contributions to it.