nLab
general covariance

Idea

In physics, the term general covariance is meant to indicate the property of a physical system or model (in theoretical physics) whose configurations, action functional and equations of motion are all equivariant under the action of the diffeomorphism group on the smooth manifold underlying the spacetime or the worldvolume of the system. Here “covariance” is as in “covariant tensor” another term for behaviour under diffeomorphisms.

The term general relativity for Einstein-gravity originates in at least closely related ideas (see History and original formulation below), and Einstein-gravity is the archtypical example of a generally covariant physical system:

here, the configuration space of physical fields over a smooth manifold $\Sigma$ is not quite the space of Riemannian metrics on $\Sigma$ itself, but is the quotient $[\Sigma ,\mathrm{Fields}]/\mathrm{Diff}(\Sigma )$ of this space by the action of the diffeomorphism group $\mathrm{Diff}(\Sigma )$: two Riemannian metrics $g_1$ and $g_2$ on $\Sigma$ represent the same field of gravity on $\Sigma$ if there is a diffeomorphism $f:\Sigma \stackrel{\simeq }{\to }\Sigma$ such that $g_2=f^{*}{g}_1$.

Or rather, such a diffeomorphism is a gauge transformation between the two field configurations. The configuration space is not the naive quotient of fields by diffeomorphisms as above, but is the homotopy quotient, or action groupoid, denoted $[\Sigma ,\mathrm{Fields}]⫽\mathrm{Diff}(\Sigma )$. In the physics literature this action groupoid is most familiar in its infinitesimal approximation, the corresponding Lie algebroid, whose formal dual is a BRST complex whose degree-1 elements are accordingly called the diffeomorphism ghosts (see there).

As with all gauge transformations, they relate physical configurations which may be nominally different, but equivalent. Therefore general covariance is an instance of the general principle of equivalence in mathematics which says that sensible statements about objects must respect the isomorphisms and more general equivalences between these objects.

A physical system which is not generally covariant in this sense is hence one where the smooth manifold $\Sigma$ as above, underlying spacetime/worldvolume is not regarded as modelling an absolute physical system (such as the observable universe in gravity), but a subsystem that is equipped with ambient structure that breaks the diffeomorphism symmetry. Notably systems like electromagnetism or Yang-Mills theory have traditionally been written in a non-generally covariant form describing gauge fields on a fixed gravitational background, as for instance the space inhabited by a particle accelerator. This ambient structure on the spacetime $\Sigma$ breaks its general diffeomorphism invariance and hence the effective resulting theory on this background is not generally covariant (a special case of the general phenomenon of spontaneous symmetry breaking).

On the other hand, such a model consisting of background (e.g. the particle accelerator) and quantum fields propagating in it is ultimately to be understood as an approximation to a more encompassing model in which also the background is dynamical, and which is again generally covariant. Specific for electromagnetism and Yang-Mills theory this refined generally covariant model is known as Einstein-Maxwell theory or more generally Einstein-Yang-Mills theory.

The idea of general covariance has a long and convoluted history and the literature witnesses plenty of disagreement about how to interpret and formalize it in technical detail (Norton). Already early arguments by Einstein himself (e.g. the “hole paradox” (Einstein-Grossmann)) show that the discussion has suffered from the beginning from lack of the basic category theoretic concept of isomorphism in the category Diff of smooth manifolds. Below in Formalization in homotopy type theory we indicate a formalization of general covariance that is general, fundamental, and accurately reflects the role of the term in theoretical physics.

History and original formulation

The question of general covariance of physical theories in space and time can be traced back to the famous debate between Gottfried Wilhelm Leibniz and Samuel Clarke (the latter assisted by Sir Isaac Newton) on the ontological status of space in the years 1715–1716 (Alexander), the central question being if space exists as a substance or as an absolute being and absolute motion is present (Clarke) or if it is constituted only in relation to co-existent things allowing for relativism in motions only (Leibniz). This kind of problems also played an important role when the general theory of relativity was being developed in the years around 1910. While Albert Einstein first characterized generally covariant field equations as inadmissible since they did not determine the metric field uniquely as shown in the hole argument ( Lochbetrachtung ) in the appendix of (Einstein-Grossmann), he later accepted (Einstein 1916) that all physical laws had to be expressed by equations that are valid in all coordinate systems, i. e., which are covariant (generally covariant) under arbitrary substitutions.

Die allgemeinen Naturgesetze sind durch Gleichungen auszudrücken, die für alle Koordinatensysteme gelten, d. h. die beliebigen Substitutionen gegenüber kovariant (allgemein kovariant) sind. (Einstein 1916 p. 776)

