As some of you might remember, back in 2015 at the meeting of the german mathematical society in Hamburg, Urs Schreiber presented three problems or “exercises” as he called it back then. There is a page about that on the nLab, if you want to know more. In this post, I will sketch a solution to some part of the first of these problems, while the occasion of writing it is a new version of my article about this, which now comes with a long introduction.
Urs Schreiber’s problems were all about formalizing results in higher differential geometry, that make also sense in the quite abstract setting of differential cohesive toposes and cohesive toposes.
A differential cohesive topos is a topos with some extra structure given by three monads and three comonads with some nice properties and adjunctions between them. There is some work concerned with having this structure in homotopy type theory. A specialized cohesive homotopy type theory concerned with three of the six (co-)monads, called real-cohesive homotopy type theory was introduced by Mike Shulman.
What I want to sketch here today is concerned only with one of the monads of differential cohesion. I will call this monad coreduction and denote it with . By the axioms of differential cohesion, it has a left and a right adjoint and is idempotent. These properties are more than enough to model a monadic modality in homotopy type theory. Monadic modalities were already defined at the end of section 7 in the HoTT-Book and named just “modalities” and it is possible to have a homotopy type theory with a monadic modality just by adding some axioms — which is known not to work for non-trivial comonadic modalities.
So let us assume that is a monadic modality in HoTT. That means that we have a map and a unit
such that a property holds, that I won’t really go into in this post — but here it is for completeness: For any dependent type on some type , such that the unit maps are equivalences for all , the map
is an equivalence. So the inverse to this map is an induction principle, that only holds for dependent types subject to the condition above.
The n-truncations and double negation are examples of monadic modalities.
At this point (or earlier), one might ask: “Where is the differential geometry”? The answer is that in this setting, all types carry differential geometric structure that is accessible via and . This makes sense if we think of some very special interpretations of and (and HoTT), where the unit is given as the quotient map from a space to its quotient by a relation that identifies infinitesimally close points in .
Since we have this abstract monadic modality, we can turn this around and define the notion of two points being infinitesimally close, denoted “” in terms of the units:
where “” denotes the identity type (of in this case). The collection of all points y in a type X that are infinitesimally close to a fixed x in X, is called the formal disk at x. Let us denote it with :
Using some basic properties of monadic modalities, one can show, that any map preserves inifinitesimal closeness, i.e.
is inhabited. For any x in A, we can use this to get a map
which behaves a lot like the differential of a smooth function. For example, the chain rule holds
and if f is an equivalence, all induced are also equivalences. The latter corresponds to the fact that the differential of a diffeomorphism is invertible.
If we have a 0-group G with unit e, the left tranlations are a family of equivalences that consistently identify with all other formal disks in G given by the differentials .
This is essentially a generalization of the fact, that the tangent bundle of a Lie-group is trivialized by left translations and a solution to the first part of the first of Urs Schreiber’s problems I mentioned in the beginning.
With the exception of the chain rule, all of this was in my dissertation, which I defended in 2017. A couple of month ago, I wrote an article about this and put it on the arxiv and since monday, there is an improved version with an introduction that explains what monads you can think of and relates the setup to Synthetic Differential Geometry.
There is also a recording on youtube of a talk I gave about this in Bonn.