started topologically twisted D=4 super Yang-Mills theory, in order to finally write a reply to that MO question we were talking about. But am being interrupted now…
]]>created a bare minimum at jet group
]]>Thomas Holder has been working on Aufhebung. I have edited the formatting a little (added hyperlinks and more Definition-environments, added another subsection header and some more cross-references, cross-linked with duality of opposites).
]]>We are in the process of finalizing an article on prequantum theory in higher geometry. An early version of our writeup I have now uploaded. It needs a few more cycles of polishing, but I thought I’ll provide this here on the nForum right now as a kind of explanation for the sheer drop in the amount of noise that I have been making around the nLab as of lately ;-:
Domenico Fiorenza, Chris Rogers, Urs Schreiber,
Regulars here will recognize various things that I/we have been talking about for a good while now. Finally they are materializing in a more pdf-kind of incarnation…
]]>While working at geometry of physics on the next chapter Differentiation I am naturally led back to think again about how to best expose/introduce infinitesimal cohesion. To the reader but also, eventually, to Coq.
First the trivial bit, concerning terminology: I am now tending to want to call it differential cohesion, and differential cohesive homotopy type theory. What do you think?
Secondly, I have come to think that the extra right adjoint in an infinitesimally cohesive neighbourhood need not be part of the axioms (although it happens to be there for ).
So I am now tending to say
Definition. A differential structure on a cohesive topos is an ∞-connected and locally ∞-connected geometric embedding into another cohesive topos.
And that’s it. This induces a homotopy cofiber sequence
Certainly that alone is enough axioms to say in the model of smooth cohesion all of the following:
So that seems to be plenty of justification for these axioms.
We should, I think, decide which name is best (“differential cohesion”?, “infinitesimal cohesion”?) and then get serious about the “differential cohesive homotopy type theory” or “infinitesimal cohesive homotopy type theory” or maybe just “differential homotopy type theory” respectively.
]]>Since it touches on several of the threads that we happen to have here, hopefully I may be excused for making this somewhat selfish post here.
For various reasons I need to finally upload my notes on “differential cohomology in a cohesive ∞-topos” to the arXiv. Soon. Maybe by next week or so.
It’s not fully finalized, clearly, I could spend ages further polishing this – but then it will probably never be fully finalized, as so many other things.
Anyway, in case anyone here might enjoy eyeballing pieces of it (again), I am keeping the latest version here
]]>added some lines to differential algebraic K-theory
also a stub Beilinson regulator
]]>For discussion at geometry of physics I need a way to point to the concept of “locality” in QFT, so I gave it a small entry: local quantum field theory.
]]>[First time posting here.. please correct me kindly if I have not followed any explicit or implicit rules. And please excuse my question if it’s vague.]
It’s exciting to see that HoTT can prove concrete homotopical results, like . It seems that to go further into other subfields, we need modality and cohesion in the theory to “buff up” the local structures – be it topological, smooth, or super-smooth..
However, I had a hard time tapping into modality and cohesion. First of, I’ve tried to understand what a cohesive topos means. As a first example of a cohesive topos, I’ve read through geometry+of+physics+–+smooth+sets and found it exciting. However, it remains unclear how to build up a theory with local model “X” from scratch by myself.
To do that, I planned to read Shulman’s proof on Brouwer’s fixed point.. hoping to understand the process by looking at a classical theorem in topology. But it is unfortunately too advanced for me, I’m not even sure where to start asking if there’s someone to help. Not being too familiar with type theory, I reckon there must be something missing.
What would you suggest if I want to quickly tap into these kind of modalic math, understand at least the proof for Brouwer fixed point, and hopefully be able to understand Schreiber’s foundation of geometry and physics?
4th year math PhD student. I’m not afraid of reading formal papers.. as long as it’s as much self-sufficient as possible. In fact, I find there’s “too much” motivation out there.. I hope to get serious, and even start to think/research in this language. Put in another way using an analogy in the world of programming: I regard Def/Thm/Proof as the source code of a program, and a regular math paper as the literate code or the manual/documentation of the source code. Sometimes it’s nice to have docs to read.. but sometimes you’d rather dive into the source code to see what it is. My mood is at the latter stage.
I’m willing to provide more details if it’d be helpful. Thank you very much!
]]>created super infinity-groupoid
(to be distinguished from smooth super infinity-groupoid!)
currently the main achievement of the page is to list lots of literature in support of the claim that the site of superpoints is the correct site to consider here.
]]>created a bare minimum at higher order frame bundle and cross-linked a bit
]]>I have split off the section on points-to-pieces transform from cohesive topos and expanded slightly, pointing also to comparison map between algebraic and topological K-theory
]]>if you have been looking at the logs you will have seen me work on this for a few days already, so I should say what I am doing:
I am working on creating an entry twisted smooth cohomology in string theory . This is supposed to eventually serve as the set of notes for my lectures at the ESI Program K-Theory and Quantum Fields in the next weeks.
This should probably sit on my personal web, and I can move it there eventually. But for the moment I am developing it as an Lab entry because that saves me from prefixing every single wiki-link with
nLab:
]]>
Yesterday I had filled in some minimum regarding the idea of rheonomy at D’Auria-Fre formulation of supergravity. (I thought I had done this long ago, but found the section empty now. )
There is something immensely curious going on here, which I was wanting to formalize ever since I started looking into this. Now maybe I am getting closer, but I am still stuck with something:
So the simple beautiful idea of rheonomy is that differential forms on a supermanifold are constrained to be something like “holomorphic” in the super-direction, in that they are fully determined by their restriction along the inclusion of the underlying ordinary manifold, in (vague? or good?) analogy with how holomorphic functions on are determined by their restriction along . This rheonomy constraint turns out to be equivalent to the more popular “superspace constraints” that are used elsewhere in the SuGra literature, but is evidently conceptually a much nicer perspective.
The striking claim then is that the equations of motion of supergravity theories enode precisely nothing but the constraint on a higher super-Cartan geometry on , modeled on a given extended super-Minkowski spacetime, to have higher super-vielbein fields which, as super-differential forms on , are rheonomic.
So the statement is something like that a solution to supergravity is nothing but a certain -structure satisfying a “holomorphicity”-like constraint.
Apart from being beautiful and remarkable in itself, this smells like it has a good chance of having an “elementary” formalization in differential cohesion. That’s what I am after. I know how to naturally say “higher super-Cartan geometry” axiomatically in differential cohesion, but I don’t know yet how to say “rheonomy” in this way.
In fact I am pretty much in the dark about it at the moment, but from the above there are some evident guesses as to what one has to consider.
So given some manifold modeled on a framed space , such as some extended super-Minkowski spacetime, then we are simply looking at an orthogonal structure exhibited by a diagram of the form
where the homotopy is (for some value of “is”) the vielbein, i.e. in the running example it is the super-vielbein together with the relevant higher form fields.
Now we may restrict this Cartan geometry to the underlying ordinary (reduced) manifold, simply by precomposing with the unit of the reduction modality
So rheonomy is supposed to be some constraint on that makes it be fully determined by its restriction .
When one expresses in terms of actual differential forms with values in a super--algebra, then the constraint simply says that the curvature forms of this super -algebra valued differential form are such that their components with incdices in directions perpendicular to in are linear combinations of the components with all indices parallel to .
So if I allowed myself to speak of components of -algebra valued differential forms I’d be done. But I am suspecting that there is a more fundamental way to express what’s going on here, in terms of some general abstract differential cohesion yoga applied to the above diagrams.
And it looks like some kind of formal étaleness condition, or maybe formal smoothness condition on . Hm…
]]>Warning: What follows is just trivia. But since we had related discussion here before, maybe I am excused to waste time with this.
Way back, we (maybe mostly Mike and me) had agreed on symbols for the three modalities of cohesion – – and seemed to have been happy with ever since.
Moreover, in the last months I have been stabilizing myself on writing and for the reduction modality and the infinitesimal flat modality of differential cohesion. The choice of works really well, I think, both with the “re” in “reduction” as well as with the intuitive meaning that the reduced types are what is real about a formal geometry. This suggests to use for one of the other two. It doesn’t really seem to work for the infinitesimal shape, but using it for infinitesimal flat seems okay.
In any case, that leaves the infinitesimal shape modality in need of a good symbol.
Originally (and still on several Lab pages) I had denoted it , alluding to the fact that it produces “infinitesimal path -groupoids”. I still think that’s a great way to think about it, but since finite shape has come to be called and also since now the other two differential modalities don’t carry an -subscript anymore, it feels a bit anachronistic now.
Better would be one single nice symbol for infinitesimal shape. Which one?
One idea I have is this: the modal types of infinitesimal shape in the slice over are precisely the (formally) étale types over . Maybe there is a nice 1-symbol reflection of “étale”.
And there is, of sorts: a ligature of the two letters “et” is what became “&”. Aren’t there also some other versions of a ligature of “et” somewhere in the common TeX collection of symbols?
]]>created little entries
Pi modality flat modality sharp modality
for completeness. The first one redirects to what used to be called Pi-closed morphism, but which should be generalized a bit.
[edit: later we renamed the “Pi modality” to shape modality ]
]]>Given a differential cohesive topos , then for each object there is the jet comonad , which is a right adjoint (to the infinitesimal disk bundle operator). Therefore by this proposition its Eilenberg-Moore category of coalgebras is itself a topos, over .
Question 1: is the topos cohesive, if is?
Actually, that seems unlikely due to the dependency on . Reminds one of the tangent topos construction. Therefore:
Question 2: Do the toposes as ranges over maybe glue into one big topos? If so, is that cohesive if is?
This question is motivated from discussion of variational calculus here.
(Incidentally, by Marvan 86 we have that is the category of partial differential equations with variables in .)
]]>The cohomology of a Lie algebra is by definition that of its Chevalley–Eilenberg complex, . It’s fairly straightforward to see that this cdga can also be obtained as the -invariant differential forms on , for any Lie group integrating :
(where the -action on forms is given by pullback along the multiplication map).
It occurred to me that this should be expressible in the language of smooth sets. First of all we have , and the -action is now given by precomposition. This means that instead of taking -invariants of the hom-set we could just map out of . But this clearly doesn’t recover .
For a moment I thought that maybe the issue is that I’m forgetting the cohesiveness of the group here: so really, I should be looking at an internal hom , and this carries a -action which is witnessed by having it as the fiber of some object (its (homotopy) quotient) over . After all, in the previous paragraph I was asking a smooth group to act on a discrete set, which should be a no-no.
But this would come from looking at internal hom in of into (which classifies the trivial action of on ). And so once again we see appearing, which even speaking cohesively is just the terminal object. So this doesn’t fix the problem either.
Does anyone see what I’m doing wrong here?
]]>I am currently writing an article as follows:
Classical field theory via higher differential geometry
Abstract We discuss here how the refined formulation of classical mechanics/classical field theory (Hamiltonian mechanics, Lagrangian mechanics) that systematically takes all global effects properly into account – such as notably non-perturbative effects, classical anomalies and the definition of and the descent to reduced phase spaces – naturally is a formulation in “higher differential geometry”. This is the context where smooth manifolds are allowed to be generalized first to smooth orbifolds and then further to Lie groupoids, then further to smooth groupoids and smooth moduli stacks and finally to smooth higher groupoids forming a higher topos for higher differential geometry. We introduce and explain this higher differential geometry as we go along. At the same time as we go along, we explain how the classical concepts of classical mechanics all follow naturally from just the abstract theory of “correspondences in higher slice toposes”.
This text is meant to serve the triple purpose of being an exposition of classical mechanics for homotopy type theorists, being an exposition of geometric homotopy theory for physicists, and finally to serve as the canonical example for and seamlessley lead over to the formulation of a local prequantum field theory which supports a localized quantization to local quantum field theory in the sense of the cobordism hypothesis.
This started out as a motivational subsection of Local prequantum field theory (schreiber) and as the nLab page prequantized Lagrangian correspondences, but for various reasons it seems worthwhile to have this as a standalone exposition and as a pdf file.
I am still working on it. Section 1 and two have already most of the content which they are supposed to have, need more polishing, but should be readable. Section 3 is currently just piecemeal, to be ignored for the moment.
]]>started
and for inclusion under “Related concepts”
]]>I am back to working on geometry of physics. I’ll be out-sourcing new paragraphs there to their own Lab entries as much as possible (because the length of the page makes saving and hence previewing it take many minutes, so I need to work in smaller sub-entries and then copy-and-paste).
In this context I now started an entry prequantum field theory. To be further expanded.
This comes with a table of related concepts extended prequantum field theory - table:
extended prequantum field theory
transgression to dimension | |
---|---|
extended Lagrangian, universal characteristic map | |
(off-shell) prequantum (n-k)-bundle | |
(off-shell) prequantum circle bundle | |
action functional = prequantum 0-bundle |
Meanwhile I have a good idea of how to give an elementary formalization, in terms of differential cohesion, of some of the key concepts in the formulation of local Lagrangian field theory on jets of field bundles. In particular I know that given a local Lagrangian then its homotopy stabilizer under , equivalently: its quantomorphism n-group, is the group of symmetries and their higher conserved currents…
…only that this is true only with some extra restrictions. If is a field fiber so that is a WZW term, then it is true, but then the symmetries are just “point symmetries”. This is interesting enough in itself and I used to be content with this, but it is not the full story.
More generally, when is the jet bundle of a field bundle, then the quantomorphisms of , which are diagrams of the form
should be constrained:
should be evolutionary;
should be horizontal.
Question: How may one impose these conditions by general abstract means, using differential cohesion and the jet comonad structure?
I suppose one should demand some kind of factorization through some universal maps of the (co-)monad, but I still don’t really see it.
]]>A thought:
With a higher connection on some group , then there is the elementary concept (in differential cohesive HoTT) of a first-order integrable definite globalization of over some -manifold . This comes with an -functor from such definite globalizations to -structures, on , for the restriction to the infinitesimal disk .
When realized in the supergeometric model and with and the GS-WZW term of the M2-brane, then this -functor lands in the solutions of 11d supergravity with vanishing gravitino field strength and equipped with a genuine globalization of the M2 WZW term. So this means we may take the space of these definite globalizations as being the actual phase space of 11d SuGra. (Details are still here.)
An interesting question to ask then is which of the symmetries of covering carry over to , i.e. which common subgroups there are of and . In the above situation this means asking for BPS states of 11-d supergravity, namely spacetimes equipped with field configurations satisfying the SuGra equations of motion such that there are super-Killing vectors.
]]>I’m trying to prove the analytic Markov’s principle “synthetically” in classical real-cohesion. The proof I know that it holds in a topological model goes by way of the following two statements:
If is a locale, write for the object of points of in a topos , so for instance if is the locale of real numbers then is the Dedekind real numbers object in . Then if is a spatial locale and is a subspace, then is relatively codiscrete. In particular, taking and , we find that strict inequality of real numbers is relatively codiscrete, hence (over a classical base with ) -closed, which is AMP.
If is an object of the site of , then the slice topos admits a local geometric morphism to a spatial localic topos . Since local geometric morphisms are left orthogonal to grouplike ones, including locales, it follows that sections , i.e. maps , i.e. geometric morphisms , are equivalently continuous maps . Moreover, since and are spatial, such a map is just a map of sets with the property of being continuous. And since is a subspace of , continuous maps are just continuous maps that happen to factor through as a map of sets. This gives the relative codiscreteness in the previous claim.
Now I’m trying to extract from one or the other of these statements something that can be proven from categorical adjoint-functor properties like the others that we see in cohesion (plus, perhaps, classicality properties of the base topos). The second one is a standard sort of “big topos” property, but it seems sort of orthogonal to the other kind of “big topos” properties that a cohesive topos has (locality, stable/punctual local connectedness, etc.). Anyone have thoughts?
]]>I have added the statement of lemmas 4.1, 4.2 of Menni-Lawvere to cohesive topos here and to points-to-pieces transform here.
]]>