Lifting a power substitution through a finite covering of a punctured disc

Let U be a simply connected, locally path connected space, for instance a polydisc, which is open and convex. Let D* = ball 0 R \ {0} be a punctured disc in ℂ, and let p : E → U × D* be a covering map whose fibre over a point has d points. Going around the puncture permutes that fibre, and the permutation has order dividing d !. The substitution t = s ^ n with d ! ∣ n unwinds it. If D'* = ball 0 R' \ {0} with R' ^ n ≤ R, the map (w, s) ↦ (w, s ^ n) from U × D'* to U × D* lifts through p, uniquely once the value at one point is fixed. The d points of the fibre therefore extend to d lifts that are distinct at every point.

The proof applies the lifting criterion IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le. A loop class of U × D* is determined by the degree of the direction of its second coordinate (TauCeti.fundamentalGroupMulEquiv_comp_map_directionFrom_comp_snd_bijective). The substitution multiplies that degree by n (Circle.fundamentalGroupMulEquiv_map_pow), so it sends every loop class of U × D'* to an n-th power. Over a fibre with d points, the n-th power of every loop class has trivial monodromy (IsCoveringMap.monodromyPerm_pow_eq_one), so it lifts to a loop.

This is the topological step of the Puiseux theorem with parameters. Let a monic polynomial in z have analytic coefficients on U × D and a discriminant that vanishes only on U × {0}. Over U × D* its roots form a covering with d sheets, d the degree. After the substitution t = s ^ n with n = d !, the lifts of the base point are d single-valued root functions.

Main definitions and results

• TauCeti.powerSubstitution: the map (w, s) ↦ (w, s ^ n) from U × (ball 0 R' \ {0}) to U × (ball 0 R \ {0}).
• IsCoveringMap.existsUnique_continuousMap_lifts_powerSubstitution: if the fibre over the image of a has d points and d ! divides n, the power substitution has a unique lift through the covering map taking a prescribed value at a.
• IsCoveringMap.exists_continuousMap_lifts_powerSubstitution: the points of that fibre extend to lifts of the power substitution which are pairwise distinct at every point.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Proposition 1.33 (the lifting criterion) and Proposition 1.34 (uniqueness of lifts).
• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 4 (the Puiseux theorem with parameters).

noncomputable def TauCeti.powerSubstitution (U : Type u_1) [TopologicalSpace U] {n : ℕ} {R R' : ℝ} (hn : n ≠ 0) (hR : R' ^ n ≤ R) : C(U × ↑(Metric.ball 0 R' \ {0}), U × ↑(Metric.ball 0 R \ {0}))

The power substitution (w, s) ↦ (w, s ^ n) from U × (ball 0 R' \ {0}) to U × (ball 0 R \ {0}), for n ≠ 0 and R' ^ n ≤ R.

Equations

• TauCeti.powerSubstitution U hn hR = (ContinuousMap.id U).prodMap { toFun := fun (s : ↑(Metric.ball 0 R' \ {0})) => ⟨↑s ^ n, ⋯⟩, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.powerSubstitution_apply_fst (U : Type u_1) [TopologicalSpace U] {n : ℕ} {R R' : ℝ} (hn : n ≠ 0) (hR : R' ^ n ≤ R) (a : U × ↑(Metric.ball 0 R' \ {0})) : ((powerSubstitution U hn hR) a).1 = a.1

@[simp]

theorem TauCeti.coe_powerSubstitution_apply_snd (U : Type u_1) [TopologicalSpace U] {n : ℕ} {R R' : ℝ} (hn : n ≠ 0) (hR : R' ^ n ≤ R) (a : U × ↑(Metric.ball 0 R' \ {0})) : ↑((powerSubstitution U hn hR) a).2 = ↑a.2 ^ n

theorem IsCoveringMap.existsUnique_continuousMap_lifts_powerSubstitution {U : Type u_1} [TopologicalSpace U] {E : Type u_2} [TopologicalSpace E] {n : ℕ} {R R' : ℝ} [SimplyConnectedSpace U] [LocallyPathConnectedSpace U] {p : E → U × ↑(Metric.ball 0 R \ {0})} (hp : IsCoveringMap p) (hn : n ≠ 0) (hR : R' ^ n ≤ R) {a : U × ↑(Metric.ball 0 R' \ {0})} [Finite ↑(p ⁻¹' {(TauCeti.powerSubstitution U hn hR) a})] (hdvd : (Nat.card ↑(p ⁻¹' {(TauCeti.powerSubstitution U hn hR) a})).factorial ∣ n) {e : E} (he : p e = (TauCeti.powerSubstitution U hn hR) a) : ∃! F : C(U × ↑(Metric.ball 0 R' \ {0}), E), F a = e ∧ p ∘ ⇑F = ⇑(TauCeti.powerSubstitution U hn hR)

Lifting the power substitution. Let p : E → U × (ball 0 R \ {0}) be a covering map, with U simply connected and locally path connected. If the fibre over the image of a under the power substitution (w, s) ↦ (w, s ^ n) is finite with d points, and d ! divides n, then the power substitution has a unique continuous lift through p taking any prescribed value e of that fibre at a.

theorem IsCoveringMap.exists_continuousMap_lifts_powerSubstitution {U : Type u_1} [TopologicalSpace U] {E : Type u_2} [TopologicalSpace E] {n : ℕ} {R R' : ℝ} [SimplyConnectedSpace U] [LocallyPathConnectedSpace U] {p : E → U × ↑(Metric.ball 0 R \ {0})} (hp : IsCoveringMap p) (hn : n ≠ 0) (hR : R' ^ n ≤ R) (a : U × ↑(Metric.ball 0 R' \ {0})) [Finite ↑(p ⁻¹' {(TauCeti.powerSubstitution U hn hR) a})] (hdvd : (Nat.card ↑(p ⁻¹' {(TauCeti.powerSubstitution U hn hR) a})).factorial ∣ n) : ∃ (F : ↑(p ⁻¹' {(TauCeti.powerSubstitution U hn hR) a}) → C(U × ↑(Metric.ball 0 R' \ {0}), E)), (∀ (e : ↑(p ⁻¹' {(TauCeti.powerSubstitution U hn hR) a})), (F e) a = ↑e ∧ p ∘ ⇑(F e) = ⇑(TauCeti.powerSubstitution U hn hR)) ∧ ∀ (b : U × ↑(Metric.ball 0 R' \ {0})), Function.Injective fun (e : ↑(p ⁻¹' {(TauCeti.powerSubstitution U hn hR) a})) => (F e) b

The points of a fibre extend to pointwise distinct lifts of the power substitution. Under the hypotheses of IsCoveringMap.existsUnique_continuousMap_lifts_powerSubstitution, each point e of the fibre over the image of a is the value at a of a lift F e of the power substitution, and at every point b the values F e b are pairwise distinct.