general covariance



physics, mathematical physics, philosophy of physics

Surveys, textbooks and lecture notes

theory (physics), model (physics)

experiment, measurement, computable physics



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 [Σ,Fields]/Diff(Σ)[\Sigma,\mathbf{Fields}]/\mathbf{Diff}(\Sigma) of this space by the action of the diffeomorphism group Diff(Σ)\mathbf{Diff}(\Sigma): two Riemannian metrics g 1g_1 and g 2g_2 on Σ\Sigma represent the same field of gravity on Σ\Sigma if there is a diffeomorphism f:ΣΣf : \Sigma \stackrel{\simeq}{\to} \Sigma such that g 2=f *g 1g_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 [Σ,Fields]Diff(Σ)[\Sigma,\mathbf{Fields}]\sslash \mathbf{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 Riem(Σ)Riem(\Sigma) for the space of (pseudo-)Riemannian metrics on Σ\Sigma. For f:ΣΣf : \Sigma \to \Sigma a diffeomorphism, there is a function f *:Riem(Σ)Riem(Σ)f^* : Riem(\Sigma) \to 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ΣTΣ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 2g_1, g_2 are gauge equivalent if there is a diffeomorphism ff such that g 2=f *g 1g_2 = f^* g_1. This is an equivalence relation. Write Riem(Σ)/Diff(Σ)Riem(\Sigma)/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 Riem(Σ)/Diff(Σ)Riem(\Sigma)/Diff(\Sigma). In particular, if Σ\Sigma is compact, then the Einstein-Hilbert action functional which a priori is defined on Riem(Σ)Riem(\Sigma) descends to Riem(Σ)/Diff(Σ)Riem(\Sigma)/Diff(\Sigma)

S EH:Riem(Σ)/Diff(Σ). 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 Riem(Σ)/Diff(Σ)Riem(\Sigma)/Diff(\Sigma) needs to be refined. It is really equipped with the structure of a smooth space Riem(Σ)/Diff(Σ)\mathbf{Riem}(\Sigma)/\mathbf{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 Riem(Σ)Diff(Σ)\mathbf{Riem}(\Sigma)\sslash\mathbf{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 [Σ,orth]Diff(Σ)[\Sigma, \mathbf{orth}]\sslash \mathbf{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 gg and every given point there is a gauge equivalent field configuration f *gf^* 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).

Informal introduction

Let Σ\Sigma be a smooth manifold to be thought of as spacetime.

Then the central idea of general covariance is that for

i 1:UΣ i_1 \;\colon\; U \hookrightarrow \Sigma


i 2:UΣ i_2 \;\colon\; U \hookrightarrow \Sigma

two subsets/submanifolds, they should be regarded as equivalent if there is a diffeomorphism ϕ:ΣΣ\phi \;\colon\; \Sigma \stackrel{}{\longrightarrow} \Sigma which takes one to the other, hence such that i 2=ϕ *i 1ϕi 1i_2 = \phi^\ast i_1 \coloneqq\phi \circ i_1 .

That this statement can be puzzling if one thinks of the case U=*U = \ast as being just a single point is the content of the historical “hole argument paradox”.

But with just a little bit of formalization the apparent paradox is resolved, because the above evidently just says that the “moduli space” for “subsets of spacetime” is not the manifold Σ\Sigma itself, but is rather a “moduli stack” namely the quotient stack Σ//Diff(Σ)\Sigma //Diff(\Sigma) of Σ\Sigma by the action of the diffeomorphism group.

Indeed, the technical term “quotient stack” is precisely defined by the condition that for UU of the shape of a disk/coordinate chart, then two maps

i:UΣΣ//Diff(Σ) i \;\colon\; U \hookrightarrow \Sigma \longrightarrow \Sigma//Diff(\Sigma)

to it are equivalent if (and only if) there is a diffeomorphism relating them, as above.

So if in a generally covariant field theory spacetime is not actually the manifold Σ\Sigma, but rather the quotient stack Σ//Diff(Σ)\Sigma//Diff(\Sigma), then also a field in this generally covariant field theory should be a field on that quotient stack, not on Σ\Sigma itself.

For Fields\mathbf{Fields} a moduli space/moduli stack of fields, in a non-generally covariant field theory a field configuration is simply a map

Φ:ΣFields \Phi \;\colon\; \Sigma \longrightarrow \mathbf{Fields}

and accordingly the space of all field configurations is the mapping space [Σ,Fields][\Sigma, \mathbf{Fields}].

From this it is clear that for a generally covariant field theory we are instead to declare that the space of field configurations is

[Σ//Diff(Σ),Fields]. [\Sigma//Diff(\Sigma), \;\mathbf{Fields}] \,.

And it is at this point that the formalism of homotopy type theory/higher topos theory works a little wonder for us. Namely the formalism allows us to prove, and this is what is discussed below, that

[Σ//Diff(Σ),Fields][Σ,Fields]//Diff(Σ). [\Sigma//Diff(\Sigma),\; \mathbf{Fields}] \simeq [\Sigma,\; \mathbf{Fields}]//Diff(\Sigma) \,.

In words, the right hand side is the time-honored answer: two fields on a spacetime manifold Σ\Sigma which are such that one goes over into the other when pulled back along a diffeomorphism are gauge equivalent. This is the statement of general covariance, derived here, formally, from just the condition that any two shapes in spacetime are to be equivalent if related by a diffeomorphism.

Here to read the above equivalence as a theorem, we have to read the left hand side, as it should, be “in the context of Diff(Σ)Diff(\Sigma)-actions”. Such context-dependence is precisely what dependent homotopy type theory takes care of, and this is what the following technical statement deals with.

Introduction in terms of type theory

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

x:ΓA(x):Type x : \Gamma \vdash A(x) : Type

is that of a Γ\Gamma-parameterized family or bundle of types, whose fiber over xΓx \in \Gamma is A(x)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 ΓBG\Gamma \simeq \mathbf{B}G of an ∞-group GG. One finds – this is discussed at ∞-action – that the context defined by the type BG\mathbf{B}G is that of GG-equivariance: every type in the context is a type in the original context, but now equipped with a GG-∞-action. In a precise sense, the homotopy type theory of GG-\infty-actions is equivalent to plain homotopy type theory in context BG\mathbf{B}G.

In the following we discuss this for the case that GG 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 Fields\mathbf{Fields} a moduli object for the given fields, so that a field configuration is a function ϕ:ΣFields\phi : \Sigma \to \mathbf{Fields}, the configuration space of covariant fields is the function type (ΣFields)(\Sigma \to \mathbf{Fields}) but formed in the “general covariance context” BAut(Σ)\mathbf{B}\mathbf{Aut}(\Sigma). When interpreted in smooth models, Conf\mathbf{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.


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

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

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

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

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

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


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

Form then the type of field moduli ”Conf(ΣFields)\mathbf{Conf} \coloneqq (\Sigma \to \mathbf{Fields})” in this context:

ConfΣ:BAut(Σ)(ΣFields):Type. \mathbf{Conf} \coloneqq \;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Fields}) : Type \,.

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

Conf=[Σ,Fields]Diff(Σ) \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\mathbf{H} for the ambient homotopy type theory, or rather an interpretation given by an (∞,1)-topos. For standard applications in physics we have H=\mathbf{H} = Smooth∞Grpd or SmoothSuper∞Grpd or similar, but none of the following general discussion depends on a concrete choice for H\mathbf{H}.

Pick once and for all an object

ΣH \Sigma \in \mathbf{H}

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

The diffeomorphism group


Aut(Σ)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

*ΣType, * \stackrel{\vdash \Sigma}{\to} Type \,,

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

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

In the standard interpretation of the homotopy type theory in H=\mathbf{H} = Smooth∞Grpd Σ\Sigma could be an ordinary smooth manifold or orbifold, in particular, and then Aut(Σ)=Diff(Σ)\mathbf{Aut}(\Sigma) = \mathbf{\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\mathbf{H} and similarly refer to Aut(Σ)\mathbf{Aut}(\Sigma) loosely as the diffeomorphism group of Σ\Sigma. But even in the specifical model H=\mathbf{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 BAut(Σ)H\mathbf{B} \mathbf{Aut}(\Sigma) \in \mathbf{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

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

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

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

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

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

which we also write

VAut(Σ) Σ:BAut(Σ)V(Σ), V \sslash \mathbf{Aut}(\Sigma) \coloneqq \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma)} V(\Sigma) \,,

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

V BAut(Σ)V(Σ) ρ¯ BAut(Σ). \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 Σ:BAut(Σ)\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) is the slice (∞,1)-topos H /BAut(Σ)\mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)} and equivalently is the (∞,1)-topos of objects in H\mathbf{H} equipped with GG-∞-actions and of GG-equivariant morphisms between them:

H /BAut(Σ)Act H(Aut(Σ)). \mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)} \simeq Act_{\mathbf{H}}(\mathbf{Aut}(\Sigma)) \,.

