October 9: Greg Langmead on "Discrete differential geometry in homotopy type theory"
Emily Riehl
The HoTTEST continues this Thursday at 11:30 AM EDT (UTC-4) / 15:30 UTC with:
Greg Langmead
whose talk is titled “Discrete differential geometry in homotopy type theory”.
The talk will be 60 minutes long, followed by up to 30 minutes for questions. The abstract is below.
More details can be found on our new website
https://hottest-seminar.github.io/
thanks to Zack Dooley, where you can find further information about the HoTTEST seminar, including the rest of our lineup for Fall 2025, and videos and slides from past talks. (Please let us know if you encounter any issues with
the website.)
See you this Thursday on Zoom: https://zoom.us/j/994874377
Emily
(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.)
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.
--
Kelly Miller Professor of Mathematics (she/her)
Johns Hopkins University
emilyriehl.github.io
Dan Christensen
Axel Ljungström
A formalisation of the Serre finiteness theorem
The talk is at 11:30am EDT (15:30 UTC) on Thursday, October 23. The
all upcoming talks.
All are welcome!
Abstract:
The central claim of the Serre finiteness theorem is that homotopy groups of spheres are finitely presented. Remarkably, this theorem can be proved constructively in HoTT. A particular consequence of this is that we get a completely synthetic proof of Brown's result that we, at least in theory, can compute (in the computer scientist's sense of the word) any homotopy group of any sphere! The HoTT proof of the Serre finiteness theorem, which is due to Barton and Campion, quickly inspired the launching of a rather extensive formalisation project, with the end-goal of verifying Barton and Campion's proof in Cubical Agda. About a month ago, this formalisation was finally completed.
In this talk, I'll give a rough outline of the Barton and Campion's proof. In my presentation, I will try to follow the timeline of the formalisation project and emphasise whenever the formalisation actually ended up leading to simplifications of the original pen-and-paper proof. I will also take the opportunity to mention some recent work on CW complexes which turned out to play an important role in both the formalisation and the pen-and-paper proof of the theorem.
This is joint work with Reid Barton, Owen Milner, Anders Mörtberg and Loïc Pujet.