6.19. MappingDegree.CriticalSetDiscrete🔗

Jacobians.MappingDegree.CriticalSetDiscrete — source

analyticAt_isolated_zero_of_not_eventually_zero_of_analytic_deriv

Per-point identity theorem (derivative version). If F' : ℂ → ℂ is analytic at z₀, vanishes at z₀, and is not identically zero on any neighbourhood of z₀, then there is an open set U ∋ z₀ on which z₀ is the unique zero of F'. This is exactly analyticAt_isolated_zero_of_not_eventually_zero applied to the derivative; it is exposed here under a "critical point" name to make the downstream usage self-documenting.

lemma analyticAt_isolated_zero_of_not_eventually_zero_of_analytic_deriv
    {F' : ℂ → ℂ} {z₀ : ℂ}
    (hF' : AnalyticAt ℂ F' z₀) (hz : F' z₀ = 0)
    (hne : ¬ ∀ᶠ z in 𝓝 z₀, F' z = 0) :
    ∃ U : Set ℂ, IsOpen U ∧ z₀ ∈ U ∧ U ∩ {z | F' z = 0} = {z₀}

CriticalChartPullbackData

Critical-point chart-pullback isolation data. For a map f : X → Y between topological spaces, a designated critical-point set crit : Set X, and a point x : X, this records a chart-pullback witness that x is isolated in crit.

The data mirrors ChartPullbackData but the analytic object is the chart-pullback derivative F' : ℂ → ℂ, and the compatibility says x' ∈ crit is detected by F' (φ x') = 0.

• V — open neighbourhood of x in X,

• W — open subset of ℂ,

• φ : V → W — homeomorphic chart image of V,

• F' : ℂ → ℂ — the chart-pulled-back derivative,

• hF'A — F' is analytic at φ x,

• hF'ne — F' is not eventually zero near φ x.

The user supplies hCompat : ∀ x' : V, x'.1 ∈ crit ↔ F' (φ x') = 0.

structure CriticalChartPullbackData {X : Type u} [TopologicalSpace X]
    {Y : Type v} (f : X → Y) (crit : Set X) (x : X) where

criticalSet_pointIsolated_via_chart_pullback

Per-critical-point isolation from chart-pullback data. Given chart-pullback derivative data witnessing that the chart-pulled-back derivative is analytic and not eventually zero at φ x, the point x is isolated in the critical set crit.

lemma criticalSet_pointIsolated_via_chart_pullback
    {X : Type u} [TopologicalSpace X]
    {Y : Type v}
    (f : X → Y) (crit : Set X) (x : X) (hx : x ∈ crit)
    (D : CriticalChartPullbackData f crit x) :
    ∃ U : Set X, IsOpen U ∧ U ∩ crit = {x}

criticalSet_isDiscrete_of_chart_pullback

Globalised: IsDiscrete of the critical set from per-point chart data. If for every x ∈ crit we have a CriticalChartPullbackData witness, then the critical set carries the discrete subspace topology.

lemma criticalSet_isDiscrete_of_chart_pullback
    {X : Type u} [TopologicalSpace X]
    {Y : Type v}
    (f : X → Y) (crit : Set X)
    (h : ∀ x ∈ crit, CriticalChartPullbackData f crit x) :
    IsDiscrete crit

criticalSet_finite_of_isDiscrete_of_isClosed

Critical set finite from compactness + discreteness. If the critical set crit ⊆ X is closed and X is compact T2, and the critical set is discrete, then it is finite.

lemma criticalSet_finite_of_isDiscrete_of_isClosed
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    {crit : Set X} (h_closed : IsClosed crit) (h_disc : IsDiscrete crit) :
    crit.Finite

criticalSet_finite_of_chart_pullback

Critical-set finiteness from chart-pullback hypothesis. Composing criticalSet_isDiscrete_of_chart_pullback with the topological half: given closedness of the critical set and a chart-pullback witness at every critical point, the critical set is finite.

lemma criticalSet_finite_of_chart_pullback
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    {Y : Type v}
    (f : X → Y) (crit : Set X)
    (h_closed : IsClosed crit)
    (h : ∀ x ∈ crit, CriticalChartPullbackData f crit x) :
    crit.Finite