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
   • CommentTimeApr 6th 2015
   • (edited Apr 6th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThis week I am at a workshop in Bristol titled _Applying homotopy type theory to physics_, funded by James Ladyman's "[Homotopy Type Theory project](http://www.bristol.ac.uk/arts/research/projects/homotopy-type-theory/)". David Corfield is also here. The program does not seem to be available publically, but among the other speakers that the $n$Lab community knows is also Jamie Vicary. Myself, I will give a survey talk titled "Modern physics formalized in Modal homotopy type theory" (which maybe should rather have "to be formalized" in the title, depending on how formal you take formal to be). I am preparing expanded notes to go with this talk, which I am keeping at * _[[schreiber:Modern Physics formalized in Modal Homotopy Type Theory]]_ This is still a bit rough at some points, but that's how it goes. I currently also have a copy of the core of this material in one section at _[[Science of Logic]]_, replacing the puny previous section on formalization that was there. While it's not puny anymore, now maybe it's too long and should be split off. But just for the time being I'll keep it there. If you look at it, you'll recognize a few points that I tried to discuss here lately, more or less successfully. This here is not meant to force more discussion about this -- we may all be happier with leaving it as it is -- it's just to announce edits, in case anyone watching the RecentlyRevised charts is wondering.

   This week I am at a workshop in Bristol titled Applying homotopy type theory to physics, funded by James Ladyman’s “Homotopy Type Theory project”. David Corfield is also here. The program does not seem to be available publically, but among the other speakers that the $n$Lab community knows is also Jamie Vicary.

   Myself, I will give a survey talk titled “Modern physics formalized in Modal homotopy type theory” (which maybe should rather have “to be formalized” in the title, depending on how formal you take formal to be). I am preparing expanded notes to go with this talk, which I am keeping at

   • Modern Physics formalized in Modal Homotopy Type Theory (schreiber)

   This is still a bit rough at some points, but that’s how it goes.

   I currently also have a copy of the core of this material in one section at Science of Logic, replacing the puny previous section on formalization that was there. While it’s not puny anymore, now maybe it’s too long and should be split off. But just for the time being I’ll keep it there.

   If you look at it, you’ll recognize a few points that I tried to discuss here lately, more or less successfully. This here is not meant to force more discussion about this – we may all be happier with leaving it as it is – it’s just to announce edits, in case anyone watching the RecentlyRevised charts is wondering.

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeApr 7th 2015
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI fixed some typos.

   I fixed some typos.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeApr 7th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks!!

   Thanks!!

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 9th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI was wondering whether the way $Loc_{\mathbb{R}}$ appears by the magic of aufhebung argues against $p$-adic physics, but then remembered that [MO question](http://mathoverflow.net/q/162803/447) you posed. But I guess what you talk about there comes later in the story.

   I was wondering whether the way $Loc_{\mathbb{R}}$ appears by the magic of aufhebung argues against $p$-adic physics, but then remembered that MO question you posed. But I guess what you talk about there comes later in the story.

5. • CommentRowNumber5.
   • CommentAuthorNikolajK
   • CommentTimeApr 13th 2015
   • (edited Apr 13th 2015)
   • PermaLink
   Author: NikolajK
   Format: MarkdownItexhttp://i.imgur.com/YsRgKgH.png That looks odd to me. It also happens to me that I see a definition where \mathcal or something might be missing, but I'm not 100% sure if it's not just a new term. Should I comment in the entry directly (not gonna make a comment like this every time). Or here, http://i.imgur.com/5D1Q3vY.png there are a bunch of term (names) and I guess some should overlap or in fact exactly not overlap, but I can't make reasonable edit.

   http://i.imgur.com/YsRgKgH.png

   That looks odd to me.

   It also happens to me that I see a definition where \mathcal or something might be missing, but I’m not 100% sure if it’s not just a new term. Should I comment in the entry directly (not gonna make a comment like this every time).

   Or here,

   http://i.imgur.com/5D1Q3vY.png

   there are a bunch of term (names) and I guess some should overlap or in fact exactly not overlap, but I can’t make reasonable edit.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeApr 13th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks for pointing out where you feel something is at odds! If you feel certain how to fix an evident typo, then doing so right away in the entry will be appreciated. In case of doubt, it doesn't hurt to ask for feedback here first. In any case, it's good to announce edits here. Regarding your first png: this is indeed meant as is, thought certainly I agree that this side-remark may be too terse to make much sense to many readers. What is going on there is that every map of types $f \colon X \to Y$ translates to a $Y$-dependent type, which may be thought of as being the preimages $f^{-1}(y)$ depending on $y \colon Y$. Precisely if $f$ is a monomorphism is this resulting dependent type a mere proposition (namely the proposition which in words reads: "is in the image of $f$"). Regarding your second png: here I am not sure if I understand what you are pointing to. Could you say it in more detail? By the way, one alternative option for pointing to precise paragraphs in an nLab entry is to prefix the paragraph with a {#label} and then link to it from here via ncatlab.org/nlab/show/page+name#label Then following the link shows the intended paragraph highlighted by gray shading.

   Thanks for pointing out where you feel something is at odds!

   If you feel certain how to fix an evident typo, then doing so right away in the entry will be appreciated. In case of doubt, it doesn’t hurt to ask for feedback here first. In any case, it’s good to announce edits here.

   Regarding your first png:

   this is indeed meant as is, thought certainly I agree that this side-remark may be too terse to make much sense to many readers. What is going on there is that every map of types $f \colon X \to Y$ translates to a $Y$-dependent type, which may be thought of as being the preimages $f^{-1}(y)$ depending on $y \colon Y$. Precisely if $f$ is a monomorphism is this resulting dependent type a mere proposition (namely the proposition which in words reads: “is in the image of $f$”).

   Regarding your second png: here I am not sure if I understand what you are pointing to. Could you say it in more detail?

   By the way, one alternative option for pointing to precise paragraphs in an nLab entry is to prefix the paragraph with a

     {#label}
   

   and then link to it from here via

   ncatlab.org/nlab/show/page+name#label

   Then following the link shows the intended paragraph highlighted by gray shading.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeApr 13th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have now added also a bit of genuine content in the last section, _Gravity_. After a bit of distraction, I'll now be focusing on this again, this is the story of higher parameterized WZW terms that I left off a while back. I still need to lay out the full story regarding solutions of sugra here more clearly. Maybe the next thing I should do is write out more precisely how underlying the étale 3-stack spacetime locally modeled on the [[supergravity Lie 3-algebra|supergravity Lie 3-group]] there is an ordinary spacetime locally modeled on its 0-truncation, $\mathbb{R}^{10,1\vert \mathbf{32}}$.

   I have now added also a bit of genuine content in the last section, Gravity.

   After a bit of distraction, I’ll now be focusing on this again, this is the story of higher parameterized WZW terms that I left off a while back.

   I still need to lay out the full story regarding solutions of sugra here more clearly. Maybe the next thing I should do is write out more precisely how underlying the étale 3-stack spacetime locally modeled on the supergravity Lie 3-group there is an ordinary spacetime locally modeled on its 0-truncation, $\mathbb{R}^{10,1\vert \mathbf{32}}$.

8. • CommentRowNumber8.
   • CommentAuthorNikolajK
   • CommentTimeApr 14th 2015
   • (edited Apr 14th 2015)
   • PermaLink
   Author: NikolajK
   Format: MarkdownItexThe reversed turnstyle is not familiar to me, and if it's read as in logic (alla $\Gamma\vdash\alpha$ and $\alpha,\Psi\vdash\vartheta$ let's you write $\Gamma,\Psi\vdash\vartheta$ (cut elimination)), then I'd expect not $f^{-1}(a)$ but a whole judgement with $:$. It might be related to adjunctions, but you have no category lingua before. In the second pic you write. $c:X\to BG$. Apart from $c$ being a term of type $C$ in the bottom left as well, I the diagram below has $B$ and $E$ into $BG$ and I don't know if it's related. The $X$ doesn't pop up below that point.

   The reversed turnstyle is not familiar to me, and if it’s read as in logic (alla $\Gamma\vdash\alpha$ and $\alpha,\Psi\vdash\vartheta$ let’s you write $\Gamma,\Psi\vdash\vartheta$ (cut elimination)), then I’d expect not $f^{-1}(a)$ but a whole judgement with $:$. It might be related to adjunctions, but you have no category lingua before.

   In the second pic you write. $c:X\to BG$. Apart from $c$ being a term of type $C$ in the bottom left as well, I the diagram below has $B$ and $E$ into $BG$ and I don’t know if it’s related. The $X$ doesn’t pop up below that point.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeApr 14th 2015
   • (edited Apr 14th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexNow I see what you mean! These were typos. I have fixed them now. Thanks.

   Now I see what you mean! These were typos. I have fixed them now. Thanks.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeApr 15th 2015
    • (edited Apr 15th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI am beginning to see how to narrow in the argument about the appearance of Lorentzian structure more. Given a [[WZW term]] $\mathbf{L}_{WZW}^V\colon V \to \mathbf{B}^{p+1}\mathbb{G}_{conn}$ I used to demand of a [[definite globalization of WZW term|definite globalization]] of it over a $V$-manifold $X$ only that it be a term $\mathbf{L}_{WZW}^X \colon X \to \mathbf{B}^{p+1}\mathbb{G}_{conn}$ which suitably restricts to $\mathbf{L}_{WZW}^V$ on the tangent spaces, which are equivalent to the infinitesimal disk $\mathbb{D}^V \to V$ in $V$. But the [[WZW term]], being constructed as a differentially twisted looping of a group cocycle $\mathbf{c} \colon \mathbf{B}V \longrightarrow \mathbf{B}^{p+2}\mathbb{G}$ carries more structure than just the bare map $\mathbf{L}_{WZW}^V$; that group cocycle itself is manifestly part of the structure that induces this map. Hence it makes sense to demand that a definite globalization of the WZW term is something stronger, namely that it also comes with a definite globalization of that group cocycle itself. For that to make sense, we need in the first place that the tangent bundle lifts from being a $\mathbb{D}^V$-fiber bundle to being a $\mathbf{B}\mathbb{D}^V$ fiber bundle, hence a Giraud $\mathbb{D}^V$-gerbe. But also, since we are talking about a group cocycle and since $Grp(\mathbf{H}) \simeq \mathbf{H}^{\ast/}_{\geq 1}$, we should not generalize too much and demand this $\mathbf{B}\mathbb{D}^V$-fiber bundle to have structure group $\mathbf{Aut}^{\ast/}(\mathbf{B}\mathbb{D}^V)\simeq \mathbf{Aut}_{Grp}(\mathbb{D}^V)$ instead of all of $\mathbf{Aut}(\mathbf{B}\mathbb{D}^V)$. That makes good sense, doesn't it. But this then gives the condition that the structure group of the frame bundle stabilizes both the group/Lie algebra structure on $\mathbb{R}^{d-1,1\vert N}$ as well as the 3-cocycle on there. And so this then constrains it to be (a higher extension of) the Lorentz Spin group.

    I am beginning to see how to narrow in the argument about the appearance of Lorentzian structure more.

    Given a WZW term $\mathbf{L}_{WZW}^V\colon V \to \mathbf{B}^{p+1}\mathbb{G}_{conn}$ I used to demand of a definite globalization of it over a $V$-manifold $X$ only that it be a term $\mathbf{L}_{WZW}^X \colon X \to \mathbf{B}^{p+1}\mathbb{G}_{conn}$ which suitably restricts to $\mathbf{L}_{WZW}^V$ on the tangent spaces, which are equivalent to the infinitesimal disk $\mathbb{D}^V \to V$ in $V$.

    But the WZW term, being constructed as a differentially twisted looping of a group cocycle $\mathbf{c} \colon \mathbf{B}V \longrightarrow \mathbf{B}^{p+2}\mathbb{G}$ carries more structure than just the bare map $\mathbf{L}_{WZW}^V$; that group cocycle itself is manifestly part of the structure that induces this map.

    Hence it makes sense to demand that a definite globalization of the WZW term is something stronger, namely that it also comes with a definite globalization of that group cocycle itself.

    For that to make sense, we need in the first place that the tangent bundle lifts from being a $\mathbb{D}^V$-fiber bundle to being a $\mathbf{B}\mathbb{D}^V$ fiber bundle, hence a Giraud $\mathbb{D}^V$-gerbe.

    But also, since we are talking about a group cocycle and since $Grp(\mathbf{H}) \simeq \mathbf{H}^{\ast/}_{\geq 1}$, we should not generalize too much and demand this $\mathbf{B}\mathbb{D}^V$-fiber bundle to have structure group $\mathbf{Aut}^{\ast/}(\mathbf{B}\mathbb{D}^V)\simeq \mathbf{Aut}_{Grp}(\mathbb{D}^V)$ instead of all of $\mathbf{Aut}(\mathbf{B}\mathbb{D}^V)$.

    That makes good sense, doesn’t it.

    But this then gives the condition that the structure group of the frame bundle stabilizes both the group/Lie algebra structure on $\mathbb{R}^{d-1,1\vert N}$ as well as the 3-cocycle on there. And so this then constrains it to be (a higher extension of) the Lorentz Spin group.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 15th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, I think that's it, should have thought of this earlier. A WZW term is a limiting cone over a certain big diagram (p. 399 in dcct [pdf](https://dl.dropboxusercontent.com/u/12630719/dcct.pdf)) and so in globalizing it one should ask to globalize that whole diagram. In its top part this means globalizing the Lie algebra cocycle, in the bottom part this means lifting to group structure and globalizing the group cocycle. Even the fact that this is to happen while sliced under the point is implied then.

    Yes, I think that’s it, should have thought of this earlier. A WZW term is a limiting cone over a certain big diagram (p. 399 in dcct pdf) and so in globalizing it one should ask to globalize that whole diagram. In its top part this means globalizing the Lie algebra cocycle, in the bottom part this means lifting to group structure and globalizing the group cocycle. Even the fact that this is to happen while sliced under the point is implied then.

12. • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 22nd 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex>There are no non-trivial judgements with (a delooping of) $\mathbb{R}$ as the subject and (a delooping of) $\mathbb{R}^{0|1}$ as the predicate. But there turn out to be some exceptional judgements with subject $\mathbb{R}^{0|q}$ and predicate $\mathbf{B}^d \mathbb{R}$. Could there be non-trivial judgements with (deloopings of) $\mathbb{R}^{0|1}$ as both the subject and the predicate?

    There are no non-trivial judgements with (a delooping of) $\mathbb{R}$ as the subject and (a delooping of) $\mathbb{R}^{0|1}$ as the predicate. But there turn out to be some exceptional judgements with subject $\mathbb{R}^{0|q}$ and predicate $\mathbf{B}^d \mathbb{R}$.

    Could there be non-trivial judgements with (deloopings of) $\mathbb{R}^{0|1}$ as both the subject and the predicate?

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeApr 22nd 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexHm, that's a good question. I haven't thought about this yet...

    Hm, that’s a good question. I haven’t thought about this yet…

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeApr 23rd 2015
    • (edited Apr 23rd 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexRegarding the localization issue and $\mathbb{R}^{0|1}$: I had myself oscillating between localization and co-localization, and then I got myself mixed up. Thanks to Dave Carchedi for catching this. If anything then it is the co-localization at $\mathbb{R}^{0|1}$ that is of relevance, and it should be equivalent to the bosonic modality $\rightsquigarrow$. Since for supermanifolds $X$ then $Hom(X,\mathbb{R}^{0|1}) = C^\infty(X)_{odd}$, even-graded $X$ are $\mathbb{R}^{0|1}$-colocal.

    Regarding the localization issue and $\mathbb{R}^{0|1}$: I had myself oscillating between localization and co-localization, and then I got myself mixed up. Thanks to Dave Carchedi for catching this. If anything then it is the co-localization at $\mathbb{R}^{0|1}$ that is of relevance, and it should be equivalent to the bosonic modality $\rightsquigarrow$.

    Since for supermanifolds $X$ then $Hom(X,\mathbb{R}^{0|1}) = C^\infty(X)_{odd}$, even-graded $X$ are $\mathbb{R}^{0|1}$-colocal.