Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 8th 2012
   • (edited Sep 8th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI wrote a little piece at _[[general covariance]]_ on how to formalize the notion in homotopy type theory. Just for completeness, I also ended up writing a little blurb at the beginning about the genera idea of general covariance.

   I wrote a little piece at general covariance on how to formalize the notion in homotopy type theory. Just for completeness, I also ended up writing a little blurb at the beginning about the genera idea of general covariance.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeSep 8th 2012
   • (edited Sep 8th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added a bit more background information for completeness: 1. a section on [History and original formulation](http://www.ncatlab.org/nlab/show/general+covariance#HistoryAndOriginalFormulation) (currently just quoting an excellent concice and to-the-point summary paragraph from [Brunetti-Porrmann-Ruzzi](http://www.ncatlab.org/nlab/show/general+covariance#BrunettiPorrmannRuzzi)) 1. some [historical original references](http://www.ncatlab.org/nlab/show/general+covariance#ReferencesHistory), Leibniz, Einstein, ... 1. a list of literature on [formalization of general covariance in AQFT](http://www.ncatlab.org/nlab/show/general+covariance#ReferencesFormalizations)

   I have added a bit more background information for completeness:

   1. a section on History and original formulation (currently just quoting an excellent concice and to-the-point summary paragraph from Brunetti-Porrmann-Ruzzi)

   2. some historical original references, Leibniz, Einstein, …

   3. a list of literature on formalization of general covariance in AQFT

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeSep 8th 2012
   • (edited Sep 8th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have further tried to prettyfy the notation at _[[general covariance]]_, in particular concerning the type-theoretic syntax. It's kind of neat: we are entirely entitled to write $\Sigma \sslash \mathbf{Aut}(\Sigma)$ as a dependent type over $\mathbf{B}\mathbf{Aut}(\Sigma)$ simply as $$ \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \Sigma : Type $$ and we are similarly entirely entitled to write the $\mathbf{Fields}$-moduli object equipped with the tivial $\mathbf{Aut}(\Sigma)$-action as $$ \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash \mathbf{Fields} : Type \,. $$ The end result is then that the configuration space of _generally covariant_ fields on $\Sigma$ is formed entirely as we'd do naively for non-covariant fields. namely simply $\mathbf{Conf} \coloneqq : \Sigma \to \mathbf{Fields}$, only that now we do it in the $\mathbf{B}\mathbf{Aut}(\Sigma)$-context to get $$ \mathbf{Conf} =_{def} \;\;\;\;\;\; \Sigma : \mathbf{B}\mathbf{Aut}(\Sigma) \vdash (\Sigma \to \mathbf{Fields}) : Type \,. $$ It's tautological. And that's beautiful: the theorem is that if you unwind the categorical semantics of this type in the smooth model, then it is the correct answer: the Lie integration of the BRST complex of gravity with diffemorphism ghosts over $\Sigma$.

   I have further tried to prettyfy the notation at general covariance, in particular concerning the type-theoretic syntax.

   It’s kind of neat:

   we are entirely entitled to write $\Sigma \sslash \mathbf{Aut}(\Sigma)$ as a dependent type over $\mathbf{B}\mathbf{Aut}(\Sigma)$ simply as

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

   and we are similarly entirely entitled to write the $\mathbf{Fields}$-moduli object equipped with the tivial $\mathbf{Aut}(\Sigma)$-action as

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

   The end result is then that the configuration space of generally covariant fields on $\Sigma$ is formed entirely as we’d do naively for non-covariant fields. namely simply $\mathbf{Conf} \coloneqq : \Sigma \to \mathbf{Fields}$, only that now we do it in the $\mathbf{B}\mathbf{Aut}(\Sigma)$-context to get

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

   It’s tautological. And that’s beautiful: the theorem is that if you unwind the categorical semantics of this type in the smooth model, then it is the correct answer: the Lie integration of the BRST complex of gravity with diffemorphism ghosts over $\Sigma$.

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 9th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexParagraph 3 seems to say "the configuration space blah is not quite ... but is blah/Diff". And presumably all $X$s should be $\Sigma$s, and in paragraph 6.

   Paragraph 3 seems to say “the configuration space blah is not quite … but is blah/Diff”. And presumably all $X$s should be $\Sigma$s, and in paragraph 6.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeSep 9th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexWoops. Thanks for catching that! You can tell that I kept changing my mind as to which symbol to use. I have turned those $X$s in paragaraph 3 and 6 now into $\Sigma$s. Thanks.

   Woops. Thanks for catching that!

   You can tell that I kept changing my mind as to which symbol to use. I have turned those $X$s in paragaraph 3 and 6 now into $\Sigma$s. Thanks.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 9th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThat was the minor point. The slightly more major point was that in >here, the configuration space $[\Sigma,Fields]$ of physical fields over a smooth manifold $\Sigma$ is not quite the space of Riemannian metrics on $\Sigma$ itself, but is the quotient $[\Sigma,Fields]/Diff(\Sigma)$ of this space... it seems to say >$[\Sigma,Fields]$ is $[\Sigma,Fields]/Diff(\Sigma)$

   That was the minor point. The slightly more major point was that in

   here, the configuration space $[\Sigma,Fields]$ of physical fields over a smooth manifold $\Sigma$ is not quite the space of Riemannian metrics on $\Sigma$ itself, but is the quotient $[\Sigma,Fields]/Diff(\Sigma)$ of this space…

   it seems to say

   $[\Sigma,Fields]$ is $[\Sigma,Fields]/Diff(\Sigma)$

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 10th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexOh, so should it be >here, the configuration space $(\Sigma \to Fields)$ of physical fields over a smooth manifold $\Sigma$ is not quite the space of Riemannian metrics on $\Sigma$ itself, but is the quotient $[\Sigma,Fields]/Diff(\Sigma)$ of this space...

   Oh, so should it be

   here, the configuration space $(\Sigma \to Fields)$ of physical fields over a smooth manifold $\Sigma$ is not quite the space of Riemannian metrics on $\Sigma$ itself, but is the quotient $[\Sigma,Fields]/Diff(\Sigma)$ of this space…

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeSep 10th 2012
   • (edited Sep 10th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOh, now I see what you mean. Okay, I have removed the first $[\Sigma, \mathbf{Fields}]$. So I am trying to explain something starting from its naive incarnation and then successively refining it. I should just use fewer technical expressions for the "naive" version, which only serves as instance for how _not_ to proceed anyway. On the other hand, you are right with your last suggestion: The punchline of the whole entry is that if you know what $(\Sigma \to \mathbf{Fields})$ means then if you only interpret it "in context $\mathbf{B}\mathbf{Aut}(\Sigma)$" then it is $[\Sigma, \mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma)$, whereas if you falsely interpret it in global context, then it is just the naive $[\Sigma, \mathbf{Fields}]$. But this I can't really say at that point of the introduction yet, I guess.

   Oh, now I see what you mean.

   Okay, I have removed the first $[\Sigma, \mathbf{Fields}]$.

   So I am trying to explain something starting from its naive incarnation and then successively refining it. I should just use fewer technical expressions for the “naive” version, which only serves as instance for how not to proceed anyway.

   On the other hand, you are right with your last suggestion: The punchline of the whole entry is that if you know what $(\Sigma \to \mathbf{Fields})$ means then if you only interpret it “in context $\mathbf{B}\mathbf{Aut}(\Sigma)$” then it is $[\Sigma, \mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma)$, whereas if you falsely interpret it in global context, then it is just the naive $[\Sigma, \mathbf{Fields}]$. But this I can’t really say at that point of the introduction yet, I guess.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeSep 13th 2012
   • (edited Sep 13th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThere are more internal homs in $\infty$-slices that are of interest in physics -- and for some of them the fact that homotopy type theory automatically makes them live in the slice again seems to yield previously unknown or at least un-evident structures. For instance, in cohesive homotopy type theory, if $\nabla : X \to \mathbf{B}^n \mathbb{G}_{conn}$ is a differential $n$-cocycle regarded as a prequantum n-bundle on $X$, then the totaö space of the subobject of the internal hom on the invertible endomorphisms $$ \mathbf{QuantMor}(\nabla) \coloneqq \sum_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla, \nabla]_{\simeq} \simeq \exp(\mathfrak{poisson}_{F_\nabla}) $$ is the corresponding quantomorphism $n$-group, the cohesive $n$-group that Lie integrates the Poisson bracket Lie $n$-algebra $\mathfrak{poisson}_{F_\nabla}$. Now homotopy type theory says, trivially, that $[X,X]_\simeq$ itself is in context $\mathbf{B}^n \mathbb{G}_{conn}$. But this tautological spatement now means: > There is a canonical $\mathbb{G}$-principal $n$-bundle with connection on the quantomorphism $n$-group $\mathbf{QuantMor}(\nabla)$. This is somewhat curious. I am not aware that this has been noticed before in the literature, for $n = 1$. The most sophisticated discssion of the quantomorphism group that I am aware of (listed at [[quantomorphism group]]) struggles to get to the point that it establishes a smooth structure on the group in the first place (which is another thing that homotopy type theory gives for free). I am not aware that anyone did anything nontrivial with this smooth structure, such as constructing a connection over it. (But if anyone here knows more, I'd be most grateful for a pointer.) So that's a little exercise: understand what homotopy type theory is teaching us here about prequantum physics.

   There are more internal homs in $\infty$-slices that are of interest in physics – and for some of them the fact that homotopy type theory automatically makes them live in the slice again seems to yield previously unknown or at least un-evident structures.

   For instance, in cohesive homotopy type theory, if $\nabla : X \to \mathbf{B}^n \mathbb{G}_{conn}$ is a differential $n$-cocycle regarded as a prequantum n-bundle on $X$, then the totaö space of the subobject of the internal hom on the invertible endomorphisms

   $$\mathbf{QuantMor}(\nabla) \coloneqq \sum_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla, \nabla]_{\simeq} \simeq \exp(\mathfrak{poisson}_{F_\nabla})$$

   is the corresponding quantomorphism $n$-group, the cohesive $n$-group that Lie integrates the Poisson bracket Lie $n$-algebra $\mathfrak{poisson}_{F_\nabla}$.

   Now homotopy type theory says, trivially, that $[X,X]_\simeq$ itself is in context $\mathbf{B}^n \mathbb{G}_{conn}$.

   But this tautological spatement now means:

   There is a canonical $\mathbb{G}$-principal $n$-bundle with connection on the quantomorphism $n$-group $\mathbf{QuantMor}(\nabla)$.

   This is somewhat curious. I am not aware that this has been noticed before in the literature, for $n = 1$. The most sophisticated discssion of the quantomorphism group that I am aware of (listed at quantomorphism group) struggles to get to the point that it establishes a smooth structure on the group in the first place (which is another thing that homotopy type theory gives for free). I am not aware that anyone did anything nontrivial with this smooth structure, such as constructing a connection over it. (But if anyone here knows more, I’d be most grateful for a pointer.)

   So that’s a little exercise: understand what homotopy type theory is teaching us here about prequantum physics.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHm, sorry, I seem to have dependent sum and dependent product mixed up in the above. Let's see, the quantomorphism $n$-group is characterized by having $U$-probes for $U \in \mathbf{H}$ given by $$ \mathbf{H}(U, \mathbf{QuantMor}_\nabla) = \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}}( U \times X, X )_\simeq \,, $$ hence the $U$-families of prequantum $n$-bundle auto-equivalences. This is $$ \begin{aligned} \cdots & \simeq \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}} \left( \left( \left(\mathbf{B}^n \mathbb{G}_{conn}\right)^* U \right) \times \nabla, \nabla \right)_\simeq \\ & \simeq \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}}\left( \left(\mathbf{B}^n\mathbb{G}_{conn}\right)^* U, [\nabla,\nabla]_\simeq \right) \\ & \simeq \mathbf{H}( U, \prod_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla,\nabla]_\simeq ) \end{aligned} $$ and so Mr. Yoneda says that $$ \mathbf{QuantMor}_\nabla \simeq \prod_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla,\nabla]_\simeq $$ instead of dependent sum.

    Hm, sorry, I seem to have dependent sum and dependent product mixed up in the above.

    Let’s see, the quantomorphism $n$-group is characterized by having $U$-probes for $U \in \mathbf{H}$ given by

    $$\mathbf{H}(U, \mathbf{QuantMor}_\nabla) = \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}}( U \times X, X )_\simeq \,,$$

    hence the $U$-families of prequantum $n$-bundle auto-equivalences. This is

    $$\begin{aligned} \cdots & \simeq \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}} \left( \left( \left(\mathbf{B}^n \mathbb{G}_{conn}\right)^* U \right) \times \nabla, \nabla \right)_\simeq \\ & \simeq \mathbf{H}_{/\mathbf{B}^n \mathbb{G}_{conn}}\left( \left(\mathbf{B}^n\mathbb{G}_{conn}\right)^* U, [\nabla,\nabla]_\simeq \right) \\ & \simeq \mathbf{H}( U, \prod_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla,\nabla]_\simeq ) \end{aligned}$$

    and so Mr. Yoneda says that

    $$\mathbf{QuantMor}_\nabla \simeq \prod_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$$

    instead of dependent sum.

11. • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 14th 2012
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexSo, after #10, what changes in #9 now we know it's product not sum we need?

    So, after #10, what changes in #9 now we know it’s product not sum we need?

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeSep 14th 2012
    • (edited Sep 14th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexRight, I should have said this (And I am sorry for spreading confusion that contradicts the whole point of what I myself just said a few entries before, I shouldn't post in certain states of tiredness and travelling and certainly not when both coincide, sorry. I ran out of my lecture yesterday, biked to the train station, jumped on the night train to Erlangen. Was a good bit exhausted. Somehow my fingers started typing (out of habit, I suppose) but my brain hadn't caught up yet. ) So $\sum_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$ is a differential refinement of the action groupoid of * invertible maps $\nabla \to \nabla$ from the prequantum $n$-bundle to itself that need _not_ respect either the connection or the principal structure * by the conjugation action of these by $\mathbf{B}^{n-1} \mathbb{G}$. And that this carries a canonical $\mathbb{G}$-$n$-connection is actually not surprising. I have begun last night to create notes on related topics for the talk of mine that I gave this morning just a few minutes back. I ran out of steam at 3:30 last night, this is how far I got so far: * [[schreiber:Erlangen2012]] Will be further working on that now.

    Right, I should have said this

    (And I am sorry for spreading confusion that contradicts the whole point of what I myself just said a few entries before, I shouldn’t post in certain states of tiredness and travelling and certainly not when both coincide, sorry. I ran out of my lecture yesterday, biked to the train station, jumped on the night train to Erlangen. Was a good bit exhausted. Somehow my fingers started typing (out of habit, I suppose) but my brain hadn’t caught up yet. )

    So $\sum_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$ is a differential refinement of the action groupoid of

    • invertible maps $\nabla \to \nabla$ from the prequantum $n$-bundle to itself that need not respect either the connection or the principal structure

    • by the conjugation action of these by $\mathbf{B}^{n-1} \mathbb{G}$.

    And that this carries a canonical $\mathbb{G}$-$n$-connection is actually not surprising.

    I have begun last night to create notes on related topics for the talk of mine that I gave this morning just a few minutes back. I ran out of steam at 3:30 last night, this is how far I got so far:

    • Erlangen2012 (schreiber)

    Will be further working on that now.

13. • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 14th 2012
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexNo need to apologise. And don't wear yourself out! >So $\sum_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$... Do you mean >So $\product_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$... ?

    No need to apologise. And don’t wear yourself out!

    So $\sum_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$…

    Do you mean

    So $\product_{\mathbf{B}^n\mathbb{G}_{conn}} [\nabla,\nabla]_\simeq$… ?

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeSep 14th 2012
    • (edited Sep 14th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexSo the first one has a canonical $\mathbf{B}^{n-1}\mathbb{G}$-connection on it (trvially so), the second one does not. But the second one is the actual quantomorphism group.

    So the first one has a canonical $\mathbf{B}^{n-1}\mathbb{G}$-connection on it (trvially so), the second one does not. But the second one is the actual quantomorphism group.

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeSep 15th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexJust for the record, since I mentioned it above: I now had a chance to turn these notes into something more coherent: _[[schreiber:Erlangen2012]]_.

    Just for the record, since I mentioned it above: I now had a chance to turn these notes into something more coherent: Erlangen2012 (schreiber).

16. • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeSep 16th 2012
    • (edited Sep 21st 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexIt seems to take me a bit to converge to the optimal way of expressing myself here. But now I have finally made more explicit, at _[[general covariance]]_, that for the example of Einstein gravity, the generally covariant configuration space is in full beauty in type theory syntax: $$ \vdash \prod_{\mathbf{c} : \mathbf{B} GL(n)} \sum_{T \Sigma : \mathbf{B}\mathbf{Aut}(T \Sigma)} (T \Sigma \to \mathbf{orth}) : Type \,. $$ and more background on reading this expressin is now at _[infinity-action -- Notions in representation theory](http://ncatlab.org/nlab/show/infinity-action#NotionsInHigherRepresentationTheory)_

    It seems to take me a bit to converge to the optimal way of expressing myself here. But now I have finally made more explicit, at general covariance, that for the example of Einstein gravity, the generally covariant configuration space is in full beauty in type theory syntax:

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

    and more background on reading this expressin is now at infinity-action – Notions in representation theory

17. • CommentRowNumber17.
    • CommentAuthorEric
    • CommentTimeSep 16th 2012
    • PermaLink
    Author: Eric
    Format: MarkdownItexIt is likely just my iPhone, but the symbol for action groupoid is coming out like a square.

    It is likely just my iPhone, but the symbol for action groupoid is coming out like a square.

18. • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeSep 17th 2012
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@Eric: Probably missing fonts. I'm on a borrowed computer now and am seeing several boxes, although at least mine are helpfully filled with Unicode numbers so I can look them up!

    @Eric: Probably missing fonts. I’m on a borrowed computer now and am seeing several boxes, although at least mine are helpfully filled with Unicode numbers so I can look them up!

19. • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeSep 21st 2012
    • (edited Sep 21st 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHere some rough notes further spelling out the homotopy type theoretic formula for the generally covariant configuration space of Einstein-gravity $$ \vdash \prod_{D^n : \mathbf{B}GL(n)} \sum_{T \Sigma : \mathbf{B}\mathbf{Aut}(T \Sigma)} (T \Sigma \to GL(n)\sslash O(n)) : Type \,. $$ in more detail. (I will turn this into something more readable later. Need to quit now after a long day, but want to record these quick notes for later processing. Don't bother if you are just following leisurely). We spell out what this means. We work in [[nLab:synthetic differential infinity-groupoid|synthetic differential cohesion]]. Let there $$ \vdash D^n : Type $$ denote the first-order infinitesimal neighbourhood of the origin in $\mathbb{R}^n$. Observing that the [[general linear group]] is $$ GL(n) \simeq \mathbf{Aut}(D^n) $$ we will write the unique term of $\mathbf{B}GL(n)$ as $$ \vdash D^n : \mathbf{B} GL(n) \,. $$ For $\Sigma$ a smooth $n$-dimensional manifold, we write $$ \Sigma \stackrel{\vdash T \Sigma}{\to} \mathbf{B} GL(n) $$ for the map modulating the $GL(n)$-principal bundle to which the tangent bundle is associated. Accordingly we have $$ D^n : \mathbf{B}GL(n) \vdash \mathbf{B}\mathbf{Aut}(T \Sigma) : Type $$ with unique term $$ D^n : \mathbf{B}GL(n) \vdash T \Sigma : \mathbf{B} \mathbf{Aut}(T \Sigma) \,. $$ Let then $\mathbf{orth} : \mathbf{B} O(n) \to \mathbf{B}GL(n)$ be given by the inclusion of the maximal compact subgroup. We have a fiber sequence $$ \array{ GL(n)/O(n) &\to& \mathbf{B}O(n) \\ && \downarrow^{\mathrlap{orth}} \\ && \mathbf{B}GL(n) } $$ and so the syntax for $\mathbf{orth} \in \mathbf{H}_{/\mathbf{B}GL(n)}$ is $$ D^n : \mathbf{B}GL(n) \vdash (GL(n)/O(n))(D^n) : Type \,. $$ Next we need to determine $\mathbf{B} \mathbf{Aut}(T \Sigma) \in \mathbf{H}_{/\mathbf{B}GL(n)}$. Observe that if $Type \in \mathbf{H}$ is the small object classifier of $\mathbf{H}$, then for any $X \in \mathbf{H}$ the projection $$ \array{ Type \times X \\ \downarrow \\ X } $$ is the small object classifier in $\mathbf{H}_{/X}$. To see this notice that slice types over $e : E \to X$ are obtained by the pullback (all our diagrams are in $\mathbf{H}$) $$ \array{ H &&\to&& \widehat{Type} \times X \\ \downarrow &&\swArrow&& \downarrow \\ E &&\stackrel{(\vdash H , e)}{\to}&& Type \times X \\ & {}_{\mathllap{e}}\searrow &\swArrow& \swarrow \\ && X } \,. $$ Hence in our case $$ \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) } \,. $$ This allows us to determine $\mathbf{B} \mathbf{Aut}(T \Sigma) \in \mathbf{H}_{/\mathbf{B}GL(n)}$. For the delooping of the automorphism group of an object is the image factorization of its name. This image factorization for the name of $T \Sigma$ in the slice is the factorization in the second column from the right in $$ \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 a pullback. the internal hom in the slice now is semantically $$ \array{ \mathbf{Aut}(T \Sigma)\backslash\backslash[T \Sigma, GL(n)\sslash O(n)] \sslash GL(n) \\ \downarrow \\ \mathbf{B}\mathbf{Aut}(T \Sigma) \times \mathbf{B}GL(n) } $$ So now $$ \vdash \prod_{D^n : \mathbf{B}\mathbf{Aut}(D^n)} \sum_{T \Sigma : \mathbf{B} \mathbf{Aut}(T \Sigma)} \vdash T \Sigma \to GL(n)/O(n) : Type $$ is seen to reduce to a familiar statement in words: a vielbein = metric is a reduction of the structure group of the frame bundle exhibited by a $GL(n)$-equivariant map $T \Sigma \to GL(n)/O(n)$ and two such metrics are to be equivalent if they are related by a diffeo.

    Here some rough notes further spelling out the homotopy type theoretic formula for the generally covariant configuration space of Einstein-gravity

    $$\vdash \prod_{D^n : \mathbf{B}GL(n)} \sum_{T \Sigma : \mathbf{B}\mathbf{Aut}(T \Sigma)} (T \Sigma \to GL(n)\sslash O(n)) : Type \,.$$

    in more detail. (I will turn this into something more readable later. Need to quit now after a long day, but want to record these quick notes for later processing. Don’t bother if you are just following leisurely).

    We spell out what this means.

    We work in synthetic differential cohesion. Let there

    $$\vdash D^n : Type$$

    denote the first-order infinitesimal neighbourhood of the origin in $\mathbb{R}^n$. Observing that the general linear group is

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

    we will write the unique term of $\mathbf{B}GL(n)$ as

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

    For $\Sigma$ a smooth $n$-dimensional manifold, we write

    $$\Sigma \stackrel{\vdash T \Sigma}{\to} \mathbf{B} GL(n)$$

    for the map modulating the $GL(n)$-principal bundle to which the tangent bundle is associated.

    Accordingly we have

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

    with unique term

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

    Let then $\mathbf{orth} : \mathbf{B} O(n) \to \mathbf{B}GL(n)$ be given by the inclusion of the maximal compact subgroup. We have a fiber sequence

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

    and so the syntax for $\mathbf{orth} \in \mathbf{H}_{/\mathbf{B}GL(n)}$ is

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

    Next we need to determine $\mathbf{B} \mathbf{Aut}(T \Sigma) \in \mathbf{H}_{/\mathbf{B}GL(n)}$.

    Observe that if $Type \in \mathbf{H}$ is the small object classifier of $\mathbf{H}$, then for any $X \in \mathbf{H}$ the projection

    $$\array{ Type \times X \\ \downarrow \\ X }$$

    is the small object classifier in $\mathbf{H}_{/X}$. To see this notice that slice types over $e : E \to X$ are obtained by the pullback (all our diagrams are in $\mathbf{H}$)

    $$\array{ H &&\to&& \widehat{Type} \times X \\ \downarrow &&\swArrow&& \downarrow \\ E &&\stackrel{(\vdash H , e)}{\to}&& Type \times X \\ & {}_{\mathllap{e}}\searrow &\swArrow& \swarrow \\ && X } \,.$$

    Hence in our case

    $$\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) } \,.$$

    This allows us to determine $\mathbf{B} \mathbf{Aut}(T \Sigma) \in \mathbf{H}_{/\mathbf{B}GL(n)}$. For the delooping of the automorphism group of an object is the image factorization of its name. This image factorization for the name of $T \Sigma$ in the slice is the factorization in the second column from the right in

    $$\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 a pullback.

    the internal hom in the slice now is semantically

    $$\array{ \mathbf{Aut}(T \Sigma)\backslash\backslash[T \Sigma, GL(n)\sslash O(n)] \sslash GL(n) \\ \downarrow \\ \mathbf{B}\mathbf{Aut}(T \Sigma) \times \mathbf{B}GL(n) }$$

    So now

    $$\vdash \prod_{D^n : \mathbf{B}\mathbf{Aut}(D^n)} \sum_{T \Sigma : \mathbf{B} \mathbf{Aut}(T \Sigma)} \vdash T \Sigma \to GL(n)/O(n) : Type$$

    is seen to reduce to a familiar statement in words:

    a vielbein = metric is a reduction of the structure group of the frame bundle exhibited by a $GL(n)$-equivariant map $T \Sigma \to GL(n)/O(n)$ and two such metrics are to be equivalent if they are related by a diffeo.

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeSep 22nd 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have expanded and polished the section _[Generally covariant field of gravity](http://www.ncatlab.org/nlab/show/general+covariance#GravityInHoTT)_ more.

    I have expanded and polished the section Generally covariant field of gravity more.

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeNov 13th 2013
    • PermaLink
    Author: Urs
    Format: MarkdownItexhave add a paragraph to a new subsection _[general covariance -- Formalization in HoTT -- Informal introduction](http://ncatlab.org/nlab/show/general+covariance#InHomotopyTypeTheory)_.

    have add a paragraph to a new subsection general covariance – Formalization in HoTT – Informal introduction.

22. • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 5th 2014
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexJust to check, where it says >The [[categorical semantics]] of the [[dependent 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. that should be $\vdash$ rather than :, and 'third column (from left)''?

    Just to check, where it says

    The categorical semantics of the dependent 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.

    that should be $\vdash$ rather than :, and ’third column (from left)”?

23. • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes! Thanks. I have fixed it.

    Yes! Thanks. I have fixed it.

24. • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 5th 2014
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexSo now maybe >Here the ∞-image is directly read off to be the factorization in the second column from the right of could also say 'third column'. All very trivial, but I'm trying to understand what perhaps is one of the most sophisticated pieces of working within a complex context in type theory. I'm trying to think about when we do something similar in every day reasoning, and whether there's something special about gravitation as a force that lends itself to this nice 'within a context' account. But little time today. By the way, I finally 'saw' the truth of the principle of equivalence at about 4:18 into this [clip](https://www.youtube.com/watch?v=E43-CfukEgs) of feathers and ball falling in a vacuum.

    So now maybe

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

    could also say ’third column’.

    All very trivial, but I’m trying to understand what perhaps is one of the most sophisticated pieces of working within a complex context in type theory. I’m trying to think about when we do something similar in every day reasoning, and whether there’s something special about gravitation as a force that lends itself to this nice ’within a context’ account. But little time today.

    By the way, I finally ’saw’ the truth of the principle of equivalence at about 4:18 into this clip of feathers and ball falling in a vacuum.

25. • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 5th 2014
    • (edited Nov 5th 2014)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOne query. The account in 'Generally covariant field of gravity' is given in terms of the specific topos SynthDiff∞Grpd. How far can one just let the properties of differential cohesion do the job? I mean could there be a large chunk of general relativity present in a wide range of differential cohesive $\infty$-toposes? I guess that's to know answers to some of the issues being discussed on the other [thread](http://nforum.mathforge.org/discussion/6288/axiomatic-tangent-structure-of-etale-homotopy-types/).

    One query. The account in ’Generally covariant field of gravity’ is given in terms of the specific topos SynthDiff∞Grpd. How far can one just let the properties of differential cohesion do the job? I mean could there be a large chunk of general relativity present in a wide range of differential cohesive $\infty$-toposes?

    I guess that’s to know answers to some of the issues being discussed on the other thread.

26. • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItex> could also say ’third column’. Yes, have changed it. Thanks. > I’m trying to think about when we do something similar in every day reasoning, While I am not sure about the every day of the man on the street, one could maybe say that while Einstein and his contemporaries were still struggling heavily with the idea ([Einstein-Grossmann 14](http://ncatlab.org/nlab/show/general+covariance#EinsteinGrossmann) is explicitly rejecting the idea), their students learned the lesson to many theoretical physicists these days "thinking covariantly" has become second nature in a way that is not unlike "thinking in a context where everything is modulo diffeomorphisms". Of course just as often it still happens that people forget the lesson. > whether there’s something special about gravitation as a force that lends itself to this nice ’within a context’ account Actually, no, I think it is important that "general covariance" is not specific to gravity. Back then in the article "QFT and the Jones polynomian" Witten still highlights this idea as new, that topological field theories share the same feature. Indeed, in Chern-Simons theory it is there, and the only reason why one does not see it emphasized so much is that CS-theory has yet another gauge symmetry, and that by coincidence of low dimensions it so happens that in 3d every diffeomorphism acting on a CS gauge field is equivalent to just a gauge transformation acting on that gauge field. This fact is embodied also in the $(\infty,n)$-cobordism hypothesis/theorem: everything there is "generally covariant". > I finally ’saw’ the truth of the principle of equivalence at about 4:18 into this clip Nice. I have added the link to _[[equivalence principle (physics)]]_ > The account in ’Generally covariant field of gravity’ is given in terms of the specific topos SynthDiff∞Grpd. How far can one just let the properties of differential cohesion do the job? I mean could there be a large chunk of general relativity present in a wide range of differential cohesive ∞-toposes? Yes, absolutely. Indeed the point of an abstract homotopy type theoretic discussion of general covariance (or any other concept in physics) is precisely to see that and how it is independent of the specific model and is a more general principle. I was just amplifying this to Gabriel Catren, my host in Paris this month. He is interested in describing geometric quantization via integrable real polarizations as a quotient map analogous to gauge quotients, and the construction that does this is a very fundamental one in homotopy type theory, hence is exceedingly more general than it might seem on first sight. I started making notes on that [here](http://ncatlab.org/nlab/show/infinity-action#ExamplesActionsInASlice) (purely technical for the moment, will need to find time to expand on the story...)

    could also say ’third column’.

    Yes, have changed it. Thanks.

    I’m trying to think about when we do something similar in every day reasoning,

    While I am not sure about the every day of the man on the street, one could maybe say that while Einstein and his contemporaries were still struggling heavily with the idea (Einstein-Grossmann 14 is explicitly rejecting the idea), their students learned the lesson to many theoretical physicists these days “thinking covariantly” has become second nature in a way that is not unlike “thinking in a context where everything is modulo diffeomorphisms”. Of course just as often it still happens that people forget the lesson.

    whether there’s something special about gravitation as a force that lends itself to this nice ’within a context’ account

    Actually, no, I think it is important that “general covariance” is not specific to gravity. Back then in the article “QFT and the Jones polynomian” Witten still highlights this idea as new, that topological field theories share the same feature. Indeed, in Chern-Simons theory it is there, and the only reason why one does not see it emphasized so much is that CS-theory has yet another gauge symmetry, and that by coincidence of low dimensions it so happens that in 3d every diffeomorphism acting on a CS gauge field is equivalent to just a gauge transformation acting on that gauge field.

    This fact is embodied also in the $(\infty,n)$-cobordism hypothesis/theorem: everything there is “generally covariant”.

    I finally ’saw’ the truth of the principle of equivalence at about 4:18 into this clip

    Nice. I have added the link to equivalence principle (physics)

    The account in ’Generally covariant field of gravity’ is given in terms of the specific topos SynthDiff∞Grpd. How far can one just let the properties of differential cohesion do the job? I mean could there be a large chunk of general relativity present in a wide range of differential cohesive ∞-toposes?

    Yes, absolutely. Indeed the point of an abstract homotopy type theoretic discussion of general covariance (or any other concept in physics) is precisely to see that and how it is independent of the specific model and is a more general principle.

    I was just amplifying this to Gabriel Catren, my host in Paris this month. He is interested in describing geometric quantization via integrable real polarizations as a quotient map analogous to gauge quotients, and the construction that does this is a very fundamental one in homotopy type theory, hence is exceedingly more general than it might seem on first sight. I started making notes on that here (purely technical for the moment, will need to find time to expand on the story…)