feat(src/topology/covering): Define covering spaces

[tb65536]

This PR adds a definition of covering spaces.

We don't want to say "there exists an index set I : Type u such that f ⁻¹' U is homeomorphic to I × U" (annoying universe issues). Instead, we can use the preimage of any point as our index set. But it's also nice to have a definition with an arbitrary index set (e.g., for proving that an explicit function is a covering map), so this file contains both definitions of evenly_covered and API relating them (evenly_covered_set.to_evenly_covered_pt).

---

[urkud]

Why not reuse fiber_bundle?

[tb65536]

Why not reuse fiber_bundle?

Ah, I hadn't thought about using fiber bundles. One annoying thing is fiber_bundle requires a specifying constant fiber F, which doesn't necessarily hold for covering maps over disconnected spaces.

[tb65536]

After talking with Patrick, I think it's best to keep a custom definition of covering spaces, but add definitions going back and forth between covering spaces and fiber bundles.

In addition to the slight extra generality with disconnected base spaces, the flexibility of different index sets at different points seems helpful when proving that a space is a covering space. For example, when proving that the universal cover (homotopy classes of paths from a fixed x to an arbitrary y) is a covering space, you want to find an index set for the preimage of a small open neighborhood of y. The natural index set is just the preimage of y, which depends on y. And if you try to use a constant index set, such as the preimage of x, I think you will find that you will have to make noncanonical choices paths from x to each y.

[alreadydone]

The nLab definition of covering space does allow non-isomorphic fibers, unlike the Wikipedia definition. Apparently the "fundamental theorem of covering spaces" (Theorem 3.14 in nLab) doesn't care about the condition. However, the nLab definition also allows empty fibers (i.e. non-surjectivity of the covering map), and states that

Remark 2.2. Fibers of a covering space may be empty. Some authors choose to forbid that, adding the condition that p be a surjection, but the resulting category of covering projections over a space B is not as nice as it would be without that condition.

Since you seem to use surjectivity only to prove that a covering map is a quotient map, you may as well just add the condition to that lemma, instead of stipulating it for all covering maps.

Since mathlib already has the fundamental groupoid, I think you may as well directly prove the fundamental theorem 3.14 and derive the existence of universal cover from it (see Proposition 1.3 in this nLab page).

[tb65536]

I removed the surjectivity assumption. I have a sorry-free construction of fiber bundle -> covering map, but it's currently over 100 lines (before serious golfing) with an auxiliary def, so perhaps it's best to leave it for a follow-up PR?

[tb65536]

I'm wondering if it would be better to just define

open topological_fiber_bundle

def is_covering_map (f : E → X) :=
∀ x, discrete_topology (f ⁻¹' {x}) ∧ ∃ e : trivialization (f ⁻¹' {x}) f, x ∈ e.base_set