6.5. MappingDegree.AnalyticFiberDiscrete🔗

Jacobians.MappingDegree.AnalyticFiberDiscrete — source

analyticAt_isolated_zero_of_not_eventually_zero

Per-point identity theorem (zero version). If F : ℂ → ℂ is analytic at z₀, F z₀ = 0, and F 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.

lemma analyticAt_isolated_zero_of_not_eventually_zero
    {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₀}

analyticAt_isolated_value_of_not_eventually_const

Per-point identity theorem (value version). Same as analyticAt_isolated_zero_of_not_eventually_zero but framed as "F z = c is isolated at z₀" for an arbitrary target value c.

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

ChartPullbackData

Chart-pullback isolation data. For a map f : X → Y between topological spaces, point x : X and value y₀ : Y, this records a chart-pullback witness that x is isolated in f ⁻¹' {y₀}.

• V — open neighbourhood of x in X,

• chartX : V → ℂ — homeomorphic image of V into ℂ,

• chartY : Y → ℂ — a continuous "chart-like" function with chartY y₀ = c for some constant c, and the property that chartY separates y₀ from other values *on f '' V*: f x' = y₀ ↔ chartY (f x') = c for x' ∈ V.

• F : ℂ → ℂ — the chart-pulled-back representation chartY ∘ f ∘ chartX⁻¹,

• hFA — F is analytic at chartX x,

• hFne — F is not eventually equal to c near chartX x.

We do not assume F z = chartY (f (chartX⁻¹ z)) globally, only that the zero-set comparison goes through, which is the only thing the proof uses.

structure ChartPullbackData {X : Type u} [TopologicalSpace X]
    {Y : Type v} (f : X → Y) (x : X) (y₀ : Y) where

fiber_pointIsolated_via_chart_pullback

Per-point isolation from chart-pullback data. Given chart-pullback data witnessing that the chart-pulled-back f is analytic and not eventually constant at chartX x, the point x is isolated in f ⁻¹' {y₀}.

lemma fiber_pointIsolated_via_chart_pullback
    {X : Type u} [TopologicalSpace X]
    {Y : Type v}
    (f : X → Y) (y₀ : Y) (x : X) (hx : f x = y₀)
    (D : ChartPullbackData f x y₀) :
    ∃ U : Set X, IsOpen U ∧ U ∩ f ⁻¹' {y₀} = {x}

isDiscrete_fiber_of_chart_pullback

Globalised: IsDiscrete of a fibre from per-point chart data. If for every x ∈ f ⁻¹' {y₀} we have a ChartPullbackData witness, then the fibre f ⁻¹' {y₀} carries the discrete subspace topology.

lemma isDiscrete_fiber_of_chart_pullback
    {X : Type u} [TopologicalSpace X]
    {Y : Type v}
    (f : X → Y) (y₀ : Y)
    (h : ∀ x ∈ f ⁻¹' {y₀}, ChartPullbackData f x y₀) :
    IsDiscrete (f ⁻¹' {y₀})

fibres_finite_of_chart_pullback

fibres_finite_statement from the chart-pullback hypothesis. Composing fibres_finite_of_all_fibers_isDiscrete with isDiscrete_fiber_of_chart_pullback reduces the full classical fibres_finite_statement to a single clean chart-pullback hypothesis: for every analytic non-constant f and every y, every fibre point admits a ChartPullbackData witness.

lemma fibres_finite_of_chart_pullback {ω : WithTop ℕ∞}
    {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type v} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] [IsManifold 𝓘(ℂ) ω Y]
    (h_chart : ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f →
      ∀ y : Y, ∀ x ∈ f ⁻¹' {y}, ChartPullbackData f x y) :
    ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f → ¬ Jacobians.Discharge.IsConstantMap f →
      ∀ y : Y, (f ⁻¹' {y}).Finite