Relationship between synthetic differential geometry and differential cohesion?

I'm a big fan of synthetic differential geometry (or smooth infinitesimal analysis), as developed by Anders Kock and Bill Lawvere. It's a beautiful and intuitive geometric theory, which gives justification for the infinitesimal methods used by many of the pioneers of analysis and differential geometry, like Sophus Lie.

I have also occasionally come across the notion of differential cohesion, which seems to be another sort of synthetic approach to differential geometry. Unfortunately, while I'm pretty comfortable with 1-category theory, I don't know much homotopy theory or higher category theory, so the language used is pretty foreign to me. There is also a lot of talk of modalities, which I don't really have any intuition for.

Question: What is the relationship between differential cohesion and synthetic differential geometry (in the sense of Kock & Lawvere)?

• There's no relation a priori. Synthetic means that there's an infinitesimal line, while cohesion means some additional geometric enrichment (like differentiability, analyticity etc). And you don't have to know higher category theory to know the definition of a cohesive topos (take a look at Lawvere papers). See for instance the references in ncatlab.org/nlab/show/cohesive+topos. In the 1-categorial case, the differential cohesion is just that bunch of adjoints for the topos of sheaves over cartesian spaces. In this case, the modalities aren't that interesting though. – user40276 Aug 17 '17 at 7:56
• user40276, why do you say that modaltities for differential cohesion are not that interesting? E.g. hott-uf.github.io/2017/abstracts/cohesivett.pdf – Bas Spitters Aug 18 '17 at 6:30
• @BasSpitters Well, differential cohesion in my opinion really shines in the infinity setting. My problem is not only with the modalities (although the non-existence of an infinitesimal path groupoid really bothers me). It's not like the 1-categorical case is not relevant, it's just not useful for what interests me (for instance, I can't integrate Lie stuff, pick deloopings etc). Of course, this is pretty subjective. I just don't like MLETT. Maybe I should have only said that it's not interesting for my applications..... – user40276 Aug 22 '17 at 20:29
• ... Or maybe I should have said nothing. Dunno, I like to say things. By the way, can one in any differential cohesion speak about parallel transport in any G-bundle (G an internal group)? This would change my mind a little. – user40276 Aug 22 '17 at 20:29
• user40276 One can speak about higher parallel transport for connections on ∞-bundles, ncatlab.org/nlab/show/higher+parallel+transport. Since his name hasn't been mentioned yet, let me point out just how much of all this work on cohesion and differential cohesion in ∞-toposes is due to Urs Schreiber. His book is well worth perusing, ncatlab.org/schreiber/show/…. – David Corfield Sep 4 '17 at 7:37

I'm a co-author on the abstract linked in the comments but I'm coming from the computer science side so I'm not an expert on the models and I know very little classical differential geometry.

I had the same question and my current understanding is that

1. Differential Cohesion and Synthetic Differential Geometry have the same "canonical model": the SDG people use the Cahiers topos and Diff Cohesion people use the $\infty$-sheaves on the same site.

2. They are by no means equivalent: for instance Synthetic Differential Geometry axiomatizes a real line object $R$ and the Kock-Lawvere axiom uses it, whereas in differential cohesion the notion of "infinitesimal" distance is more "formal" in that it is just derived from abstract modalities. For instance there are very simple models of DC like this one that have a very strange notion of "infinitesimally close".

It's a matter of ongoing research how much differential geometry can be done using just differential cohesion, but clearly if you want to get all of the classical theorems you need to at some point axiomatize the reals (unfortunately any internal definition of the reals via Dedekind cuts will give you the wrong reals because you want to only have the smooth functions).

On the other hand Differential Cohesion is more "categorical" which syntactically means we hope to get well-behaved type-theoretic connectives instead of uninterpreted axioms, like how having the identity type in HoTT is much nicer than axiomatizing the n-spheres.

The main source for what can be formalized in (solid, differential) cohesion is Urs' book, look for the sections on the differential cohesion modalities to see some comparisons to SDG, but also note that much of that book can be formalized with just a cohesive topos.

For some shorter/simpler examples, see Felix Wellen's thesis if you want to see what some of differential geometry looks like using just one of the modalities from differential cohesion. Also maybe check out Mike Shulman's paper for (non-differential) cohesion plus some axioms for a more hybrid style.

Also, when it comes to the infinity-stuff, I have been assured by experts that you can just ignore the word infinity when you are looking for intuition. A big takeaway from infinity-category theory and Homotopy Type Theory is that infinity groupoids act a lot like sets.

• any internal definition of the reals via Dedekind cuts will give you the wrong reals because you want to only have the smooth functions it might be worth pointing out that Dedekind cuts defined internally give all continuous functions. – David Roberts Aug 24 '17 at 23:23
• As for how much (higher) differential geometry can be done, take a look at section 5.3 of ncatlab.org/schreiber/show/…. Section 4.2 also remarks: "A well-known proposal for an axiomatic characterization of infinitesimal objects in a 1-topos goes by the name synthetic differential geometry, where infinitesimal extension is characterized by algebraic properties of dual function algebras, as above. From the point of view and in the presence of cohesion in an ∞-topos, however, there is a more immediate geometric characterization" – David Corfield Sep 4 '17 at 7:08