Semilocal simple connectivity and covering maps

This file relates semilocal simple connectivity to local homeomorphisms and covering maps.

The mechanism for descending semilocal simple connectivity is a local section. If p : E → X is a local homeomorphism and e : E, then p restricts to a homeomorphism from a neighbourhood of e onto an open set U ∋ p e, so a loop inside U is the image under p of a loop in E. If that loop in E is null-homotopic, so is its image. Only the local-section structure of a local homeomorphism is used, never path lifting. At a chosen e : E, only loops based at e need to be null-homotopic. The space-level result assumes this at every point, which is weaker than SimplyConnectedSpace E: it does not ask E to be path-connected, and so applies to a cover whose components are separately simply connected.

The same neighbourhoods run the other way as well: the preimage of a witnessing neighbourhood is one upstairs, because a covering map is injective on the Hom-sets of the fundamental groupoid.

Main results

• TauCeti.semilocallySimplyConnectedAt_of_isLocalHomeomorph: the image of a point under a local homeomorphism is a point of semilocal simple connectivity if every loop based at the source point is null-homotopic.
• TauCeti.SemilocallySimplyConnectedSpace.of_isLocalHomeomorph and TauCeti.SemilocallySimplyConnectedSpace.of_isCoveringMap: the space-level forms, the second saying that the base of a surjective covering map with simply connected total space is semilocally simply connected.
• IsCoveringMap.semilocallySimplyConnectedSpace: conversely, the total space of a covering map over a semilocally simply connected base is semilocally simply connected.

References

The necessity argument is the classical one from Hatcher, Algebraic Topology, the discussion following Proposition 1.36.

theorem TauCeti.semilocallySimplyConnectedAt_of_isLocalHomeomorph {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsLocalHomeomorph p) (e : E) (hE : ∀ (γ : Path e e), γ.Homotopic (Path.refl e)) : SemilocallySimplyConnectedAt (p e)

The image of a point under a local homeomorphism is semilocally simply connected, as soon as every loop based at that point is null-homotopic.

The witnessing neighbourhood of p e is the source of the local inverse of p at e; a loop inside it is carried by that local inverse to a loop in E, which is null-homotopic by hypothesis, and pushing the null-homotopy forward along p returns the original loop.

theorem TauCeti.SemilocallySimplyConnectedSpace.of_isLocalHomeomorph {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsLocalHomeomorph p) (hsurj : Function.Surjective p) (hE : ∀ (e : E) (γ : Path e e), γ.Homotopic (Path.refl e)) : SemilocallySimplyConnectedSpace X

A space that is the image of a local homeomorphism whose source has only null-homotopic loops is semilocally simply connected.

theorem TauCeti.SemilocallySimplyConnectedSpace.of_isCoveringMap {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} [SimplyConnectedSpace E] (hp : IsCoveringMap p) (hsurj : Function.Surjective p) : SemilocallySimplyConnectedSpace X

The base of a surjective covering map whose total space is simply connected is semilocally simply connected. So the standing hypothesis under which the universal cover is built is not just sufficient but necessary.

theorem IsCoveringMap.semilocallySimplyConnectedSpace {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} [TauCeti.SemilocallySimplyConnectedSpace X] (hp : IsCoveringMap p) : TauCeti.SemilocallySimplyConnectedSpace E

Semilocal simple connectivity passes to the total space of a covering map. A loop in the preimage of a witnessing neighbourhood downstairs projects to a null-homotopic loop, and a covering map is injective on the Hom-sets of the fundamental groupoid, so the loop upstairs is null-homotopic as well.

Together with IsLocalHomeomorph.locallyPathConnectedSpace this says that a covering map preserves the two local standing hypotheses of the universal-cover construction: over a locally path-connected, semilocally simply connected base, the total space is again locally path-connected and semilocally simply connected. Path-connectedness of the base is not inherited — a cover can be disconnected — so to iterate the construction one restricts to a path component of E.