Covering maps involving the complex plane

In this file, we show that Complex.exp and (· ^ n) (for n ≠ 0) are a covering map on {0}ᶜ. We also show that any complex polynomial is a covering map on the set of regular values.

theorem Complex.isAddQuotientCoveringMap_exp : IsAddQuotientCoveringMap (fun (z : ℂ) => ⟨exp z, ⋯⟩) ↥(AddSubgroup.zmultiples (2 * ↑Real.pi * I))

theorem Complex.isCoveringMap_exp : IsCoveringMap fun (z : ℂ) => ⟨exp z, ⋯⟩

exp : ℂ → ℂ \ {0} is a covering map.

theorem Complex.isCoveringMapOn_exp : IsCoveringMapOn exp {0}ᶜ

theorem Polynomial.isCoveringMapOn_eval {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (p : Polynomial 𝕜) : IsCoveringMapOn (fun (x : 𝕜) => eval x p) ((fun (x : 𝕜) => eval x p) '' {k : 𝕜 | eval k (derivative p) = 0})ᶜ

theorem isCoveringMapOn_npow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℕ) (hn : ↑n ≠ 0) : IsCoveringMapOn (fun (x : 𝕜) => x ^ n) {0}ᶜ

theorem isCoveringMap_npow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℕ) (hn : ↑n ≠ 0) : IsCoveringMap fun (x : { x : 𝕜 // x ≠ 0 }) => ⟨↑x ^ n, ⋯⟩

(· ^ n) : 𝕜 \ {0} → 𝕜 \ {0} is a covering map (if n ≠ 0 in 𝕜).

theorem isCoveringMap_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℤ) (hn : ↑n ≠ 0) : IsCoveringMap fun (x : { x : 𝕜 // x ≠ 0 }) => ⟨↑x ^ n, ⋯⟩

(· ^ n) : 𝕜 \ {0} → 𝕜 \ {0} is a covering map (if n ≠ 0 in 𝕜).

theorem isCoveringMapOn_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℤ) (hn : ↑n ≠ 0) : IsCoveringMapOn (fun (x : 𝕜) => x ^ n) {0}ᶜ

theorem isQuotientCoveringMap_npow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℕ) (hn : ↑n ≠ 0) (surj : Function.Surjective fun (x : 𝕜) => x ^ n) : IsQuotientCoveringMap (fun (x : 𝕜ˣ) => x ^ n) ↥(powMonoidHom n).ker

theorem Complex.isQuotientCoveringMap_npow (n : ℕ) [NeZero n] : IsQuotientCoveringMap (fun (z : ℂˣ) => z ^ n) ↥(powMonoidHom n).ker

theorem isQuotientCoveringMap_zpow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℤ) (hn : ↑n ≠ 0) (surj : Function.Surjective fun (x : 𝕜) => x ^ n) : IsQuotientCoveringMap (fun (x : 𝕜ˣ) => x ^ n) ↥(zpowGroupHom n).ker