Classification of Covering Spaces and Canonical Change of Basepoint

Jelle Wemmenhove; Cosmin Manea; Jim Portegies

doi:10.4230/LIPIcs.TYPES.2023.1

Classification of Covering Spaces and Canonical Change of Basepoint

Jelle Wemmenhove^*
, Cosmin Manea
, Jim Portegies

^*Corresponding author for this work

Eindhoven University of Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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 [6].

Original language	English
Title of host publication	29th International Conference on Types for Proofs and Programs, TYPES 2023
Editors	Delia Kesner, Eduardo Hermo Reyes, Benno van den Berg
Publisher	Dagstuhl Publishing
ISBN (Electronic)	9783959773324
DOIs	https://doi.org/10.4230/LIPIcs.TYPES.2023.1
Publication status	Published - Aug 2024
Externally published	Yes
Event	29th International Conference on Types for Proofs and Programs, TYPES 2023 - Valencia, Spain Duration: 12 Jun 2023 → 16 Jun 2023

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	303
ISSN (Print)	1868-8969

Conference

Conference	29th International Conference on Types for Proofs and Programs, TYPES 2023
Country/Territory	Spain
City	Valencia
Period	12/06/23 → 16/06/23

Bibliographical note

Publisher Copyright:
© Jelle Wemmenhove, Cosmin Manea, and Jim Portegies.

Keywords

Change-of-Basepoint Isomorphism
Covering Spaces
Homotopy Type Theory
Synthetic Homotopy Theory

Access to Document

10.4230/LIPIcs.TYPES.2023.1Licence: CC BY

Cite this

Wemmenhove, J., Manea, C., & Portegies, J. (2024). Classification of Covering Spaces and Canonical Change of Basepoint. In D. Kesner, E. H. Reyes, & B. van den Berg (Eds.), 29th International Conference on Types for Proofs and Programs, TYPES 2023 Article 1 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 303). Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.TYPES.2023.1

@inproceedings{1675dab1359d433fac23a721bafd9d78,

title = "Classification of Covering Spaces and Canonical Change of Basepoint",

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 [6].",

keywords = "Change-of-Basepoint Isomorphism, Covering Spaces, Homotopy Type Theory, Synthetic Homotopy Theory",

author = "Jelle Wemmenhove and Cosmin Manea and Jim Portegies",

note = "Publisher Copyright: {\textcopyright} Jelle Wemmenhove, Cosmin Manea, and Jim Portegies.; 29th International Conference on Types for Proofs and Programs, TYPES 2023 ; Conference date: 12-06-2023 Through 16-06-2023",

year = "2024",

month = aug,

doi = "10.4230/LIPIcs.TYPES.2023.1",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Dagstuhl Publishing",

editor = "Delia Kesner and Reyes, \{Eduardo Hermo\} and \{van den Berg\}, Benno",

booktitle = "29th International Conference on Types for Proofs and Programs, TYPES 2023",

}

Wemmenhove, J, Manea, C & Portegies, J 2024, Classification of Covering Spaces and Canonical Change of Basepoint. in D Kesner, EH Reyes & B van den Berg (eds), 29th International Conference on Types for Proofs and Programs, TYPES 2023., 1, Leibniz International Proceedings in Informatics, LIPIcs, vol. 303, Dagstuhl Publishing, 29th International Conference on Types for Proofs and Programs, TYPES 2023, Valencia, Spain, 12/06/23. https://doi.org/10.4230/LIPIcs.TYPES.2023.1

Classification of Covering Spaces and Canonical Change of Basepoint. / Wemmenhove, Jelle; Manea, Cosmin; Portegies, Jim.
29th International Conference on Types for Proofs and Programs, TYPES 2023. ed. / Delia Kesner; Eduardo Hermo Reyes; Benno van den Berg. Dagstuhl Publishing, 2024. 1 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 303).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Classification of Covering Spaces and Canonical Change of Basepoint

AU - Wemmenhove, Jelle

AU - Manea, Cosmin

AU - Portegies, Jim

N1 - Publisher Copyright: © Jelle Wemmenhove, Cosmin Manea, and Jim Portegies.

PY - 2024/8

Y1 - 2024/8

N2 - 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 [6].

AB - 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 [6].

KW - Change-of-Basepoint Isomorphism

KW - Covering Spaces

KW - Homotopy Type Theory

KW - Synthetic Homotopy Theory

UR - https://www.scopus.com/pages/publications/85203267058

U2 - 10.4230/LIPIcs.TYPES.2023.1

DO - 10.4230/LIPIcs.TYPES.2023.1

M3 - Conference contribution

AN - SCOPUS:85203267058

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 29th International Conference on Types for Proofs and Programs, TYPES 2023

A2 - Kesner, Delia

A2 - Reyes, Eduardo Hermo

A2 - van den Berg, Benno

PB - Dagstuhl Publishing

T2 - 29th International Conference on Types for Proofs and Programs, TYPES 2023

Y2 - 12 June 2023 through 16 June 2023

ER -

Classification of Covering Spaces and Canonical Change of Basepoint

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this