Classification of Covering Spaces and Canonical Change of Basepoint
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914955722227712 |
|---|---|
| author | Wemmenhove, Jelle Manea, Cosmin Portegies, Jim |
| author_facet | Wemmenhove, Jelle Manea, Cosmin Portegies, Jim |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_15351 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Classification of Covering Spaces and Canonical Change of Basepoint Wemmenhove, Jelle Manea, Cosmin Portegies, Jim Algebraic Topology Logic in Computer Science Logic 68V20 F.4.1; I.2.4 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. |
| title | Classification of Covering Spaces and Canonical Change of Basepoint |
| topic | Algebraic Topology Logic in Computer Science Logic 68V20 F.4.1; I.2.4 |
| url | https://arxiv.org/abs/2409.15351 |