The hole argument was dismissed by the reasoning that it is not the spacetime metric that has to be fixed uniquely by the field equations, but only the physical phenomena that occur in spacetime need to be given a unique expression with reference to any description of spacetime. All physical statements are given in terms of spacetime coincidences; measurements result in statements on meetings of material points of the measuring rods with other material points or in coincidences between watch hands and points on the clockface. The introduction of a reference system merely serves the easy description of the totality of all these coincidences (point-coincidence argument) (Einstein 1916 p. 776f).

from (Brunetti-Pormann-Ruzzi)

Modern formulation in differential geometry

We discuss the modern formulation of general covariance in differential geometry.

In gravity

Let $\Sigma \in$ SmoothMfd be a smooth manifold. Write $\mathrm{Riem}(\Sigma )$ for the space of (pseudo-)Riemannian metrics on $\Sigma$. For $f:\Sigma \to \Sigma$ a diffeomorphism, there is a function $f^{*}:\mathrm{Riem}(\Sigma )\to \mathrm{Riem}(\Sigma )$ which sends a Riemannian metric to its pullback:

$$(f^{*}g)(v,w)≔g(f_{*}v,f_{*}w),$$(f^*g)(v,w) \coloneqq g(f_* v, f_* w) \,,

where $f_{*}:T\Sigma \to T\Sigma$ is the canonical map induced on the tangent bundle (see at derivative).

Say that two metrics $g_1,g_2$ are gauge equivalent if there is a diffeomorphism $f$ such that $g_2=f^{*}{g}_1$. This is an equivalence relation. Write $\mathrm{Riem}(\Sigma )/\mathrm{Diff}(\Sigma )$ for the corresponding set of equivalence classes.

The statement of general covariance is that the distinct configurations of the gravitational field form the set $\mathrm{Riem}(\Sigma )/\mathrm{Diff}(\Sigma )$. In particular, if $\Sigma$ is compact, then the Einstein-Hilbert action functional which a-prior is defined on $\mathrm{Riem}(\Sigma )$ descends to $\mathrm{Riem}(\Sigma )/\mathrm{Diff}(\Sigma )$

$$S_{\mathrm{EH}}:\mathrm{Riem}(\Sigma )/\mathrm{Diff}(\Sigma )\to ℝ.$$S_{EH} : Riem(\Sigma)/Diff(\Sigma) \to \mathbb{R} \,.

While this captures the idea of general covariance accurately, for further development of the theory of gravity, however, the set $\mathrm{Riem}(\Sigma )/\mathrm{Diff}(\Sigma )$ needs to be refined. It is really equipped with the structure of a smooth space $\mathrm{Riem}(\Sigma )/\mathrm{Diff}(\Sigma )$ (in order to perform variational calculus and hence derive the equations of motion of the theory), and second it is to be refined to a smooth groupoid $\mathrm{Riem}(\Sigma )⫽\mathrm{Diff}(\Sigma )$.

Finally, for setups that admit to introduce fermions/spinors into the model one needs to refine Riemannian metrics to vielbein fields/orthogonal structures. The fully refined generally covariance smooth configuration groupoid is then $[\Sigma ,\mathrm{orth}]⫽\mathrm{Diff}(\Sigma )$, discussed in more detail below.

Relation to the “principle of equivalence” in gravity

The principle of equivalence in general relativity is formally the statement that around every point in a (pseudo-)Riemannian manifold one can find a coordinate system such that the Levi-Civita connection vanishes (“Riemann normal coordinates”), which means that to first infinitesimal order around that point particle dynamics subject to the force of gravity is equivalent to dynamics in Minkowski spacetime with vanishing field of grvity.

By the above this is a special case of the principle of general covariance: for every field configuration $g$ and every given point there is a gauge equivalent field configuration $f^{*}g$ such that the “force of gravity” (the Levi-Civita connection) vanishes at that point.

It is via this relation that the physical “principle of equivalence” relates to the mathematical principle of equivalence: this says that formulations need to respect the given notion of equivalence/gauge transformation, and so

principle of equivalence in mathematics $\Rightarrow$ principle of general covariance $\Rightarrow$ principle of equivalence in physics .

In other topological field theories

Formalization in homotopy type theory

We discuss here that general covariance in field theory has a natural formalization in homotopy type theory, hence internal to any (∞,1)-topos. For exposition, background and further details on the discussion of classical/quantum field theory in this fashion see (Schreiber, ESI lectures) and (Schreiber-Shulman).

Introduction

A basic idea of traditional dependent type theory is of course that types $A$ may appear in context of other types $\Gamma$. The traditional interpretation of such a dependent type

$$x:\Gamma ⊢A(x):\mathrm{Type}$$x : \Gamma \vdash A(x) : Type

is that of a $\Gamma$-parameterized family or bundle of types, whose fiber over $x\in \Gamma$ is $A(x)$.

But in homotopy type theory, types are homotopy types and, hence so are the contexts. A type in context is now in general something more refined than just a family of types. It is really a family of types equipped with equivariance structure with respect to the homotopy groups of the context type.