Hence a type in context Σ:BAut(Σ)\Sigma : \mathbf{B}\mathbf{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. Σ:BAut(Σ)\Sigma : \mathbf{B}\mathbf{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 Aut(Σ)\mathbf{Aut}(\Sigma) on it, which syntactically we may write

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

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

Σ Σ:BAut(Σ)Σ ρ Σ¯ BAut(Σ), \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 Type˜Type\widetilde Type \to Type along the defining inclusion BAutType\mathbf{B}\mathbf{Aut} \hookrightarrow Type.

Here the total space

ΣAut(Σ) Σ:BAut(Σ)Σ \Sigma \sslash \mathbf{Aut}(\Sigma) \coloneqq \sum_{\Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) } \Sigma

is the homotopy quotient or action groupoid of Σ\Sigma by Aut(Σ)\mathbf{Aut}(\Sigma). This is the type characterized by the fact that a function f:UΣAut(Σ)f : U \to \Sigma \sslash \mathbf{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

FieldsH \mathbf{Fields} \in \mathbf{H}

be an object that represents the moduli ∞-stack of field configurations on Σ\Sigma for some model (in theoretical physics) to be described. For instance for GGrp(H)G \in Grp(\mathbf{H}) an ∞-group and H\mathbf{H} a cohesive homotopy type theory, we could have Fields=BG conn\mathbf{Fields} = \mathbf{B}G_{conn} the moduli for a choice of GG-principal ∞-connection, being the moduli for GG-(higher)gauge fields. For general Fields=XH\mathbf{Fields} = X \in \mathbf{H} we may always regard XX as the target space of a sigma-model.

Then the internal hom

Fields(Σ)[Σ,Fields]H \mathbf{Fields}(\Sigma) \coloneqq [\Sigma, \mathbf{Fields}] \in \mathbf{H}

hence the function type

ΣFields: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 /BAut(Σ)\mathbf{H}_{/\mathbf{B} \mathbf{Aut}(\Sigma)}.

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

H /BG BAut(Σ) BAut(Σ)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 BAut(Σ)\mathbf{B}\mathbf{Aut}(\Sigma), the moduli type Fields\mathbf{Fields} is freely moved to the general covariant context, where it is regarded as equipped with the trivial ∞-action. Accordingly we will write just FieldsH /BAut(Σ)\mathbf{Fields} \in \mathbf{H}_{/\mathbf{B}\mathbf{Aut}(\Sigma)} with that trivial action understood, which is justified by the precise syntactic expression for it:

Σ:BAut(Σ)Fields: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 ϕ\phi 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 BAut(Σ)\mathbf{B}\mathbf{Aut}(\Sigma)-context

Σ:BAut(Σ)ϕ:ΣFields \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \phi : \Sigma \to \mathbf{Fields}

and that accordingly the configuration space of fields is

Σ:BAut(Σ)ΣFields: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

Conf[ΣAut(Σ),Fields]H /Aut(Σ), \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:

Conf[Σ,Fields]Aut(Σ) \mathbf{Conf} \simeq [\Sigma,\mathbf{Fields}] \sslash \mathbf{Aut}(\Sigma)

is the homotopy quotient of the naive fields Fields(Σ)\in \mathbf{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 covariant theory over Σ\Sigma are precisely the ordinary configuration spaces of fields, but formed in the context BAut(Σ)\mathbf{B}\mathbf{Aut}(\Sigma):

Conf= defΣ:BAut(Σ)(ΣField):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=\mathbf{H} = Smooth∞Grpd or ==SynthDiff∞Grpd.

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

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

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

D n:BGL(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 H\hookrightarrow \mathbf{H} of dimension nn. As discussed at orthogonal structure and vielbein, we are to regard Σ\Sigma in the context of the delooping of the general linear group GL(n)Grp(H)GL(n) \in Grp(\mathbf{H}) via its tangent bundle TΣΣT \Sigma \to \Sigma, by which we always mean here the GL(n)GL(n)-principal bundle to which the tangent bundle is associated.

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

(ΣTΣBGL(n))H /BGL(n) (\Sigma \stackrel{\vdash T \Sigma}{\to} \mathbf{B} GL(n)) \in \mathbf{H}_{/\mathbf{B} GL(n)}

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

TΣ Σ TΣ BGL(n) \array{ T \Sigma &\to& \Sigma \\ && \downarrow^{\mathrlap{\vdash T \Sigma}} \\ && \mathbf{B}GL(n) }

in H\mathbf{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:BGL(n)TΣ(D n):Type D^n : \mathbf{B}GL(n) \vdash T \Sigma(D^n) : Type

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

D n:BGL(n)TΣ:Type. D^n : \mathbf{B}GL(n) \vdash T \Sigma : Type \,.

Let then

(BO(n)orthBGL(n))H /BGL(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)GL(n)O(n) \to GL(n) of the maximal compact subgroup of GL(n)GL(n), the orthogonal group O(n)O(n), regarded as an object in the slice-(∞,1)-topos over BGL(n)\mathbf{B}GL(n). Since this sits in the homotopy fiber sequence

GL(n)/O(n) BO(n) orth BGL(n) \array{ GL(n)/O(n) &\to& \mathbf{B}O(n) \\ && \downarrow^{\mathrlap{orth}} \\ && \mathbf{B}GL(n) }

with the coset smooth space GL(n)/O(n)GL(n)/O(n), the syntax of this object is the dependent type

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

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

H /BGL(n)Act H(GL(n)) \mathbf{H}_{/\mathbf{B}GL(n)} \simeq Act_{\mathbf{H}}(GL(n))

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

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

D n:BGL(n)TΣGL(n)/O(n):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 GL(n)GL(n)-equivariant map from TΣT \Sigma to the coset GL(n)/O(n)GL(n)/O(n).

The categorical semantics of such a vielbein ee is as a diagram

Σ BO(n) e orth BGL(n). \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 vielbein is a reduction of the structure group of the GL(n)GL(n)-principal bundle TΣT \Sigma along O(n)GL(n)O(n) \to GL(n).

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

Conf D n:BGL(n) TΣ:BAut(TΣ)TΣGL(n)/O(n):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 ee on XX;

  • 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:BGL(n)BAut(TΣ):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 BGL(n)\mathbf{B}GL(n). By the discussion at automorphism ∞-group the delooping BAut(TΣ)\mathbf{B}Aut(T \Sigma) is the ∞-image of the name

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

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

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

Σ Type^×BGL(n) BGL(n) (Σ,id) Type×BGL(n) id BGL(n) \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\mathbf{H}. Here the ∞-image is directly read off to be the factorization in the second column from the right of

TΣ Σ (TΣAut(TΣ))×BGL(n) Type^×BGL(n) * BGL(n) BAut(TΣ)×BGL(n) Type×BGL(n) id BGL(n), \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\mathbf{H}. This shows that the automorphism \infty-group of TΣT \Sigma in the context of BGL(n)\mathbf{B}GL(n) is just the absolute automorphism \infty-group freely context extended. The categorical semantics of the dependent type

D n:BGL(n),TΣ:BAut(TΣ):TΣ: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

Conf D n:BGL(n) TΣ:BAut(TΣ)TΣGL(n)/O(n):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 /BGL(n)\mathbf{H}_{/\mathbf{B}GL(n)} between the homotopy fiber of that third column formed in H /BGL(n)\mathbf{H}_{/\mathbf{B}GL(n)}, which is the second column (and therefore now does rememeber the GL(n)GL(n)-action on TΣT \Sigma) with orth\mathbf{orth}, rememeberting that the result has an Aut(TΣ)\mathbf{Aut}(T\Sigma)-action by precomposition.



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

A review is in

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

See also higher category theory and physics.

Revised on November 23, 2013 04:51:04 by David Corfield (