Covering Space vs Covering Maps

Stream: maths

[Gareth Ma]

In Hatcher a covering space of a space $X$ is defined as follows:

image.png

While in Mathlib, there's the notion of covering maps, but digging through the definitions it seems they are different notions. Are covering spaces defined in Mathlib?

[Adam Topaz]

Are you looking for docs#IsCoveringMap ?

[Adam Topaz]

The def you linked says that a map is a covering map around a point x in the base

[Gareth Ma]

Oh I didn't realise I linked to IsEvenlyConnected insteaed of IsCoveringMap. But it seems different from what Hatcher is defining

[Gareth Ma]

It requires $p^{-1}(\{x\})$ to be discrete whereas in Hatcher it wants $p^{-1}(\{x\})$ to be disjoint union of open sets?

[Gareth Ma]

Sorry if I'm like missing something obvious by the way, my topology is objectively bad :sweat:

[Adam Topaz]

Think of it like this… if X is a topological space and Y is discrete then $X \times Y$ is homeomorphic to a disjoint union of copies of X indexed by Y.

[Adam Topaz]

And Hatcher doesn’t work with the fiber above x, rather above some sufficiently small neighbourhood of x

[Gareth Ma]

Thanks, I will think about it

[Gareth Ma]

Oh right in Hatcher it's $p^{-1}(U_{\alpha})$ for one of the covering sets $U_{\alpha}$, instead of just $\{x\}$ which is what you're saying

[Gareth Ma]

Oh okay I get it now. So take the covering map $p : \mathbb{R} \to \mathbb{S}^1$ where $p(t) = (\cos(t), \sin(t))$, then Mathlib's $p^{-1}(\text{a point})$ will be a bunch of discrete points, while Hatcher's $p^{-1}(\text{an open interval on } \mathbb{S}^1)$ will be a bunch of disjoint intervals.

[Adam Topaz]

I’m not sure what you mean? It’s the same map. And being a covering w.r.t. Hatcher is equivalent to being a covering w.r.t. mathlib

[Gareth Ma]

Okay. Sorry I was just a bit confused.

[Yury G. Kudryashov]

Sometimes Mathlib definitions a written in a way that cause confusion when you first see them... Usually, there is a reason (e.g., to make it work in sufficiently general settings).

[Kevin Buzzard]

e.g. docs#Group ;-)