Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Classification of Covering Spaces and Canonical Change of Basepoint

Jelle Wemmenhove, Cosmin Manea, Jim Portegies

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.

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.
Paper Structure (16 sections, 15 theorems, 22 equations)

This paper contains 16 sections, 15 theorems, 22 equations.

Table of Contents

  1. Introduction
  2. Background
  3. Topological interpretation
  4. Spaces, points, paths, and higher paths
  5. Type families, transport, and dependent paths
  6. Truncations and path-connectedness
  7. Loop spaces and homotopy groups
  8. Dealing with truncations
  9. Notation
  10. Classification of covering spaces
  11. Covering spaces in HoTT
  12. Lifting criterion
  13. Classification theorem
  14. Canonical change of basepoint
  15. Relation to free pointedness
  16. ...and 1 more sections

Key Result

Lemma 1

Let $P, Q : X \to \mathsf{Type}$ be two type families and let $f_{(\mathord{\space\text{--}\space})}:\prod_x (P(x) \to Q(x))$ be a family of maps, then for all paths $p : a =_X b$ and points $u : P(a)$ it holds that

Theorems & Definitions (21)

  • Remark
  • Lemma 1
  • Lemma 2: Extension by weak constancy, cf. generalization kraus2015weakextension
  • Definition 3: cf. favonia-covspaces
  • Lemma 4: Characterization of equality between pointed covering spaces
  • Definition 5
  • Theorem 6: direct translation, cf. hatcherAT
  • Lemma 7
  • Theorem 8: Lifting criterion, cf. hatcherAT
  • Theorem 9: Classification, cf. hatcherAT
  • ...and 11 more