Hence in homotopy theory types in context generically satisfy an equivariance-principle.

Specifically, if the context type is connected and pointed, then it is equivalent to the delooping $\Gamma \simeq BG$ of an ∞-group $G$. One finds – this is discussed at ∞-action – that the context defined by the type $BG$ is that of $G$-equivariance: every type in the context is a type in the original context, but now equipped with a $G$-∞-action. In a precise sense, the homotopy type theory of $G$-$\mathrm{\infty }$-actions is equivalent to plain homotopy type theory in context $BG$.

In the following we discuss this for the case that $G$ is an automorphism ∞-group of a type $\Sigma$ which is regarded as representing spacetime or a worldvolume. We show that in this context the rules of homotopy type theory automatically induce the principle of general covariance and naturally produce configurations spaces of generally covariant field theories: for $\mathrm{Fields}$ a moduli object for the given fields, so that a field configuration is a function $\varphi :\Sigma \to \mathrm{Fields}$, the configuration space of covariant fields is the function type $(\Sigma \to \mathrm{Fields})$ but formed in the “general covariance context” $B\mathrm{Aut}(\Sigma )$. When interpreted in smooth models, $\mathrm{Conf}$ is the smooth groupoid of field configurations and diffeomorphism gauge transformations acting on them, the Lie integrations of the BRST complex whose degree-1 elements are the diffeomorphism ghosts.

More precisely, we show the following.

Definition

Consider in homotopy type theory two types $⊢\Sigma ,\mathrm{Fields}:\mathrm{Type}$, to be called spacetime and field moduli. Let

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

be the image of the name of $\Sigma$, with essentially unique term

$$⊢\Sigma :B\mathrm{Aut}(\Sigma ).$$\vdash \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \,.

Perform the canonical context extension of $\Sigma$ and trivial context extension of $\mathrm{Fields}$ to get types in context

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

and

$$\Sigma :B\mathrm{Aut}(\Sigma )⊢\mathrm{Fields}:\mathrm{Type}.$$\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \mathbf{Fields} : Type \,.

Form then the type of field moduli ”$\mathrm{Conf}≔(\Sigma \to \mathrm{Fields})$” in this context:

$$\mathrm{Conf}≔\Sigma :B\mathrm{Aut}(\Sigma )⊢(\Sigma \to \mathrm{Fields}):\mathrm{Type}.$$\mathbf{Conf} \coloneqq \;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Fields}) : Type \,.

Proposition

The categorical semantics of $\mathrm{Conf}$ in the model Smooth∞Grpd of the homotopy type theory and for $\Sigma \in$ SmoothMfd $\hookrightarrow \mathrm{Smooth}\mathrm{\infty }\mathrm{Grpd}$ is given by the diffeological groupoid

$$\mathrm{Conf}=[\Sigma ,\mathrm{Fields}]⫽\mathrm{Diff}(\Sigma )$$\mathbf{Conf} = [\Sigma, \mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma)

whose objects are field configurations on $\Sigma$ and whose morphisms are diffeomorphism gauge transformations between them. In particular the corresponding Lie algebroid is dual to the BRST complex of fields with diffeomorphism ghosts in degree 1.

The ambient theory

Write $H$ for the ambient homotopy type theory, or rather an interpretation given by an (∞,1)-topos. For standard applications in physics we have $H=$ Smooth∞Grpd or SmoothSuper∞Grpd or similar, but none of the following general discussion depends on a concrete choice for $H$.

Pick once and for all an object

$$\Sigma \in H$$\Sigma \in \mathbf{H}

supposed to represent the space underlying spacetime or the worldvolume of a model (in theoretical physics),

The diffeomorphism group

Write

$$\mathrm{Aut}(\Sigma )\in \mathrm{Grp}(H)$$\mathbf{Aut}(\Sigma) \in Grp(\mathbf{H})

for the automorphism ∞-group of $\Sigma$. As discussed there, this is the loop space object of the homotopy image-factorization of

$$*\stackrel{⊢\Sigma }{\to }\mathrm{Type},$$* \stackrel{\vdash \Sigma}{\to} Type \,,

hence the factorization by an effective epimorphism followed by a monomorphism:

$$*\stackrel{}{\to }B\mathrm{Aut}(\Sigma )\stackrel{}{\hookrightarrow }\mathrm{Type}.$$* \stackrel{}{\to} \mathbf{B}\mathbf{Aut}(\Sigma) \stackrel{}{\hookrightarrow} Type \,.

In the standard interpretation of the homotopy type theory in $H=$ Smooth∞Grpd $\Sigma$ could be an ordinary smooth manifold or orbifold, in particular, and then $\mathrm{Aut}(\Sigma )=Diff(\Sigma )$ is the diffeomorphism group of $\Sigma$, regarded as a diffeological group object. In view of this archetypical example we will in the following often say diffeomorphism for short instead of auto-equivalence in $H$ and similarly refer to $\mathrm{Aut}(\Sigma )$ loosely as the diffeomorphism group of $\Sigma$. But even in the specifical model $H=$ Smooth∞Grpd/SmoothSuper∞Grpd, $\Sigma$ can be much more general than a smooth manifold or supermanifold or orbifold.

