$\,$
This page collects material related to this thesis that I once advised:
Formalizing Cartan Geometry in Modal Homotopy Type Theory
PhD Thesis, KIT 2017
(thesis pdf, archived version: web, talk slides: pdf, preprint version: arXiv:1806.05966, HoTT-Agda code: DCHoTT-Agda.
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 shape” modality $\Im$. For $X$ any homotopy type then the standard interpretation of the type $\Im X$ is the result of “identifying infinitesimally close points in $X$”.
(By synthetic PDE theory (Khavkine-Schreiber 17) the dependent types over $\Im X$ have the interpretation of being partial differential equations with free variables ranging in $X$. The linear dependent types over $\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 $X$ (Schreiber 13).
The main theorem of the thesis shows that the infinitesimal disk bundle of any such manifold $X$ 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 $X$ with torsion-free G-structure means to equip $X$ with a flavor of geometry, depending on the choice of $G$, such as (pseudo-)Riemannian geometry, conformal geometry, complex geometry, symplectic geometry etc. pp. The moduli stacks of all given $G$-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) $G$-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 exposition see
and tutorial 6 in:
Dan Licata, Felix Wellen, Synthetic Mathematics in Modal Dependent Type Theories, tutorial at Types, Homotopy Theory and Verification, 2018
Tutorial 1, Dan Licata: A Fibrational Framework for Modal Simple Type Theories (recording)
Tutorial 2, Felix Wellen: The Shape Modality in Real cohesive HoTT and Covering Spaces (recording)
Tutorial 3, Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT (recording)
Tutorial 4, Felix Wellen, Discrete and Codiscrete Modalities in Cohesive HoTT, II (recording)
Tutorial 5, Dan Licata: A Fibrational Framework for Modal Dependent Type Theories (recording)
Tutorial 6, Felix Wellen: Differential Cohesive HoTT, (recording)
slides:
Dan Licata, Synthetic Mathematics in Modal Dependent Type Theories, notes for tutorial at Types, Homotopy Theory and Verification, 2018 (pdf)
also
$\,$
For more exposition see also at Formalizing Cartan Geometry in Modal HoTT and at geometry of physics – manifolds and orbifolds.
For more higher differential geometry-background see
For further development concerning jet bundles and PDEs, see
$\,$
$\,$
Last revised on April 6, 2019 at 17:08:44. See the history of this page for a list of all contributions to it.