covering space theory

Stream: maths

[Apurva Nakade]

Hi, is anyone working on covering space theory a la Munkres? Specifically, I need the fact that R^1 is the universal cover of S^1 to define winding numbers. Thanks,

[Patrick Massot]

See https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Covering.html

[Patrick Massot]

But there is not a lot in this direction.

[Apurva Nakade]

Thanks! Yeah, I had seen that file but I couldn't find anything else on the topic. I'll start working on formalizing some Munkres then.