The context of general covariance

Write then $B\mathrm{Aut}(\Sigma )\in H$ for the delooping of the diffeomorphism group. The essentially unique term of this type is to be thought of as being $\Sigma$ itself, and so we write it as

$$⊢\Sigma :B\mathrm{Aut}(\Sigma ).$$\vdash \Sigma : \mathbf{B} \mathbf{Aut}(\Sigma) \,.

By the discussion at ∞-action, a type in context of $B\mathrm{Aut}(\Sigma )$

$$\Sigma :B\mathrm{Aut}(\Sigma )⊢V(\Sigma )$$\Sigma : \mathbf{B} \mathbf{Aut}(\Sigma) \vdash V(\Sigma)

is a type $⊢V:\mathrm{Type}$ in the absolute context equipped with an $\mathrm{Aut}(\Sigma )$-∞-action $\rho :V\times \mathrm{Aut}(\Sigma )\to V$ on it. The dependent sum

$$⊢\sum _{\Sigma :B\mathrm{Aut}(\Sigma )}V(\Sigma ):\mathrm{Type},$$\vdash \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma) : Type \,,

which we also write

$$V⫽\mathrm{Aut}(\Sigma )≔\sum _{\Sigma :B\mathrm{Aut}(\Sigma )}V(\Sigma ),$$V \sslash \mathbf{Aut}(\Sigma) \coloneqq \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma) \,,

is the total space of the universal associated $V$-fiber ∞-bundle:

$$\begin{array}{ccc}V& \to & \sum _{B\mathrm{Aut}(\Sigma )}V(\Sigma )\\ & & {\downarrow }^{\overline{\rho }}\\ & & B\mathrm{Aut}(\Sigma )\end{array}.$$\array{ V &\to& \sum_{\mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma) \\ && \downarrow^{\overline{\rho}} \\ && \mathbf{B}\mathbf{Aut}(\Sigma) } \,.

Hence the interpretation of the context $\Sigma :B\mathrm{Aut}(\Sigma )$ is the slice (∞,1)-topos $H_{/B\mathrm{Aut}(\Sigma )}$ and equivalently is the (∞,1)-topos of objects in $H$ equipped with $G$-∞-actions and of $G$-equivariant morphisms between them:

$$H_{/B\mathrm{Aut}(\Sigma )}\simeq {\mathrm{Act}}_H(\mathrm{Aut}(\Sigma )).$$\mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)} \simeq Act_{\mathbf{H}}(\mathbf{Aut}(\Sigma)) \,.

Hence a type in context $\Sigma :B\mathrm{Aut}(\Sigma )$ is a “generally covariant type” with respect to $\Sigma$ in the sense that it transforms covariantly by equivalences under diffeomorphisms of $\Sigma$. In summary then

Fact. $\Sigma :B\mathrm{Aut}(\Sigma )$ is the context of general covariance with respect to $\Sigma$.

In the precise formal sense.

In particular, $\Sigma$ itself is canonically equipped with the defining action of $\mathrm{Aut}(\Sigma )$ on it, which syntactically we may write

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

and which semantically is exhibited by the universal associated $\Sigma$-fiber ∞-bundle

$$\begin{array}{ccc}\Sigma & \to & \sum _{\Sigma :B\mathrm{Aut}(\Sigma )}\Sigma \\ & & {\downarrow }^{\overline{{\rho }_{\Sigma }}}\\ & & B\mathrm{Aut}(\Sigma )\end{array},$$\array{ \Sigma &\to& \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} \Sigma \\ && \downarrow^{\overline{\rho_{\Sigma}}} \\ && \mathbf{B} \mathbf{Aut}(\Sigma) } \,,

given by the pullback of the universe $\widetilde{\mathrm{Type}}\to \mathrm{Type}$ along the defining inclusion $B\mathrm{Aut}\hookrightarrow \mathrm{Type}$.

Here the total space

$$\Sigma ⫽\mathrm{Aut}(\Sigma )≔\sum _{\Sigma :B\mathrm{Aut}(\Sigma )}\Sigma$$\Sigma \sslash \mathbf{Aut}(\Sigma) \coloneqq \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) } \Sigma

is the homotopy quotient or action groupoid of $\Sigma$ by $\mathrm{Aut}(\Sigma )$. This is the type characterized by the fact that a function $f:U\to \Sigma ⫽\mathrm{Aut}(\Sigma )$ is a function to $\Sigma$ which is regarded as (gauge) equivalent to another function to $\Sigma$ if both differ by postcomposition with a diffeomorphism of $\Sigma$.

