Path components of the preimage of a subset under a covering map

Let p : E → X be a covering map, let V ⊆ X be path connected, and fix v ∈ V. The path components of p ⁻¹' V are read off from the monodromy of the loops of V on the single fibre over v:

• two points of that fibre are joined by a path inside p ⁻¹' V exactly when monodromy along the image of a loop of V carries one to the other (IsCoveringMap.joinedIn_preimage_iff): project a joining path to a loop of V, and conversely lift a loop of V, whose lift stays over V;
• every point of p ⁻¹' V is joined inside p ⁻¹' V to a point of that fibre (IsCoveringMap.exists_joinedIn_preimage), by lifting a path of V.

When π₁(V, v) is generated by one class c, the orbits of loops of V on the fibre are the cycles of the single monodromy permutation of c. The path components of p ⁻¹' V are then in bijection with the cycles of that permutation (IsCoveringMap.sameCycleQuotientEquivZerothHomotopy). This is the local input for filling in the punctures of a cover of a punctured surface: over a punctured-disc neighbourhood of a puncture, the components of the preimage, and so the points to be added, are the cycles of the local monodromy.

Main declarations

• IsCoveringMap.joinedIn_preimage_iff: points of the fibre over v ∈ V are joined inside p ⁻¹' V exactly when they differ by the monodromy of a loop of V.
• IsCoveringMap.exists_joinedIn_preimage: for a path-connected V, every point of p ⁻¹' V is joined inside p ⁻¹' V to the fibre over v.
• IsCoveringMap.sameCycle_monodromyPerm_iff_joinedIn_preimage: when c generates π₁(V, v), two points of the fibre lie in the same cycle of the monodromy of c exactly when they are joined inside p ⁻¹' V.
• IsCoveringMap.sameCycleQuotientEquivZerothHomotopy: the cycles of that monodromy permutation are the path components of p ⁻¹' V.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, §1.3: Proposition 1.30 (lifting of paths) and the action of π₁ on a fibre by monodromy.

theorem IsCoveringMap.joinedIn_preimage_iff {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {V : Set X} {v : X} (hv : v ∈ V) (e e' : ↑(p ⁻¹' {v})) : JoinedIn (p ⁻¹' V) ↑e ↑e' ↔ ∃ (g : FundamentalGroup ↑V ⟨v, hv⟩), hp.monodromy ((FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨v, hv⟩) g) e = e'

Points of a fibre joined over V. Two points of the fibre over v ∈ V are joined by a path inside p ⁻¹' V exactly when monodromy along the image in π₁(X, v) of some loop of V carries the first to the second.

theorem IsCoveringMap.exists_joinedIn_preimage {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {V : Set X} (hV : IsPathConnected V) {v : X} (hv : v ∈ V) {e : E} (he : p e ∈ V) : ∃ (e' : ↑(p ⁻¹' {v})), JoinedIn (p ⁻¹' V) e ↑e'

Every point over a path-connected V is joined over V to the fibre over v. Lifting a path of V from p e to v, starting at e, gives a path inside p ⁻¹' V ending over v.

theorem IsCoveringMap.sameCycle_monodromyPerm_iff_joinedIn_preimage {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {V : Set X} {v : X} (hv : v ∈ V) {c : FundamentalGroup ↑V ⟨v, hv⟩} (hc : Subgroup.zpowers c = ⊤) (e e' : ↑(p ⁻¹' {v})) : ((hp.monodromyPerm v) ((FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨v, hv⟩) c)).SameCycle e e' ↔ JoinedIn (p ⁻¹' V) ↑e ↑e'

Cycles of a generating loop are the components over V. If the class c generates π₁(V, v), two points of the fibre over v lie in the same cycle of the monodromy permutation of c exactly when they are joined by a path inside p ⁻¹' V.

noncomputable def IsCoveringMap.sameCycleQuotientEquivZerothHomotopy {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {V : Set X} (hV : IsPathConnected V) {v : X} (hv : v ∈ V) {c : FundamentalGroup ↑V ⟨v, hv⟩} (hc : Subgroup.zpowers c = ⊤) : Quotient (Equiv.Perm.SameCycle.setoid ((hp.monodromyPerm v) ((FundamentalGroup.map { toFun := Subtype.val, continuous_toFun := ⋯ } ⟨v, hv⟩) c))) ≃ ZerothHomotopy ↑(p ⁻¹' V)

The cycles of the local monodromy are the path components over V. For a path-connected V ∋ v whose fundamental group is generated by c, sending a point of the fibre over v to its path component in p ⁻¹' V identifies the cycles of the monodromy permutation of c with the path components of p ⁻¹' V.

Equations

• hp.sameCycleQuotientEquivZerothHomotopy hV hv hc = Equiv.ofBijective (Quotient.lift (fun (e : ↑(p ⁻¹' {v})) => ZerothHomotopy.mk ⟨↑e, ⋯⟩) ⋯) ⋯

theorem IsCoveringMap.sameCycleQuotientEquivZerothHomotopy_mk {E : Type u_1} {X : Type u_2} [TopologicalSpace E] [TopologicalSpace X] {p : E → X} (hp : IsCoveringMap p) {V : Set X} (hV : IsPathConnected V) {v : X} (hv : v ∈ V) {c : FundamentalGroup ↑V ⟨v, hv⟩} (hc : Subgroup.zpowers c = ⊤) (e : ↑(p ⁻¹' {v})) : (hp.sameCycleQuotientEquivZerothHomotopy hV hv hc) ⟦e⟧ = ZerothHomotopy.mk ⟨↑e, ⋯⟩

The identification of cycles with path components sends the cycle of a point of the fibre to the path component containing that point.