General Covariance in Homotopy Type Theory

September 8, 2012

General Covariance in Homotopy Type Theory

Posted by Urs Schreiber

$MathML-enabled post (click for more details).$

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. The archetypical example of a generally covariant system is of course Einstein-gravity / “general relativity”.

I indicate here how general covariance has a natural formalization in homotopy type theory, hence internal to any $\infty$ -topos. For background and all details see at general covariance on the $n$ Lab, and the links given there.

$MathML-enabled post (click for more details).$

Of course a basic idea of traditional dependent type theory is that types $A$ may appear in context of other types $\Gamma$ . The traditional interpretation of such a dependent 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, of course, 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.

Specifically, if the context type is connected and pointed, then it is equivalent to the delooping $\Gamma \simeq \mathbf{B}G$ of an $\infty$ -group $G$ . One finds (this is discussed here) – that the context defined by the type $\mathbf{B}G$ 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$ -∞-actions is equivalent to plain homotopy type theory in context $\mathbf{B}G$ .

Consider this for the case that $G$ is an automorphism $\infty$ -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 $\mathbf{Fields}$ a moduli object for the given fields, so that a field configuration is a function $\phi : \Sigma \to \mathbf{Fields}$ , the configuration space of covariant fields is the function type $(\Sigma \to \mathbf{Fields})$ but formed in the “general covariance context” $\mathbf{B}\mathbf{Aut}(\Sigma)$ . When interpreted in smooth models, $\mathbf{Conf}$ is the smooth groupoid of field configurations and diffeomorphism gauge transformations acting on them, the Lie integration of the BRST complex whose degree-1 elements are accordingly called the diffeomorphism ghosts.

More precisely, I show the following (and thanks again to Mike, for discussion of this here).

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

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

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

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

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

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

and

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

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

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

Proposition. The categorical semantics of $\mathbf{Conf}$ in the model of smooth cohesion, and for $\Sigma$ a smooth manifold, is given by the diffeological groupoid

$\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 (off-shell) BRST complex of fields with diffeomorphism ghosts in degree 1.

Posted at September 8, 2012 11:12 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2555

5 Comments & 0 Trackbacks

Re: General Covariance in Homotopy Type Theory

$MathML-enabled post (click for more details).$

This looks great. So you’re interested in $(X \to Y)$ with equivalences under automorphisms of $X$ ? Are there other unobvious instances of this phenomenon?

Going back to basics, in a discrete setting, there are simple combinatorial situations where you work out how many distinct ways there are of colouring a die with, say, at most four colours. So you take all $4^6$ colourings and let $S_4$ act on the cube.

Does anything interesting happen with $X$ having higher homotopy?

Posted by: David Corfield on September 10, 2012 3:31 PM | Permalink | Reply to this

Re: General Covariance in Homotopy Type Theory

$MathML-enabled post (click for more details).$

So you’re interested in $(X \to Y)$ with equivalences under automorphisms of $X$ ?

Yes. Concretly I was asking myself: given $\infty$ -stacks $X$ and $Y$ , how can a succinctly construct $[X,Y]/\mathbf{Aut}(X)$ in full generality using just some diagrammatics.

I don’t know about you all, but I didn’t use to have an active internal representation of internal homs in slices of $\infty$ -toposes. It can easily get kind of convoluted when written out in terms of constructions in the original $\infty$ -topos. Speaking of “What is homotopy type theory good for?”, this is something I really learned from HoTT for my concrete $\infty$ -topos theory toolbox: to embrace internal homs in $\infty$ -slices.

So, here, I looked at the above question and thought to myself: “Hm, the only thing you can really do is form $X\sslash \mathbf{Aut}(X)$ and then hom that into $Y$ . Unfortunately, that results in something entirely unlike what I am after.” But then some voice said to me “You idiot, $X\sslash \mathbf{Aut}(X)$ naturally lives in the slice over $\mathbf{B}\mathbf{Aut}(X)$ where it is really just $X$ itself again, so you should form the internal hom there!”

It was right away clear that this had to be the right answer. But then it turned out that my toolbx for slice-computations wasn’t filled all that well. So I started making computations and was able to check that indeed the hom in the slice seems to have the right properties, but I couldn’t quite nail it down. And then luckily Mike reminded me that $\infty$ -base change is cartesian closed (which is something everybody should know of course, but which you might have more readily available if you think homotopy type theory). This then trivialized the problem and led to this blog post here.

You know, this is something I am enjoying most about this. You see, we are formalizing actual open cutting edge questions in QFT here in homotopy type theory. In this case, I am working on multisymplectic BRST. So I work a bit and then get stuck. A few years back this would have been the end of the story, given the small number of people involved in this.

But these days, and this is absolutely remarkable, I can go to a homotopy type theorist like Mike Shulman, who has zero background on anything even remotely related to “multisymplctic BRST” (that’s a fair statement, Mike, right?), and I can ask him a question. I can say:

Look, Mike, I need to construct this higher order diffeomorphism-ghost generalized-orbifold BRST complex and I am stuck at this point here, do you have an idea?

then feed that question through the physics-to-homotopy-type-theory Babel fish and – receive the solution to my problem.

Posted by: Urs Schreiber on September 11, 2012 5:56 PM | Permalink | Reply to this

Re: General Covariance in Homotopy Type Theory

$MathML-enabled post (click for more details).$

The idea that objects over a thing $X$ are equivalent to objects with an action of a thing associated to $X$ is, of course, quite old and appears all over the place, such as in the cohomological classification of bundles. John called it the “fundamental principle of Galois theory”.

