Pulling a covering map back along a continuous map

Let g : Z → Y be a covering map and f : X → Y a continuous map. The fibre product X ×_Y Z = {(x, z) | f x = g z} (Mathlib's Function.Pullback f g), with the subspace topology of X × Z, projects to X by Function.Pullback.fst, and that projection is again a covering map whose fibre over x is the fibre of g over f x. If H : g ⁻¹' U ≃ₜ U × I trivialises g over an open U ∋ f x, then (x', z) ↦ (x', (H z).2) trivialises the projection over f ⁻¹' U.

The relative version is what produces covers from equations: for n ≠ 0 the power map y ↦ y ^ n is a covering of ℂ over ℂ ∖ {0}, so for a continuous h : X → ℂ without zeros the curve {(x, y) | h x = y ^ n} is a covering of X.

Pulling a covering back along a homotopy equivalence e : A ≃ₕ B does not change the homotopy type of the total space: the projection A ×_B E → E is a homotopy equivalence. With φ : A → B, ψ : B → A and homotopies φ ∘ ψ ≃ id and ψ ∘ φ ≃ id, the homotopy inverse sends e ∈ E to ψ (p e) together with the end of the lift at e of the path from p e to φ (ψ (p e)). That this is a right homotopy inverse follows from the lifted homotopy. For the other side, the same construction for the pulled-back covering A ×_B E → A and the map ψ gives a right homotopy inverse of the projection B ×_A (A ×_B E) → A ×_B E; following a path forwards and back returns to its start by uniqueness of lifts, and the two one-sided inverses combine. Only the homotopy lifting property of coverings and uniqueness of path lifts are used; no compatibility between the two homotopies is needed.

Main results

• IsEvenlyCovered.pullback_fst: a point evenly covered by g pulls back to evenly covered points of the projection, with the same fibre.
• IsCoveringMap.pullback_fst: the pullback of a covering map is a covering map.
• IsCoveringMapOn.pullback_fst: the pullback of a map that is a covering over s is a covering over the preimage of s.
• IsCoveringMapOn.isCoveringMap_pullback_fst: the pullback of a map that is a covering over s along a map into s is a covering map.
• IsCoveringMap.pullbackHomotopyEquiv: the pullback of a covering map along a homotopy equivalence has homotopy equivalent total space.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, §1.3 (covering spaces and their lifting properties, Proposition 1.30 for homotopy lifting).
• J. P. May, A Concise Course in Algebraic Topology, University of Chicago Press, 1999, Chapter 7 (fibrations; the pullback of a fibration along a homotopy equivalence).

theorem IsEvenlyCovered.pullback_fst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Z → Y} {I : Type u_4} [TopologicalSpace I] {x : X} (hf : Continuous f) (h : IsEvenlyCovered g (f x) I) : IsEvenlyCovered Function.Pullback.fst x I

If f x is evenly covered by g with fibre I, then x is evenly covered with fibre I by the projection X ×_Y Z → X of the fibre product of f and g.

theorem IsCoveringMap.pullback_fst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Z → Y} (hg : IsCoveringMap g) (hf : Continuous f) : IsCoveringMap Function.Pullback.fst

The pullback of a covering map is a covering map: for a covering map g : Z → Y and a continuous f : X → Y, the projection X ×_Y Z → X of the fibre product is a covering map.

theorem IsCoveringMapOn.pullback_fst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Z → Y} {s : Set Y} (hg : IsCoveringMapOn g s) (hf : Continuous f) : IsCoveringMapOn Function.Pullback.fst (f ⁻¹' s)

If g : Z → Y is a covering map over s and f : X → Y is continuous, then the projection X ×_Y Z → X of the fibre product is a covering map over f ⁻¹' s.

theorem IsCoveringMapOn.isCoveringMap_pullback_fst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Z → Y} {s : Set Y} (hg : IsCoveringMapOn g s) (hf : Continuous f) (hfs : ∀ (x : X), f x ∈ s) : IsCoveringMap Function.Pullback.fst

If g : Z → Y is a covering map over s and the continuous map f : X → Y takes values in s, then the projection X ×_Y Z → X of the fibre product is a covering map.

Pulling back along a homotopy equivalence

noncomputable def IsCoveringMap.pullbackHomotopyEquiv {E : Type u_4} {B : Type u_5} {A : Type u_6} [TopologicalSpace E] [TopologicalSpace B] [TopologicalSpace A] {p : E → B} (hp : IsCoveringMap p) (e : ContinuousMap.HomotopyEquiv A B) : ContinuousMap.HomotopyEquiv (Function.Pullback (⇑e.toFun) p) E

Pulling a covering back along a homotopy equivalence. If p : E → B is a covering map and e : A ≃ₕ B is a homotopy equivalence, then the projection A ×_B E → E from the fibre product of e and p is a homotopy equivalence.

@[simp]

theorem IsCoveringMap.coe_pullbackHomotopyEquiv {E : Type u_4} {B : Type u_5} {A : Type u_6} [TopologicalSpace E] [TopologicalSpace B] [TopologicalSpace A] {p : E → B} (hp : IsCoveringMap p) (e : ContinuousMap.HomotopyEquiv A B) : ⇑(hp.pullbackHomotopyEquiv e).toFun = Function.Pullback.snd

@[simp]

theorem IsCoveringMap.pullbackHomotopyEquiv_symm_apply_fst {E : Type u_4} {B : Type u_5} {A : Type u_6} [TopologicalSpace E] [TopologicalSpace B] [TopologicalSpace A] {p : E → B} (hp : IsCoveringMap p) (e : ContinuousMap.HomotopyEquiv A B) (x : E) : ((hp.pullbackHomotopyEquiv e).symm.toFun x).fst = e.symm.toFun (p x)

The first coordinate of the homotopy inverse of the projection A ×_B E → E at x is e.symm (p x).