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.

Differential Geometry in Modal HoTT

Differential Geometry in Modal HoTT

Recommend

Impredicative Encodings, Part 3

HoTT 2019 Call for Submissions

Geometry in Modal HoTT now on Zoom

Introduction to Univalent Foundations of Mathematics with Agda

The Cantor-Schröder-Bernstein Theorem for ∞-groupoids

William Lawvere

Peter J. Freyd

Isabelle

So Long, and Thanks for All the Fish

人人都能做视频赚钱引流两不误千年来赚钱最快的方法

About Joyk