Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeSep 8th 2012
    • (edited Sep 8th 2012)

    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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeSep 8th 2012
    • (edited Sep 8th 2012)

    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

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 8th 2012
    • (edited Sep 8th 2012)

    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 ΣAut(Σ)\Sigma \sslash \mathbf{Aut}(\Sigma) as a dependent type over BAut(Σ)\mathbf{B}\mathbf{Aut}(\Sigma) simply as

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

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

    Σ:BAut(Σ)Fields:Type. \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 Conf:ΣFields\mathbf{Conf} \coloneqq : \Sigma \to \mathbf{Fields}, only that now we do it in the BAut(Σ)\mathbf{B}\mathbf{Aut}(\Sigma)-context to get

    Conf= defΣ:BAut(Σ)(ΣFields):Type. \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.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 9th 2012

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

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 9th 2012

    Woops. Thanks for catching that!

    You can tell that I kept changing my mind as to which symbol to use. I have turned those XXs in paragaraph 3 and 6 now into Σ\Sigmas. Thanks.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 9th 2012

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

    here, the configuration space [Σ,Fields][\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 [Σ,Fields]/Diff(Σ)[\Sigma,Fields]/Diff(\Sigma) of this space…

    it seems to say

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

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 10th 2012

    Oh, so should it be

    here, the configuration space (ΣFields)(\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 [Σ,Fields]/Diff(Σ)[\Sigma,Fields]/Diff(\Sigma) of this space…

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeSep 10th 2012
    • (edited Sep 10th 2012)

    Oh, now I see what you mean.

    Okay, I have removed the first [Σ,Fields][\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 (ΣFields)(\Sigma \to \mathbf{Fields}) means then if you only interpret it “in context BAut(Σ)\mathbf{B}\mathbf{Aut}(\Sigma)” then it is [Σ,Fields]Diff(Σ)[\Sigma, \mathbf{Fields}]\sslash \mathbf{Diff}(\Sigma), whereas if you falsely interpret it in global context, then it is just the naive [Σ,Fields][\Sigma, \mathbf{Fields}]. But this I can’t really say at that point of the introduction yet, I guess.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

    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 :XB n𝔾 conn\nabla : X \to \mathbf{B}^n \mathbb{G}_{conn} is a differential nn-cocycle regarded as a prequantum n-bundle on XX, then the totaö space of the subobject of the internal hom on the invertible endomorphisms

    QuantMor() B n𝔾 conn[,] exp(𝔭𝔬𝔦𝔰𝔰𝔬𝔫 F ) \mathbf{QuantMor}(\nabla) \coloneqq \sum_{\mathbf{B}^n \mathbb{G}_{conn}} [\nabla, \nabla]_{\simeq} \simeq \exp(\mathfrak{poisson}_{F_\nabla})

    is the corresponding quantomorphism nn-group, the cohesive nn-group that Lie integrates the Poisson bracket Lie nn-algebra 𝔭𝔬𝔦𝔰𝔰𝔬𝔫 F \mathfrak{poisson}_{F_\nabla}.

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

    But this tautological spatement now means:

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

    This is somewhat curious. I am not aware that this has been noticed before in the literature, for n=1n = 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.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeSep 13th 2012
    • (edited Sep 13th 2012)

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

    Let’s see, the quantomorphism nn-group is characterized by having UU-probes for UHU \in \mathbf{H} given by

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

    hence the UU-families of prequantum nn-bundle auto-equivalences. This is

    H /B n𝔾 conn(((B n𝔾 conn) *U)×,) H /B n𝔾 conn((B n𝔾 conn) *U,[,] ) H(U, B n𝔾 conn[,] ) \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

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

    instead of dependent sum.

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 14th 2012

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

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeSep 14th 2012
    • (edited Sep 14th 2012)

    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 B n𝔾 conn[,] \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 nn-bundle to itself that need not respect either the connection or the principal structure

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

    And that this carries a canonical 𝔾\mathbb{G}-nn-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:

    Will be further working on that now.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 14th 2012

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

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

    Do you mean

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

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeSep 14th 2012
    • (edited Sep 14th 2012)

    So the first one has a canonical B n1𝔾\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.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeSep 15th 2012

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

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeSep 16th 2012
    • (edited Sep 21st 2012)

    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:

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

    • CommentRowNumber17.
    • CommentAuthorEric
    • CommentTimeSep 16th 2012

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

    • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeSep 17th 2012

    @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!

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeSep 21st 2012
    • (edited Sep 21st 2012)

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

    D n:BGL(n) TΣ:BAut(TΣ)(TΣGL(n)O(n)):Type. \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

    D n:Type \vdash D^n : Type

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

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

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

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

    For Σ\Sigma a smooth nn-dimensional manifold, we write

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

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

    Accordingly we have

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

    with unique term

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

    Let then orth:BO(n)BGL(n)\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

    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) }

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

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

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

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

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

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

    H Type^×X E (H,e) Type×X e X. \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

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

    This allows us to determine BAut(TΣ)H /BGL(n)\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ΣT \Sigma in the slice is the factorization in the second column from the right in

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

    the internal hom in the slice now is semantically

    Aut(TΣ)\\[TΣ,GL(n)O(n)]GL(n) BAut(TΣ)×BGL(n) \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

    D n:BAut(D n) TΣ:BAut(TΣ)TΣGL(n)/O(n):Type \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)GL(n)-equivariant map TΣGL(n)/O(n)T \Sigma \to GL(n)/O(n) and two such metrics are to be equivalent if they are related by a diffeo.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeSep 22nd 2012

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

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeNov 13th 2013
    • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 5th 2014

    Just to check, where it says

    The categorical semantics of the dependent type

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

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014

    Yes! Thanks. I have fixed it.

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 5th 2014

    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.

    • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 5th 2014
    • (edited Nov 5th 2014)

    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.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeNov 5th 2014

    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 (,n)(\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…)