The nice fact that given an object $Y$ with an action of $X$ , the corresponding object over $X$ is some kind of colimit of the given action, is also quite general, though perhaps not as well-known as it should be. For instance, it recently came up on the nForum that the “Grothendieck construction” of a functor into $Cat$ is just its lax colimit, which explains why composition in the Grothendieck construction looks similar to composition in a Kleisli category (which is also a lax colimit). In the homotopy-theoretic context, at least, it’s easy to see, because the functor “forget the map to $X$ ” from $\mathbf{H}/X$ to $\mathbf{H}$ is the left adjoint to pullback, and pullback corresponds to giving an object the trivial $X$ -action.

It’s also a well-known fact, in some circles, that in the monoidal category of objects with $G$ -action, whose morphisms are $G$ -equivariant maps, the internal hom $[X,Y]$ consists of all maps from $X$ to $Y$ (not necessarily $G$ -equivariant), with $G$ acting by conjugation (so that the fixed points of the action are the $G$ -equivariant maps). This means that categories enriched over $G$ -spaces can be confusing if you’re not used to it: they have hom-spaces on which $G$ acts, and hence an “underlying category” in a naive sense whose morphisms are the points of these hom-spaces, but this is not the “underlying category” in the formal sense of enriched category theory — that consists of the fixed points of the $G$ -action, which one should think of as the equivariant maps.

But even though I knew all of that, it still seems surprisingly magical to me that when we pass across the Galois-theory equivalence, we can conclude that function-spaces in the slice $\mathbf{H}/B G$ capture the conjugation action of $G$ on not-necessarily equivariant maps (in Urs’ case, the action on the target is trivial, so conjugation is just precomposition) — and thus the total space of this parametrized function-space is the homotopy quotient of this space of maps by the conjugation action.

Posted by: Mike Shulman on September 10, 2012 5:12 PM | Permalink | Reply to this

Re: General Covariance in Homotopy Type Theory

$MathML-enabled post (click for more details).$

[…] It’s also a well-known fact, in some circles, […]

Certainly most of the ingredients here are well known in some context. Still I feel that the homotopy type theory serves to make that which is clear be clearly clear, if I may paraphrase somebody.

I am reminded of the discussion we had here a while back in the thread What is homotopy type theory good for?. There I had given an example of how reasoning in homotopy type theory makes a problem that was generally regarded as deep and somewhat mysterious become immediately evident. I remember that from reactions such as your comment here I then thought to myself: look this is now so very obvious to those who speak in $\infty$ -toposes that those of them who haven’t seen the original version of the problem can’t even appreciate anymore that there even was once a mystery.

It’s a similar effect here that I would like to point out. I am not claiming that the insight $Act_{\mathbf{H}}(G) \simeq \mathbf{H}_{/\mathbf{B}G}$ as closed monoidal $\infty$ -categories will win anyone a Fields medal. The right reaction to that statement is instead indeed: ah right, I always roughly knew this but maybe never quite expressed it this succinctly.

I also remember a related discussion we once had here, which I won’t point to, where I pointed out that the fundamental theorem of categorical Galois theory is just the $\infty$ -Yoneda lemma applied four times in a row, which I regard as another instance of a mystery-turned-into-triviality. In that discussion I didn’t get the impression that these kinds of simplifications achieved by homotopy type theory are widely appreciated.

What I enjoyed about the issue of general covariance here is just how trivial it really becomes, in the homotopy type theory. I enjoyed the observation that the only step necessary to pass from Einstein’s (and almost everybody’s, except maybe Leibnitz’) wrong idea of his 1914 Entwurf, which is that the space of fields is

$\vdash : (\Sigma \to \mathbf{Fields}) : Type$

to Einstein’s correct observation in 1916 and including Feynman’s addition to this of diffeomorphism ghosts about 50 years later, one just has to state this in context:

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

That’s kind of neat.

(Not to forget the additional bonus that this expression not only informs us about the generally covariant space of fields of Einstein-gravity, but also of that of every $\infty$ -Chern-Simons theory with gauge $\infty$ -group being whatever and the spacetime manifold generalized to orbifolds, stacks, you name it.)

While it is true that if you decompose the proof of this statement into its separate steps, you recognize old friends in each single step, I still find this a statement worth making explicit. After all, the concepts of general covariance and diffemorphism ghosts at least tended to have a certain air of mystery associated with them, so it’s nice to see them reduced to something trivial, at least trivial to a homotopy type theorist’s eye.

(To be completely honest I should say that typing this also was a great way to procrastinate my teaching duties.)

Finally, I wasn’t motivated to look into this for its own sake. This here just seemed to be a nice intermediate statement for a blog post. What I am really meaning to use this for is understanding “multisymplectic BRST”, something that arguably is a mystery right now. This is how I always feel about conceptual reformulation in physics. Of course when it has just happened – say when you just realized that the 2 pages that Maxwell still filled with equations really just means that $d \star \nabla^2 = 0$ , you haven’t achieved anything yet, in a sense. But the thing is that only then can you go beyond what was there before.

That’s at least how I feel about it.

Posted by: Urs Schreiber on September 11, 2012 5:35 PM | Permalink | Reply to this

Re: General Covariance in Homotopy Type Theory

$MathML-enabled post (click for more details).$

I’m sorry; I didn’t mean to sound belittling, or imply that I didn’t think this post was interesting or worth writing or anything. I agree with everything you wrote! In particular, as I said, I find it surprisingly magical how these “well-known” things come together into this kind of simplicity when you approach them from the right viewpoint.

I just wanted to add some more to the discussion by pointing out connections with some other things, which may be more familiar to some readers, or which some other readers might thereby be motivated to become familiar with.

Posted by: Mike Shulman on September 14, 2012 7:05 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

September 8, 2012