thesis Wellen


This page collects material related to this thesis that I once advised:

on higher Cartan geometry formalized in modal homotopy type theory.


This thesis implements a fragment of the axioms of differential cohesion (Schreiber 13) for synthetic differential geometry, formalized in homotopy type theory and implemented in the Agda proof management system:

A modal operator is introduced (see Schreiber 15 for exposition) which is interpreted as an “infinitesimal shapemodality \Im. For XX any homotopy type then the standard interpretation of the type X\Im X is the result of “identifying infinitesimally close points in XX”.

(By synthetic PDE theory (Khavkine-Schreiber 17) the dependent types over X\Im X have the interpretation of being partial differential equations with free variables ranging in XX. The linear dependent types over X\Im X are also known as D-modules, as used in geometric representation theory.)

Using this infinitesimal shape modality \Im the thesis presents a formalization of the concept of manifold in the type theory. Via the homotopy theoretic interpretation of the type theory the interpretation of such “manifold types” is really as étale ∞-stacks XX (Schreiber 13).

The main theorem of the thesis shows that the infinitesimal disk bundle of any such manifold XX is a fiber ∞-bundle which is associated to a principal ∞-bundle (Nikolaus-Schreiber-Stevenson 12): its frame bundle.

This solves the first of the three problems in modal type theory that had been posed in

Classically, the concept of frame bundle is the foundation of all genuine geometry, via Cartan geometry: Equipping the frame bundle of a manifold XX with torsion-free G-structure means to equip XX with a flavor of geometry, depending on the choice of GG, such as (pseudo-)Riemannian geometry, conformal geometry, complex geometry, symplectic geometry etc. pp. The moduli stacks of all given GG-structures on a given manifold are of central interest in the classical theory, such as the moduli stacks of complex structures, or the moduli stacks of conformal structures.

In order to lift classical Cartan geometry from classical manifolds to higher Cartan geometry on étale ∞-stacks, the thesis closes by formalizing the concept of torsion-free G-structure on manifold types. Due to the homotopy-theoretic interpretation this is really a formalization of higher (∞-group) GG-structures on étale ∞-stacks, including also examples such as string structures or Fivebrane structures.
Finally the thesis demonstrates the construction of the (higher) moduli stacks of such torsion-free G-structures

For more exposition see also at Formalizing Cartan Geometry in Modal HoTT.

For further development concerning jet bundles and PDEs, see



Revised on October 9, 2017 08:43:36 by Urs Schreiber (