Generally covariant field configuration spaces

Let now

$$\mathrm{Fields}\in H$$\mathbf{Fields} \in \mathbf{H}

be an object that represent the moduli ∞-stack of field configuration on $\Sigma$ for some model (in theoretical physics) to be described. For instance for $G\in \mathrm{Grp}(H)$ an ∞-group and $H$ a cohesive homotopy type theory, we could have $\mathrm{Fields}=B{G}_{\mathrm{conn}}$ the moduli for a choice of $G$-principel ∞-connection, being the moduli for $G$-(higher)gauge fields. For general $\mathrm{Fields}=X\in H$ we may always regard $X$ as the target space of a sigma-model.

Then the internal hom

$$\mathrm{Fields}(\Sigma )≔[\Sigma ,\mathrm{Fields}]\in H$$\mathbf{Fields}(\Sigma) \coloneqq [\Sigma, \mathbf{Fields}] \in \mathbf{H}

hence the function type

$$⊢\Sigma \to \mathrm{Fields}:\mathrm{Type}$$\vdash \Sigma \to \mathbf{Fields} : Type

is the naive configuration space of the model. This is not generally covariant, precisely so by the above definition: it is not in the generally covariant context $H_{/B\mathrm{Aut}(\Sigma )}$.

But by the inverse image of the $B\mathrm{Aut}(\Sigma )$-dependent product étale geometric morphism

$$H_{/BG}\stackrel{\stackrel{\sum _{B\mathrm{Aut}(\Sigma )}}{\to }}{\overleftarrow{\underset{\prod _{B\mathrm{Aut}(\Sigma )}}{\to }}}H$$\mathbf{H}_{/\mathbf{B}G} \stackrel{\overset{\sum_{\mathbf{B}\mathbf{Aut}(\Sigma)}}{\to}}{ \stackrel{\overset{}{\leftarrow}}{\underset{\prod_{\mathbf{B}\mathbf{Aut}(\Sigma)}}{\to}}} \mathbf{H}

which is context enlargement by $B\mathrm{Aut}(\Sigma )$, the the moduli type $\mathrm{Fields}$ is freely moved to the general covariant context, where it is regaded as equipped with the trivial ∞-action. Accordingly we will write just $\mathrm{Fields}\in H_{/B\mathrm{Aut}(\Sigma )}$ with that trivial action understood, which is justified by the precise syntactic expression for it:

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

We may then form the configuration space of fields in the generally covariant context . As before, a field $\varphi$ should be a function on $\Sigma$ with values in the moduli type of field configurations, but now we interpret this statement in the generally covariant context. Syntactically this simply means that a field is now a term in $B\mathrm{Aut}(\Sigma )$-context

$$\Sigma :B\mathrm{Aut}(\Sigma )⊢\varphi :\Sigma \to \mathrm{Fields}$$\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \phi : \Sigma \to \mathbf{Fields}

and that accordingly the configuration space of fields is

$$\Sigma :B\mathrm{Aut}(\Sigma )⊢\Sigma \to \mathrm{Fields}:\mathrm{Type}.$$\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma \to \mathbf{Fields} : Type \,.

The semantics of this is the internal hom in the slice (∞,1)-topos, the Internal hom of ∞-actions

$$\mathrm{Conf}≔[\Sigma ⫽\mathrm{Aut}(\Sigma ),\mathrm{Fields}]\in H_{/\mathrm{Aut}(\Sigma )},$$\mathbf{Conf} \coloneqq [\Sigma \sslash \mathbf{Aut}(\Sigma), \mathbf{Fields}] \in \mathbf{H}_{/\mathbf{Aut}(\Sigma)} \,,

The central observation now is that discussed at ∞-action – Examples – General covariance:

$$\mathrm{Conf}\simeq [\Sigma ,\mathrm{Fields}]⫽\mathrm{Aut}(\Sigma )$$\mathbf{Conf} \simeq [\Sigma,\mathbf{Fields}] \sslash \mathbf{Aut}(\Sigma)

is the homotopy quotient of the naive fields $\in \mathrm{Fields}(\Sigma )$ by the action of the diffeomorphism group, exhibiting a gauge equivalence between any two field configurations that differ after pullback along a diffeomorphism.

This is precisely as it should be for configuration space of generally covariant theories. We have found:

Fact. In terms of homotopy type theory, configuration spaces of a generally coveriant theory over $\Sigma$ are precisely the ordinary configuration spaces of fields, but formed in the context $B\mathrm{Aut}(\Sigma )$:

$$\mathrm{Conf}{=}_{\mathrm{def}}\Sigma :B\mathrm{Aut}(\Sigma )⊢(\Sigma \to \mathrm{Field}):\mathrm{Type}.$$\mathbf{Conf} =_{def} \;\;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Field}) : Type \,.

Generally covariant field of gravity

