6.45. MappingDegree.PerChartNonConstancyReduction🔗

Jacobians.MappingDegree.PerChartNonConstancyReduction — source

not_eventually_eq_self_of_witness

Single-point off-centre witness ⇒ not eventually constant. If F is analytic on a preconnected open set U, z₀ ∈ U, and there is some z₁ ∈ U with F z₁ ≠ F z₀, then F is not eventually F z₀ at z₀. This is the contrapositive of mathlib's identity theorem (AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq) against the constant fun _ => F z₀.

lemma not_eventually_eq_self_of_witness
    {F : ℂ → ℂ} {U : Set ℂ} {z₀ z₁ : ℂ}
    (hF : AnalyticOnNhd ℂ F U) (hU : IsPreconnected U)
    (h₀ : z₀ ∈ U) (h₁ : z₁ ∈ U) (h_ne : F z₁ ≠ F z₀) :
    ¬ ∀ᶠ z in 𝓝 z₀, F z = F z₀

exists_value_ne_in_nhds_of_witness

Per-point form of the identity-theorem reduction. From analyticity on a preconnected open U and a single off-centre witness z₁ ∈ U with F z₁ ≠ F z₀ (where z₀ ∈ U), every neighborhood of z₀ contains a point at which F differs from F z₀.

This is the per-point shape consumed by PerChartNonConstancyHypothesis.

lemma exists_value_ne_in_nhds_of_witness
    {F : ℂ → ℂ} {U : Set ℂ} {z₀ z₁ : ℂ}
    (hF : AnalyticOnNhd ℂ F U) (hU : IsPreconnected U)
    (h₀ : z₀ ∈ U) (h₁ : z₁ ∈ U) (h_ne : F z₁ ≠ F z₀) :
    ∀ V ∈ 𝓝 z₀, ∃ z ∈ V, F z ≠ F z₀

ChartBallOffCentreWitnessHypothesis

Chart-ball off-centre witness hypothesis (all radii). For every non-constant C^ω map f : X → Y, every fibre point x of every y₀ : Y, and *every* radius r > 0, there is a point z₁ in the open ball of radius r around the chart image of x at which the chart pullback F differs from F at the chart image of x.

Equivalently: the chart pullback is not locally constant at the chart image of x.

This shape is strictly smaller than PerChartNonConstancyHypothesis:

• It eliminates the universal quantifier over neighborhoods V ∈ 𝓝 z₀. The caller produces, for each radius r > 0, a single off-centre witness inside Metric.ball z₀ r — the identity theorem (mathlib's AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq) lifts these witnesses to *every* neighborhood.

• It does not mention Filter, 𝓝, or eventual equality at all.

• The metric structure is fixed (open balls in ℂ) — no preconnectedness, analyticity, or chart-data is required from the caller.

def ChartBallOffCentreWitnessHypothesis
    (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] : Prop

perChartNonConstancy_of_chartBallOffCentreWitness

Reduction. The chart-ball off-centre witness hypothesis (all radii) implies the per-chart non-constancy hypothesis. The proof:

1. From contMDiff_omega_analyticAt_chart_pullback the chart pullback is AnalyticAt ℂ at the chart image of x.

2. By exists_preconnected_open_ball_of_analyticAt, there is a preconnected open ball of radius r₀ > 0 on which the pullback is AnalyticOnNhd ℂ.

3. The hypothesis applied at radius r₀ gives a witness z₁ inside that same ball with F z₁ ≠ F z₀.

4. Mathlib's identity theorem (exists_value_ne_in_nhds_of_witness above) lifts this single off-centre witness to every neighborhood of z₀.

theorem perChartNonConstancy_of_chartBallOffCentreWitness
    {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 : ChartBallOffCentreWitnessHypothesis X Y) :
    PerChartNonConstancyHypothesis X Y

fibres_finite_statement_holds_of_chartBallOffCentreWitness

End-to-end conditional discharge of fibres_finite_statement from the chart-ball hypothesis.

theorem fibres_finite_statement_holds_of_chartBallOffCentreWitness
    {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 : ChartBallOffCentreWitnessHypothesis X Y) :
    ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f →
        ∀ y : Y, (f ⁻¹' {y}).Finite