Universal cover of a topological space

Stream: Is there code for X?

[Michael Rothgang]

I wanted to suggest a student project today, which needs the existence of the universal cover... do we have that in mathlib? If not, how far are we from it? I remember there being a saga of covering space PRs, some of which overlapped and/or got stale... can you update me on the progress? Covering spaces are such a basic and useful topic, it would be great to have this :-)

[Michael Rothgang]

@Junyan Xu If I remember correctly, you wrote one of these PRs, right?

[Damiano Testa]

Side stepping the question: do you need the existence, or would assuming that you have a simply connected cover be enough?

[Damiano Testa]

I also agree that having the existence is something that I would expect in the long run!

[Michael Rothgang]

I guess I could side-step it by saying "it has a simply connected cover". Feels a little naughty, though :-)

[Yury G. Kudryashov]

BTW, it would be nice to refactor simply connected so that

• we have IsSimplyConnected predicate for sets, not only a typeclass types;
• we have a Pre* version that doesn't assume nonempty and connected;
• the definition doesn't import category theory.

[Joël Riou]

I have formalized Serre fibrations and the long exact sequence of a fibration of Kan complexes (which implies a similar long homotopy sequence of homotopy groups for a Serre fibration). As I have also formalized the fact that to be a Serre fibration is a local on the base, it is clear that a covering of topological spaces is a Serre fibration, and so there is a long exact homotopy sequences attached to it. Then, if this is relevant for this project, it is probably not necessary to attempt at formalizing the full homotopy sequence of a covering as it will be dissolved in more general API later, but there is no harm doing the lower degree part of it involving the fundamental group and path connected components.

[Junyan Xu]

Thanks for the ping! My plan is to formalize the fundamental theorem of covering spaces, which says taking monodromy (#22771) is an equivalence between the category of covering spaces over a nice space B and the category of functors from its fundamental groupoid to Type _.

The inverse of the monodromy functor associates a covering space to each functor F from the fundamental groupoid of B to Type _; the universal cover will be obtained from the co-Yoneda functor applied to a chosen base point. F.obj b will be the fiber over b : B of the covering map, and we may define a predicate P over partial sections of the type family F.obj, so that for each open U : Set B and section f : Π b : U, F.obj b, P f is defined to say that for any path p entirely lying in U between any two points x and y, one has F.map p (f x) = f y. If the base space B is nice (locally path-connected and semilocally simply-connected) then P is locally constant, and it's proven in #22782 that the étalé space associated to a locally constant predicate is a covering space.

#22782 will also be used to show e.g. holomorphic functions on simply-connected domains have primitives.

#22771 (monodromy) will also be used to compute the fundamental group of the circle (or in general the quotient by a free properly discontinuous action; #7596 shows the quotient map is a covering map, but is currently stuck due to some outstanding request that depends on some API connecting IsCoveringMap and IsCoveringMapOn that's half-finished in another branch.

I tried to write down a definition of semi-locally simply connectedness (SLSC) in a branch but I realized we probably also want locally simply-connected (LSC), weakly locally simply-connected (WLSC), weakly locally path connected (WLPC), and weakly locally connected (WLC), similar to docs#WeaklyLocallyCompactSpace (we already have docs#LocPathConnectedSpace (LPC)), and we can have the following instances:

        LSC →  LPC →  LC
         ↓      ↓     ↓
SLSC ← WLSC → WLPC → WLC
         ↑      ↑     ↑
         SC →   PC →  C

I need to prepare a repo for a workshop on algebraic geometry in two weeks' time so I'm not returning to this soon (though I just addressed review in #22782). There's probably something a student could help with, or they may even follow my outline to construct the universal cover if they find it appealing.

[Filippo A. E. Nuccio]

@Alex Kontorovich hadn't you got something along these lines at Simons?

[Kim Morrison]

I proved "in a semilocally simply connected, locally path-connected space, the quotient of paths by homotopy has the discrete topology" in #31576, which is close to the statement one wants

[Kim Morrison]

(Mostly this was an exercise in seeing what Claude can do these days. I tried for a while to avoid actually typing anything except into Claude code, but eventually relented and finish a few proofs myself. I couldn't get Claude to understand how to implement the refactor in #31574, which in my mind was essential to doing the proofs sanely.)

[Alex Kontorovich]

Oh yes, John Morgan and I put together this scaffold : https://alexkontorovich.github.io/CoveringSpacesProject/web/dep_graph_document.html (He wasn't happy that mathlib's proof of the fundamental theorem of algebra used complex analysis; insisted that it should be a purely topological proof...)