We now spell out the example of ordinary Einstein-gravity in this language. Plenty of further examples work analogously.

For pure gravity, we choose $H=$ Smooth∞Grpd or $=$SynthDiff∞Grpd.

If we denote by $D^n\in$ SynthDiff∞Grpd the first order infinitesimal neighbourhood of the origin in the Cartesian space ${ℝ}^n$, then

$$\mathrm{GL}(n)=\mathrm{Aut}(D^n)$$GL(n) = \mathbf{Aut}(D^n)

is the automorphism ∞-group of $D^n$. Accordingly we write the unique term of the delooping $B\mathrm{GL}(n)$ as

$$⊢D^n:B\mathrm{GL}(n).$$\vdash D^n : \mathbf{B}GL(n) \,.

The fields of Einstein gravity are orthogonal structures (Riemannian metrics) on a smooth manifold $\Sigma \in$ SmoothMfd $\hookrightarrow H$ of dimension $n$. As discussed at orthogonal structure and vielbein, we are to regard $\Sigma$ in the context of the delooping of the general linear group $\mathrm{GL}(n)\in \mathrm{Grp}(H)$ via its tangent bundle $T\Sigma \to \Sigma$, by which we always mean here the $\mathrm{GL}(n)$-principal bundle to which the tangent bundle is associated.

By the discussion at principal ∞-bundle this is modulated by a morphism

$$(\Sigma \stackrel{⊢T\Sigma }{\to }B\mathrm{GL}(n))\in H_{/B\mathrm{GL}(n)}$$(\Sigma \stackrel{\vdash T \Sigma}{\to} \mathbf{B} GL(n)) \in \mathbf{H}_{/\mathbf{B} GL(n)}

to the delooping $B\mathrm{GL}(n)$ of $\mathrm{GL}(n)$ (the moduli stack of $\mathrm{GL}(n)$-principal bundles) in that we have a fiber sequence

$$\begin{array}{ccc}T\Sigma & \to & \Sigma \\ & & {\downarrow }^{⊢T\Sigma }\\ & & B\mathrm{GL}(n)\end{array}$$\array{ T \Sigma &\to& \Sigma \\ && \downarrow^{\mathrlap{\vdash T \Sigma}} \\ && \mathbf{B}GL(n) }

in $H$. (A detailed exposition of this and the following, with further pointers, is in (Schreiber, ESI lectures).)

Therefore the syntax of the tangent bundle as a dependent type is

$$D^n:B\mathrm{GL}(n)⊢T\Sigma (D^n):\mathrm{Type}$$D^n : \mathbf{B}GL(n) \vdash T \Sigma(D^n) : Type

and since $D^n$ is essentially unique we will notationally suppress it in the succedent on the right and just write

$$D^n:B\mathrm{GL}(n)⊢T\Sigma :\mathrm{Type}.$$D^n : \mathbf{B}GL(n) \vdash T \Sigma : Type \,.

Let then

$$(BO(n)\stackrel{\mathrm{orth}}{\to }B\mathrm{GL}(n))\in H_{/B\mathrm{GL}(n)}$$(\mathbf{B} O(n) \stackrel{\mathbf{orth}}{\to} \mathbf{B} GL(n)) \in \mathbf{H}_{/\mathbf{B}GL(n)}

be the delooping of the inclusion $O(n)\to \mathrm{GL}(n)$ of the maximal compact subgroup of $\mathrm{GL}(n)$, the orthogonal group $O(n)$, regarded as an object in the slice-(∞,1)-topos over $B\mathrm{GL}(n)$. Since this sits in the homotopy fiber sequence

$$\begin{array}{ccc}\mathrm{GL}(n)/O(n)& \to & BO(n)\\ & & {\downarrow }^{\mathrm{orth}}\\ & & B\mathrm{GL}(n)\end{array}$$\array{ GL(n)/O(n) &\to& \mathbf{B}O(n) \\ && \downarrow^{\mathrlap{orth}} \\ && \mathbf{B}GL(n) }

with the coset smooth space $\mathrm{GL}(n)/O(n)$, the syntax of this object is the dependent type

$$D^n:B\mathrm{GL}(n)⊢\mathrm{GL}(n)/O(n):\mathrm{Type}.$$D^n : \mathbf{B}GL(n) \vdash GL(n)/O(n) : Type \,.

In view of the equivalence of (∞,1)-categories

$$H_{/B\mathrm{GL}(n)}\simeq {\mathrm{Act}}_H(\mathrm{GL}(n))$$\mathbf{H}_{/\mathbf{B}GL(n)} \simeq Act_{\mathbf{H}}(GL(n))

this expresses the canonical $\mathrm{GL}(n)$-action on the coset $\mathrm{GL}(n)/O(n)$ (by mutliplication from the “other side”).

The syntax of the moduli stack of vielbein fields / Riemannian metrics on $\Sigma$ is

