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 $\pi_1(S^1) \simeq \mathbb{Z}$. 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

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*).

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*

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…

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 $n$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 $X$ are constrained to be something like “holomorphic” in the super-direction, in that they are fully determined by their restriction along the inclusion $\Re X \longrightarrow X$ of the underlying ordinary manifold, in (vague? or good?) analogy with how holomorphic functions on $\mathbb{C}$ are determined by their restriction along $\mathbb{R} \hookrightarrow \mathbb{C}$. 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 $X$, modeled on a given extended super-Minkowski spacetime, to have higher super-vielbein fields $E$ which, as super-differential forms on $X$, are rheonomic.

So the statement is something like that a solution to supergravity is nothing but a certain $G$-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 $X$ modeled on a framed space $V$, such as some extended super-Minkowski spacetime, then we are simply looking at an orthogonal structure exhibited by a diagram of the form

$\array{ X && \longrightarrow && \mathbf{B} O(V) \\ & \searrow &\swArrow_{E}& \swarrow \\ && \mathbf{B}GL(V) }$where the homotopy $E$ 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

$\left( \array{ \Re X && \longrightarrow && \mathbf{B} O(V) \\ & \searrow &\swArrow_{\Re E}& \swarrow \\ && \mathbf{B}GL(V) } \right) \;\;\;\; \coloneqq \;\;\;\; \left( \array{ \Re X &\longrightarrow& X && \longrightarrow && \mathbf{B} O(V) \\ && & \searrow &\swArrow_{E}& \swarrow \\ && && \mathbf{B}GL(V) } \right)$So rheonomy is supposed to be some constraint on $E$ that makes it be fully determined by its restriction $\Re E$.

When one expresses $E$ in terms of actual differential forms with values in a super-$L_\infty$-algebra, then the constraint simply says that the curvature forms of this super $L_\infty$-algebra valued differential form are such that their components with incdices in directions perpendicular to $\Re X$ in $X$ are linear combinations of the components with all indices parallel to $X$.

So if I allowed myself to speak of components of $L_\infty$-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 $E$. 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 – $ʃ, \flat, \sharp$ – and seemed to have been happy with ever since.

Moreover, in the last months I have been stabilizing myself on writing $\Re$ and $\Im$ for the reduction modality and the infinitesimal flat modality of differential cohesion. The choice of $\Re$ 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 $\Im$ 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 $n$Lab pages) I had denoted it $\mathbf{\Pi}_{inf}$, alluding to the fact that it produces “infinitesimal path $\infty$-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 ${}_{inf}$-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 $X$ are precisely the (formally) *étale* types over $X$. 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 $\dashv$ flat modality $\dashv$ 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 $\mathbf{H}$, then for each object $X \in \mathbf{H}$ there is the jet comonad $Jet_X \colon \mathbf{H}_{/X} \to \mathbf{H}_{/X}$, which is a right adjoint (to the infinitesimal disk bundle operator). Therefore by this proposition its Eilenberg-Moore category of coalgebras $EM(Jet_X)$ is itself a topos, over $\mathbf{H}_{/X}$.

**Question 1:** is the topos $EM(Jet_X)$ cohesive, if $\mathbf{H}$ is?

Actually, that seems unlikely due to the dependency on $X$. Reminds one of the tangent topos construction. Therefore:

**Question 2:** Do the toposes $EM(Jet_X)$ as $X$ ranges over $\mathbf{H}$ maybe glue into one big topos? If so, is *that* cohesive if $\mathbf{H}$ is?

This question is motivated from discussion of variational calculus here.

(Incidentally, by Marvan 86 we have that $EM(Jet_X) = PDE(X)$ is the category of partial differential equations with variables in $X$.)

]]>The cohomology of a Lie algebra $g$ is by definition that of its Chevalley–Eilenberg complex, $CE^*(g)$. It’s fairly straightforward to see that this cdga can also be obtained as the $G$-invariant differential forms on $G$, for any Lie group $G$ integrating $g$:

