6.18. MappingDegree.CriticalSetDerivBridge🔗

Jacobians.MappingDegree.CriticalSetDerivBridge — source

deriv_ne_zero_of_analyticOrderAt_eq_one

From analyticOrderAt (g - w₀) x₀ = 1 to deriv g x₀ ≠ 0.

theorem deriv_ne_zero_of_analyticOrderAt_eq_one
    {g : ℂ → ℂ} {x₀ w₀ : ℂ}
    (hg : AnalyticAt ℂ g x₀)
    (h_w₀ : g x₀ = w₀)
    (hord : analyticOrderAt (fun z => g z - w₀) x₀ = (1 : ℕ∞)) :
    deriv g x₀ ≠ 0

injOn_nhds_of_deriv_ne_zero

Locally injective from non-vanishing derivative.

theorem injOn_nhds_of_deriv_ne_zero
    {g : ℂ → ℂ} {x₀ : ℂ}
    (hg : AnalyticAt ℂ g x₀) (hd : deriv g x₀ ≠ 0) :
    ∃ U ∈ 𝓝 x₀, Set.InjOn g U

notInjOn_of_analyticOrderAt_ge_two

Order ≥ 2 ⇒ not locally injective.

For analytic g : ℂ → ℂ at x₀ with g x₀ = w₀ and analytic order of g - w₀ at x₀ equal to k ≥ 2, g is not injective on any neighbourhood of x₀: write g(z) − w₀ = v(z)^k with v(z) = (z − x₀)·r(z), deriv v x₀ = r(x₀) ≠ 0 (analytic k-th root of the local factorization); the inverse function theorem on v pulls two distinct k-th roots of unity back to two distinct preimages with equal g-values.

theorem notInjOn_of_analyticOrderAt_ge_two
    {g : ℂ → ℂ} {x₀ w₀ : ℂ} {k : ℕ}
    (hg : AnalyticAt ℂ g x₀)
    (h_w₀ : g x₀ = w₀)
    (hk_ge_two : 2 ≤ k)
    (hord : analyticOrderAt (fun z => g z - w₀) x₀ = (k : ℕ∞)) :
    ¬ ∃ U ∈ 𝓝 x₀, Set.InjOn g U

notInjOn_iff_deriv_zero_of_analytic_of_order

Planar key lemma (under finite-order hypothesis).

For analytic g : ℂ → ℂ at x₀ with the analytic order of g - g x₀ at x₀ equal to some natural k ≥ 1,

(¬ ∃ U ∈ 𝓝 x₀, Set.InjOn g U) ↔ deriv g x₀ = 0,

equivalently ↔ k ≥ 2. The "finite-order" hypothesis is the way the "g not locally constant at its value" assumption enters: locally constant ↔ analyticOrderAt = ⊤.

theorem notInjOn_iff_deriv_zero_of_analytic_of_order
    {g : ℂ → ℂ} {x₀ : ℂ} {k : ℕ}
    (hg : AnalyticAt ℂ g x₀)
    (hk_ge_one : 1 ≤ k)
    (hord : analyticOrderAt (fun z => g z - g x₀) x₀ = (k : ℕ∞)) :
    (¬ ∃ U ∈ 𝓝 x₀, Set.InjOn g U) ↔ deriv g x₀ = 0

ChartBridgePackage

Chart bridge package. Records a chart-pullback view of f : X → Y near x : X together with the data needed to translate "no neighbourhood of x is InjOn for f" into "no neighbourhood of the chart image is InjOn for the chart pullback F", plus analyticity and the explicit finite-order hypothesis.

structure ChartBridgePackage {X Y : Type*}
    [TopologicalSpace X] [TopologicalSpace Y]
    (f : X → Y) (x : X) where

criticalSet_iff_chart_pullback_deriv_zero

Manifold-side bridge. Under a ChartBridgePackage, "x is in the critical set" (no neighbourhood is InjOn for f) is equivalent to "the chart pullback has vanishing derivative at the chart image".

theorem criticalSet_iff_chart_pullback_deriv_zero
    {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    {f : X → Y} {x : X}
    (P : ChartBridgePackage f x) :
    (¬ ∃ U ∈ 𝓝 x, Set.InjOn f U) ↔ deriv P.F P.z₀ = 0