$$⊢\prod _{D^n:B\mathrm{GL}(n)}T\Sigma \to \mathrm{GL}(n)/O(n):\mathrm{Type}.$$\vdash \prod_{D^n : \mathbf{B}GL(n)} T \Sigma \to GL(n)/O(n) : Type \,.

This almost verbatim expresses the familiar statement:

A vielbein on $\Sigma$ is a $\mathrm{GL}(n)$-equivariant map from $T\Sigma$ to the coset $\mathrm{GL}(n)/O(n)$.

The categorical semantics of such a vielbein $e$ is as a diagram

$$\begin{array}{ccccc}\Sigma & & \stackrel{}{\to }& & BO(n)\\ & \searrow & {⇙}_e& {\swarrow }_{\mathrm{orth}}\\ & & B\mathrm{GL}(n)\end{array}.$$\array{ \Sigma && \stackrel{}{\to}&& \mathbf{B}O(n) \\ & \searrow &\swArrow_{e}& \swarrow_{\mathrlap{orth}} \\ && \mathbf{B}GL(n) } \,.

This in turn almost verbatim expresses the familar equivalent statement

A vielbeing is a reduction of the structure group of the $\mathrm{GL}(n)$-principal bundle $T\Sigma$ along $O(n)\to \mathrm{GL}(n)$.

This is still the naive space of fields, not yet generally covariant. So we next pass to the general covariant $B\mathrm{Aut}(T\Sigma )$-context and form the correct generally covariant space of fields, being the type in context $B\mathrm{Aut}(T\Sigma )$ given by

$$\mathrm{Conf}≔⊢\prod _{D^n:B\mathrm{GL}(n)}\sum _{T\Sigma :B\mathrm{Aut}(T\Sigma )}T\Sigma \to \mathrm{GL}(n)/O(n):\mathrm{Type},$$\mathbf{Conf} \coloneqq \vdash \prod_{D^n : \mathbf{B}GL(n)} \sum_{T\Sigma : \mathbf{B}\mathbf{Aut}(T\Sigma)} T \Sigma \to GL(n)/O(n) : Type \,,

which is the integrated BRST complex of Einstein gravity field configurations modulo diffeomorphism ghosts: the smooth groupoid whose

• objects are vielbein fields $e$ on $X$;

• morphisms are

  1. orthogonal frame transformations of the fibers of the tangent bundle;

  2. general diffeomorphisms of the base $\Sigma$.

We unwind this a bit more.

A slight subtlety in interpreting the above expression is that in

$$D^n:B\mathrm{GL}(n)⊢B\mathrm{Aut}(T\Sigma ):\mathrm{Type}$$D^n : \mathbf{B}GL(n) \vdash \mathbf{B}Aut(T \Sigma) : Type

the automorphism ∞-group of the tangent bundle it to be formed in the context of $B\mathrm{GL}(n)$. By the discussion at automorphism ∞-group the delooping $B\mathrm{Aut}(T\Sigma )$ is the ∞-image of the name

$$(*\stackrel{}{\to }\mathrm{Type})\in H_{/B\mathrm{GL}(n)}$$(* \stackrel{}{\to} Type) \in \mathbf{H}_{/\mathbf{B}GL(n)}

of $(\Sigma \to B\mathrm{GL}(n))$ in the slice. By the discussion at slice-(∞,1)-topos – Object classifier the object classifier in the slice is the projection $(\mathrm{Type}\times B\mathrm{GL}(n)\to B\mathrm{GL}(n))$.

So the name and its pullback are given by a diagram of the form

$$\begin{array}{ccccc}\Sigma & & \to & & \widehat{\mathrm{Type}}\times B\mathrm{GL}(n)\\ {}^{}\downarrow & & ⇙& & \downarrow \\ B\mathrm{GL}(n)& & \stackrel{(⊢\Sigma ,\mathrm{id})}{\to }& & \mathrm{Type}\times B\mathrm{GL}(n)\\ & {}_{\mathrm{id}}\searrow & ⇙& \swarrow \\ & & B\mathrm{GL}(n)\end{array}$$\array{ \Sigma &&\to&& \widehat{Type} \times \mathbf{B}GL(n) \\ {}^{\mathllap{}}\downarrow &&\swArrow&& \downarrow \\ \mathbf{B}GL(n) &&\stackrel{(\vdash \Sigma, id)}{\to}&& Type \times \mathbf{B}GL(n) \\ & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow \\ && \mathbf{B}GL(n) }

in $H$. Here the ∞-image is directly read off to be the factorization in the second column from the right of

