Synthetic G-jet-structures in modal homotopy type theory

TL;DR

This work embeds a differential-geometric program inside modal homotopy type theory by fixing a monadic modality $\Im$ to encode infinitesimal proximity. It builds formal disks $\mathbb{D}_a$ and the formal disk bundle $T_\infty A$, with a functorial differential $df$ and chain rule, all relative to $\Im$ and its elimination principles. By defining $V$-manifolds and $G$-jet-structures as lifts and moduli problems over classifying spaces $\mathrm{BAut}(\mathbb{D}_e)$, the paper constructs moduli spaces of torsion-free $G$-jet-structures on formal $\mathbb{D}_e$-spaces, with several equivalent fiber-bundle formalisms and stability properties under pullback. The approach yields a concise, formalizable framework that can interpret differential Cartan geometry in arbitrary $\infty$-toposes and supports formal verification in proof assistants, offering a tractable path to synthetic differential geometry and higher-structure moduli computations.

Abstract

This article constructs the moduli stack of torsionfree $G$-jet-structures in homotopy type theory with one monadic modality. This yields a construction of this moduli stack for any $\infty$-topos equipped with any stable factorization systems. In the intended applications of this theory, the factorization systems are given by the deRham-Stack construction. Homotopy type theory allows a formulation of this abstract theory with surprising low complexity. This is witnessed by the accompanying formalization of large parts of this work.

Theorems & Definitions (86)

• Definition 2.1
• Definition 2.2
• Lemma 2.3
• Corollary 2.4
• Proposition 2.6
• Proof 1
• Definition 2.7
• Definition 2.8
• Remark 2.9
• Proposition 2.10