Document Open Access Logo

Classification of Covering Spaces and Canonical Change of Basepoint

Authors Jelle Wemmenhove , Cosmin Manea , Jim Portegies

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2023.1.pdf
  • Filesize: 0.86 MB
  • 23 pages

Document Identifiers

Author Details

Jelle Wemmenhove
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Cosmin Manea
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands
Jim Portegies
  • Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands

Cite AsGet BibTex

Jelle Wemmenhove, Cosmin Manea, and Jim Portegies. Classification of Covering Spaces and Canonical Change of Basepoint. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.TYPES.2023.1

Abstract

Using the language of homotopy type theory (HoTT), we 1) prove a synthetic version of the classification theorem for covering spaces, and 2) explore the existence of canonical change-of-basepoint isomorphisms between homotopy groups. There is some freedom in choosing how to translate concepts from classical algebraic topology into HoTT. The final translations we ended up with are easier to work with than the ones we started with. We discuss some earlier attempts to shed light on this translation process. The proofs are mechanized using the Coq proof assistant and closely follow classical treatments like those by Hatcher [Allen Hatcher, 2002].

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Algebraic topology
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • Synthetic Homotopy Theory
  • Homotopy Type Theory
  • Covering Spaces
  • Change-of-Basepoint Isomorphism

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT Library: A Formalization of Homotopy Type Theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pages 164-172, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3018610.3018615.
  2. Guillame Brunerie. On the homotopy groups of spheres in homotopy type theory. PhD thesis, Laboratoire J.A. Dieudonné, August 2016. URL: https://doi.org/10.48550/arXiv.1606.05916.
  3. Ulrik Buchholtz and Kuen-Bang Hou. Cellular Cohomology in Homotopy Type Theory. Logical Methods in Computer Science, Volume 16, Issue 2, June 2020. URL: https://doi.org/10.23638/LMCS-16(2:7)2020.
  4. Ulrik Buchholtz, Floris van Doorn, and Egbert Rijke. Higher Groups in Homotopy Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 205-214, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209150.
  5. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of Higher Truncations. In Stephan Kreutzer, editor, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs, pages 359-373, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2015.359.
  6. Allen Hatcher. Algebraic Topology. Cambridge University Press, 2002. URL: https://pi.math.cornell.edu/~hatcher/AT/ATpage.html.
  7. Kuen-Bang Hou (Favonia). Higher-Dimensional Types in the Mechanization of Homotopy Theory. PhD thesis, Carnegie Mellon University, February 2017. URL: https://favonia.org/thesis.
  8. Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 565-574, 2016. URL: https://doi.org/10.1145/2933575.2934545.
  9. Kuen-Bang Hou (Favonia) and Robert Harper. Covering Spaces in Homotopy Type Theory. In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetić, editors, 22nd International Conference on Types for Proofs and Programs (TYPES 2016), volume 97 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2016.11.
  10. Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen Theorem in Homotopy Type Theory. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 22:1-22:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.22.
  11. Hideyuki Kachi. Homotopy commutativity of the loop space of a finite CW-complex. Hiroshima Mathematical Journal, 20(2):365-384, 1990. URL: https://doi.org/10.32917/hmj/1206129185.
  12. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of Univalent Foundations (after Voevodsky). Journal of European Mathematical Society, 23(6):2071-2126, March 2021. URL: https://doi.org/10.4171/JEMS/1050.
  13. Daniel R. Licata and Guillaume Brunerie. π_n(Sⁿ) in Homotopy Type Theory. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs, pages 1-16, Cham, 2013. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-03545-1_1.
  14. Axel Ljüngstrom and Anders Mörtberg. Formalizing π₄(𝕊³) ≅ ℤ/2ℤ and Computing a Brunerie Number in Cubical Agda. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13, Los Alamitos, CA, USA, June 2023. IEEE Computer Society. URL: https://doi.org/10.1109/LICS56636.2023.10175833.
  15. Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Mathematical Structures in Computer Science, 28(6):856-941, 2018. URL: https://doi.org/10.1017/S0960129517000147.
  16. James Stasheff. On homotopy Abelian H-spaces. Mathematical Proceedings of the Cambridge Philosophical Society, 57(4):734-745, 1961. URL: https://doi.org/10.1017/S0305004100035878.
  17. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  18. Jelle Wemmenhove, Cosmin Manea, and Jim Portegies. Formalization of Classification of Covering Spaces and Canonical Change of Basepoint in HoTT. Software, version 0.3., swhId: https://archive.softwareheritage.org/swh:1:dir:bea0c0af55e3ec9869679f3a5611cc5154a9ddbf;origin=https://gitlab.tue.nl/computer-verified-proofs/covering-spaces;visit=swh:1:snp:6b1d9a68d2f10e958534db29214f30ddd1dd9db3;anchor=swh:1:rev:cfc827a2b07f8cb93b412bd6e551d31fae044fb9 (visited on 2024-07-19). URL: https://gitlab.tue.nl/computer-verified-proofs/covering-spaces.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact