Discrete differential geometry in homotopy type theory

TL;DR

The work develops a HoTT-based framework for discrete differential geometry by modeling simplicial complexes with higher inductive types and defining principal circle bundles, connections, curvature, and vector fields via pushouts and realizations. It establishes a total-curvature versus total-index relation on oriented 2D complexes, illustrated through an octahedron model of the sphere, and provides a concrete vector-field example with explicit computations. The central contributions include a HoTT-compatible construction of tangent bundles on discrete surfaces, a formalization of flat connections as local trivialisations, and a total-construction theorem linking local geometric data to global invariants, paving the way toward Gauss–Bonnet and Poincaré–Hopf-type results in homotopy type theory. The work also outlines open questions, such as general existence of connections beyond special combinatorial cases and the need for an Euler characteristic analogue within this framework, with potential for formalization and connections to CW-complex approaches in HoTT.

Abstract

Type families on higher inductive types such as pushouts can capture homotopical properties of differential geometric constructions including connections, curvature, and vector fields. We define a class of pushouts based on simplicial complexes, then define principal bundles, connections, and curvature on these. We provide an example of a tangent bundle but do not prove when these must exist. We define vector fields, and the index of a vector field. Our main result is a theorem relating total curvature and total index, a key step to proving the Gauss-Bonnet theorem and the Poincaré-Hopf theorem, but without an existing definition of Euler characteristic to compare them to. We draw inspiration in part from the young field of discrete differential geometry, and in part from the original classical proofs, which often make use of triangulations and other discrete arguments.

Figures (9)

• Figure 1: A path $\pi$ over the path $p$ in the base involves the transport function.
• Figure 2: Transport along $p$ in the fibers of a family of paths. The fiber over $a$ is $\phi(a)=\psi(a)$ where $\phi,\psi:A\to B$.
• Figure 3: The link of $v$ in this complex consists of the vertices $\{a,b,c,d,e,f\}$ and the edges $\{ab,bc,cd,de,ef,fa\}$, forming a hexagon.
• Figure 4: We imagine shrinking $r_{21}$ down to become $\mathsf{refl}_\mathsf{base}$ in $S^1$.
• Figure 5: The Hasse diagram of the simplicial complex $O$, and a possible realization. The row of singletons in the Hasse diagram is $O_0$ and above it are $O_1$ and $O_2$.

Theorems & Definitions (53)

• Definition 2.1
• Lemma 2.2
• Lemma 2.3
• Corollary 2.4
• Definition 2.5
• Definition 2.6
• Theorem 2.7
• Remark 2.8
• Definition 3.1
• Definition 3.2