$$\begin{array}{ccccccc}T\Sigma & \to & \Sigma & \to & (T\Sigma ⫽\mathrm{Aut}(T\Sigma ))\times B\mathrm{GL}(n)& \to & \widehat{\mathrm{Type}}\times B\mathrm{GL}(n)\\ \downarrow & & {}^{}\downarrow & & \downarrow & & \downarrow \\ *& \to & B\mathrm{GL}(n)& \stackrel{}{\to }& B\mathrm{Aut}(T\Sigma )\times B\mathrm{GL}(n)& \to & \mathrm{Type}\times B\mathrm{GL}(n)\\ & & & {}_{\mathrm{id}}\searrow & ⇙& \swarrow \\ & & & & B\mathrm{GL}(n)\end{array},$$\array{ T \Sigma &\to& \Sigma &\to& (T \Sigma \sslash \mathbf{Aut}(T\Sigma)) \times \mathbf{B}GL(n) &\to& \widehat{Type} \times \mathbf{B}GL(n) \\ \downarrow && {}^{\mathllap{}}\downarrow && \downarrow && \downarrow \\ * &\to& \mathbf{B}GL(n) &\stackrel{}{\to}& \mathbf{B}\mathbf{Aut}(T \Sigma) \times \mathbf{B}GL(n) &\to& Type \times \mathbf{B}GL(n) \\ && & {}_{\mathllap{id}}\searrow &\swArrow& \swarrow \\ && && \mathbf{B}GL(n) } \,,

where each square and hence each rectangle is an (∞,1)-pullback in $H$. This shows that the automorphism $\mathrm{\infty }$-group of $T\Sigma$ in the context of $B\mathrm{GL}(n)$ is just the absolute automorphism $\mathrm{\infty }$-group freely context extended. The categorical semantics of the dependent type

$$D^n:B\mathrm{GL}(n),T\Sigma :B\mathrm{Aut}(T\Sigma ):T\Sigma :\mathrm{Type}$$D^n :\mathbf{B}GL(n), T \Sigma : \mathbf{B}\mathbf{Aut}(T \Sigma) : T \Sigma : Type

is the third column from the right in the above diagram. This means that the dependent sum in

$$\mathrm{Conf}≔⊢\prod _{D^n:B\mathrm{GL}(n)}\sum _{T\Sigma :B\mathrm{Aut}(T\Sigma )}T\Sigma \to \mathrm{GL}(n)/O(n):\mathrm{Type},$$\mathbf{Conf} \coloneqq \vdash \prod_{D^n : \mathbf{B}GL(n)} \sum_{T\Sigma : \mathbf{B}\mathbf{Aut}(T\Sigma)} T \Sigma \to GL(n)/O(n) : Type \,,

Forms the internal hom in $H_{/B\mathrm{GL}(n)}$ between the homotopy fiber of that third column formed in $H_{/B\mathrm{GL}(n)}$, which is the second column (and therefore now does rememeber the $\mathrm{GL}(n)$-action on $T\Sigma$) with $\mathrm{orth}$, rememeberting that the result has an $\mathrm{Aut}(T\Sigma )$-action by precomposition.

References

History

The pre-history of the idea of general covariance is reviewed in

• H. G. Alexander (ed.), The Leibniz-Clarke Correspondence: Together With Extracts from Newton’s Principia and Opticks, Manchester University Press (1998)

The original articles by Einstein on the idea of general covariance include his Entwurf (sketch)

• Albert Einstein, M. Grossmann, Entwurf einer verallgemeinerten Relativitätstheorie und einer Theorie der Gravitation Zeitschrift für Math. Phys. 62, 225–259 (1914)

of the theory of gravity (where the notion of general covariance is still rejected) and then the full development of general relativity

• Albert Einstein, Die Grundlage der allgemeinen Relativitätstheorie. Ann. Phys. (Leipzig) 49, 769–822 (1916)

where it is fully embraced.

An attempt at a fairly comprehensive review of the history of the idea of general covariance and its reception up to modern days is in

• J. D. Norton, General covariance and the foundations of general relativity: eight decades of dispute, Rep. Prog. Phys 56 (1993), (original pdf, reprint pdf)

Formalizations of general covariance

A formalization in the context of AQFT is proposed and discussed in

• Klaus Fredenhagen, Rudolf Haag, Generally covariant quantum field theory and scaling limits, Comm. Math. Phys. Volume 108, Number 1 (1987), 91-115. (EUCLID)

• Romeo Brunetti, Klaus Fredenhagen, Rainer Verch, The generally covariant locality principle – A new paradigm for local quantum physics, Commun.Math.Phys.237:31-68,2003 (math-ph/0112041)

A review is in

• Romeo Brunetti, Martin Porrmann, Giuseppe Ruzzi, General Covariance in Algebraic Quantum Field Theory (arXiv:math-ph/0512059)

For more see the references at AQFT on curved spacetimes.

Formalization in homotopy type theory

Background and context for the above formalization of classical/quantum field theory in homotopy type theory see

• Urs Schreiber, twisted smooth cohomology in string theory, Lectures at ESI program on K-theory and quantum fields (2012)

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

See also higher category theory and physics.