Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2504.20363 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910921670000640 |
|---|---|
| author | Langmead, Greg |
| author_facet | Langmead, Greg |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_20363 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Discrete differential geometry in homotopy type theory Langmead, Greg Category Theory Differential Geometry 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. |
| title | Discrete differential geometry in homotopy type theory |
| topic | Category Theory Differential Geometry |
| url | https://arxiv.org/abs/2504.20363 |