$CE^*(g) \cong \Omega^*(G)^G$(where the $G$-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 $\Omega^k(G) = hom_{SmthSet}(G,\Omega^k)$, and the $G$-action is now given by precomposition. This means that instead of taking $G$-invariants of the hom-set we could just map out of $G/G = pt$. But this clearly doesn’t recover $CE^k(g)$.

For a moment I thought that maybe the issue is that I’m forgetting the cohesiveness of the group $G$ here: so really, I should be looking at an internal hom $[G,\Omega^k]$, and this carries a $G$-action which is witnessed by having it as the fiber of some object (its (homotopy) quotient) over $\mathbf{B}G$. 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 ${\mathbf H}_{/{\mathbf B}G}$ of $G/G$ into $\Omega^k \times {\mathbf B}G$ (which classifies the trivial action of $G$ on $\Omega^k$). And so once again we see $G/G$ 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*

AbstractWe 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 $n$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**

$0 \leq k \leq n$ | transgression to dimension $k$ |
---|---|

$0$ | extended Lagrangian, universal characteristic map |

$k$ | (off-shell) prequantum (n-k)-bundle |

$n-1$ | (off-shell) prequantum circle bundle |

$n$ | 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 $\mathbf{L} \colon E \to \mathbf{B}^n U(1)_{conn}$ then its homotopy stabilizer under $\mathbf{Aut}(E)$, 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 $E$ is a field fiber so that $\mathbf{L}$ 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 $E = Jet(F)$ is the jet bundle of a field bundle, then the quantomorphisms of $\mathbf{L}$, which are diagrams of the form

$\array{ Jet(F) && \underoverset{\simeq}{\phi}{\longrightarrow} && Jet(F) \\ & {}_{\mathllap{\mathbf{L}}}\searrow &\swArrow^{\eta}_{\mathrlap{\simeq}}& \swarrow_{\mathrlap{\mathbf{L}}} \\ && \mathbf{B}^n U(1)_{conn} }$should be constrained:

$\phi$ should be evolutionary;

$\eta$ 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 $\mathbf{L}_{WZW}$ a higher connection on some group $V$, then there is the elementary concept (in differential cohesive HoTT) of a first-order integrable definite globalization $\mathbf{L}_{WZW}^X$ of $\mathbf{L}_{WZW}$ over some $V$-manifold $X$. This comes with an $\infty$-functor from such definite globalizations to $\mathrm{Stab}(\mathbf{L}_{WZW}^{inf})$-structures, on $X$, for $\mathbf{L}_{\mathrm{WZW}}^{inf}$ the restriction to the infinitesimal disk $\mathbb{D}^V \to V$.

When realized in the supergeometric model and with $V = \mathbb{R}^{10,1|N=1}$ and $\mathbf{L}_{\mathrm{WZW}} = \mathbf{L}_{M2}$ the GS-WZW term of the M2-brane, then this $\infty$-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 $\mathbf{L}_{WZW}^{inf}$ covering $V$ carry over to $\mathbf{L}_{WZW}^X$, i.e. which common subgroups $Q$ there are of $Heis(\mathbf{L}_{WZW}) \coloneqq Stab_{V}(\mathbf{L}_{WZW})$ and $QuantMorph(\mathbf{L}_{\mathrm{WZW}}^X) \coloneqq Stab_{Aut(X)}(\mathbf{L}_{WZW}^X)$. In the above situation this means asking for *BPS states* of 11-d supergravity, namely spacetimes $X$ 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 $X$ is a locale, write $X_E$ for the object of points of $X$ in a topos $E$, so for instance if $R$ is the locale of real numbers then $R_E$ is the Dedekind real numbers object in $E$. Then if $X$ is a spatial $T_U$ locale and $Y$ is a subspace, then $Y_E\to X_E$ is relatively codiscrete. In particular, taking $X=R$ and $Y=R_{\gt 0}$, we find that strict inequality of real numbers is relatively codiscrete, hence (over a classical base with $\sharp0=0$) $\neg\neg$-closed, which is AMP.

If $U$ is an object of the site of $E$, then the slice topos $E/U$ admits a local geometric morphism to a

*spatial*localic topos $Sh(L_U)$. Since local geometric morphisms are left orthogonal to grouplike ones, including $T_U$ locales, it follows that sections $X_E(U)$, i.e. maps $U\to X_E$, i.e. geometric morphisms $E/U \to X$, are equivalently continuous maps $L_U\to X$. Moreover, since $X$ and $L_U$ are spatial, such a map is just a map of sets $(L_U)_0 \to X_0$ with the property of being continuous. And since $Y$ is a subspace of $X$, continuous maps $L_U\to Y$ are just continuous maps $L_U\to X$ that happen to factor through $Y$ 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.

In two recent threads [1, 2] I had started to look into elementary formalization of the following obstruction problem in higher geometry:

given

a Klein geometry $H \to G$,

a WZW term $\mathbf{L}_{WZW} : G/H \longrightarrow \mathbf{B}^{p+1} \mathbb{G}_{conn}$;

a Cartan geometry $X$ modeled on $G/H$

then:

- what is the obstruction to globalizing the WZW term to $X$?

Here are first concrete observations, holding in any elementary $\infty$-topos (meaning: this may be proven using HoTT, not needing simplicial or other infinite diagrams):

First, a lemma that turns the datum of a global WZW term $Fr(X) \longrightarrow \mathbf{B}^{p+1}\mathbb{G}_{conn}$ on the frame bundle of $X$ (each of whose fibers looks like the formal disk $\mathbb{D}$ around the base point, or any other point, in $G/H$) into something closer to cohomological data on $X$. In the following $Fr(X)$ may be any fiber bundle $E$ and $\mathbf{B}^{p+1}\mathbb{G}_{conn}$ may be any coefficient object $A$.

**Lemma.** Let $E \to X$ be an $F$-fiber bundle associated to an $Aut(F)$-principal bundle $P \to X$. Then $A$-valued functions on $E$ are equivalent to sections of the $[F,A]$-fiber bundle canonically associated to $P$.

**Proof.** By the discussion at *infinity-action*, the universal $[F,A]$-fiber bundle $[F,A]/Aut(F)\to \mathbf{B} Aut(F)$ is simply the function space $[F,A]_{\mathbf{B} Aut(F)}$ formed in the slice over $\mathbf{B} Aut(F)$, with $F$ regarded with its canonical $Aut(F)$-action and $A$ regarded with the trivial $Aut(F)$-action.

Now, by universality, sections of $P \underset{Aut(F)}{\times} [F,A] \to X$ are equivalently diagonal maps in

$\array{ && [F,A]/Aut(F) \\ & \nearrow & \downarrow \\ X & \longrightarrow & \mathbf{B} Aut(F) }$But by Cartesian closure in the slice and using the above, these are equivalent to horizontal maps in

$\array{ E & = & P \underset{Aut(F)}{\times} F && \longrightarrow && A \times \mathbf{B}Aut(F) \\ && & \searrow && \swarrow \\ && && \mathbf{B}Aut(F) }$Finally by $(\underset{\mathbf{B}Aut(F)}{\sum} \dashv \mathbf{B}Aut(F)^\ast)$ this is equivalent to maps $E \to A$. $\Box$

$\,$

[ continued in next comment ]

]]>am working on a new chapter of the *geometry of physics* cluster:

Still a bit rough towards the end, but I need a break now.

In the course of this I started splitting off a further chapter *geometry of physics – prequantum geometry*, but that’s rudimentary at the moment.

I have been writing about synthetic formalization of (super-)Einstein equations of motion in various talk notes scattered around, (such recently at *Modern Physics formalized in Modal Homotopy Type Theory (schreiber)*) but now it is maybe time to turn it into a polished comprehensive account.

It would seem that I should be doing this in a separate document, but since the proof depends on a fairly wide range of chapters in cohesion, I have been typing it now right into the big file. A first version is now in section 7.1.3 “Gravity” of the dcct pdf. This needs polishing, but that’s where it is for the moment.

]]>