Differential Geometry in Modal HoTT

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 $\Im$ . 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 $\Im$ is a monadic modality in HoTT. That means that we have a map $\Im:\mathcal U\to \mathcal U$ and a unit

$\iota:\prod_{X:\mathcal U} X\to \Im X$

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 $E:\Im X\to\mathcal U$ on some type $X$ , such that the unit maps $\iota_{E(x)}$ are equivalences for all $x:X$ , the map

$\_\circ\iota_X:\left(\prod_{x:\Im X}E(x)\right)\to\prod_{x:X}E(\iota_X(x))$

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 $\Im$ and $\iota$ . This makes sense if we think of some very special interpretations of $\Im$ and $\iota$ (and HoTT), where the unit $\iota_X$ is given as the quotient map from a space $X$ to its quotient $\Im X$ by a relation that identifies infinitesimally close points in $X$ .
Since we have this abstract monadic modality, we can turn this around and define the notion of two points $x,y:X$ being infinitesimally close, denoted “ $x\sim y$ ” in terms of the units:

$(x\sim y) :\equiv (\iota_X(x)=\iota_X(y))$

where “ $\_=\_$ ” denotes the identity type (of $\Im X$ 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 $D_x$ :

$D_x:\equiv \sum_{y:X}y\sim x$

Using some basic properties of monadic modalities, one can show, that any map $f:X\to Y$ preserves inifinitesimal closeness, i.e.

$\prod_{x,y:X}(x\sim y)\to (f(x)\sim f(y))$

is inhabited. For any x in A, we can use this to get a map

$df_x:D_x\to D_{f(x)}$

which behaves a lot like the differential of a smooth function. For example, the chain rule holds

$d(f\circ g)_x = df_{g(x)}\circ dg_x$

and if f is an equivalence, all induced $df_x$ 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 $g\cdot\_:\equiv x\mapsto g\cdot x$ are a family of equivalences that consistently identify $D_e$ with all other formal disks $D_x$ in G given by the differentials $d(g\cdot\_)_e$ .
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 $\Im$ 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.

This entry was posted in Uncategorized. Bookmark the permalink.

8 Responses to Differential Geometry in Modal HoTT

David Corfield says:

23 August 2018 at 14:06

Could your results work for a modality corresponding to germs rather than jets? Borisov and Kreminzer are looking to contract at infinity-nilpotent neighbourhoods: https://nforum.ncatlab.org/discussion/2523/jet-bundle/?Focus=66961#Comment_66961

- fwellen says:
  
  23 August 2018 at 15:28
  
  Thanks for pointing out the work of Borisov and Kreminzer! I wasn’t aware of it.
  Short answer: The results work for any (monadic) modality and this seems to be one – at least on presheaves.
  On presheaves $\Im$ is defined by precomposition with reduction and its properties can be derived from the fact that reduction is a coreflection (on affine schemes).
  According to Borisov and Kreminzer, there is a coreflection $R_{\infty}$ on $C^\infty-rings$ and if I guess correctly how they move on, we get a different version of the de Rham space by precomposing presheaves with that coreflection.
  So if we just look at presheaves on $C^\infty-rings$ , you can get a monad $\Im_{\mathrm{germ}}$ that has the same nice abstract properties that $\Im$ has.
  
  - Mike Shulman says:
    
    23 August 2018 at 16:39
    
    Is there a problem with making it work for sheaves too?
    
    - fwellen says:
      
      23 August 2018 at 17:39
      
      It can happen that $\Im$ (=precomposition with the usual reduction) does not preserve sheaves. I’m afraid I don’t have a counterexample. On affine schemes with the usual reduction, it is enough to see that covers are preserved by reduction and reduced objects are always covered by reduced objects to show that $\Im$ preserves sheaves. That is true for the Zariski topology and the étale topology. For the Zariski topology (which should be more interesting here), this follows from the algebraic fact, that localizing commutes with reduction. So a possible attempt for a proof would be to show a similar property for the topology on $C^\infty-\mathrm{rings}$ .
      Another approach would be to sheafify after applying $\Im$ , which I never really thought about. Maybe checking that the result is still modal for $\Im$ leads to the similar conditions as above.
      A hint that just sheafifying doesn’t help in general is that $\Im$ is called “de Rham prestack” in contexts where finer topologies are used.
      So my first guess is, that it also works for sheaves. An argument could go like this:
      Without loss of generality a cover consists of subsets that are the non-zeros of a function (don’t know enough about $C^\infty-\mathrm{rings}$ to know if this is ok), i.e. come from localizations maps of the form $R \to R[f^{-1}]$ . Then modding out $\infty$ -nilpotents is (like with reduction) just modding out an ideal, so it commutes with this localization.
      
  - David Corfield says:
    
    24 August 2018 at 01:40
    
    For what it’s worth, the germ of the diagonal idea led to the concept of (tangent) microbundle, as Jim Stasheff remarks https://golem.ph.utexas.edu/category/2007/08/more_on_tangent_categories.html#c011887.
    
- Urs Schreiber says:
  
  27 August 2018 at 05:24
  
  Just to remind us that a germ-scale shape modality should be related to Bunge et al.’s “Synthetic Differential Topology”. I once made a brief note on this in the nLab entry of that title (lower case). But check.
  
  - Felix Wellen says:
    
    27 August 2018 at 09:55
    
    Here is the link to this nLab-page:
    synthetic differential topology
    I looked more closely at the $\infty$ -reduction on $C^\infty-\mathrm{rings}$ . As I understand it, it behaves more like reduction in Algebraic Geometry than the actual reduction on $C^\infty-\mathrm{rings}$ . At least with respect to all the properties of reduction I use in the algebraic world, to show that $\Im$ preserves sheaves. So now, I convinced myself that $\Im_{\mathrm{germ}}$ (induced by $\infty$ -reduction) is a modality, but realized that I don’t really know why $\Im$ (induced by the usual reduction) should be a modality (on $C^\infty-\mathrm{rings}^{\mathrm{op}}$ ).
    
Urs Schreiber says:

9 September 2018 at 09:59

One neat feature of this differentially-cohesive synthetic formulation of V-manifolds is that, due to the ambient homotopy theory, the resulting V-manifolds are in general not plain manifolds, but are orbifolds, in fact may be infinity-orbifolds, usually known as “etale infinity-stacks” (Prop. 6.5.60 in dcct).

In order to reduce this freedom, we may pick a group object G_glob and ask that a given V-manifold X admits a faithful (i.e. 0-truncated) map to B G_glob. This condition ensures that the isotropy groups of X are subgroups of G_glob. If, in the standard model, G_glob is a compact Lie group, this means that X is then constrained to be an orbifold which admits local charts of the form U_i//G_i, where G_i is any discrete subgroup of G_glob (with some 0-type U_i).

We may then consider any other type A equipped with a faithful (0-truncated) map to BG_glob, and consider the function type
H(X,A) := X –> A
in the slice over BG_glob (i.e. as a map of dependent types in context BG_glob). I think this is equivalently the “global equivariant” orbifold cohomology of X with coefficients in the “global space” A, for the underlying family of equivariance groups being that of finite subgroups of G_glob.

I have tried to spell out this last staement at nLab:orbifold cohomology.

This should be pretty interesting.