6.7. MappingDegree.ChartBallOffCentreWitnessDischarge🔗

Jacobians.MappingDegree.ChartBallOffCentreWitnessDischarge — source

AnalyticAt.exists_off_centre_value_ne

Off-centre witness in any small ball. If F : ℂ → ℂ is analytic at z₀ and is *not* eventually equal to F z₀ near z₀, then every metric ball around z₀ of positive radius contains a point at which F differs from F z₀.

Mechanism: the mathlib dichotomy AnalyticAt.eventually_eq_zero_or_eventually_ne_zero applied to G z := F z - F z₀ rules out the "eventually zero" branch by hypothesis, leaving G ≠ 0 (i.e., F z ≠ F z₀) on a punctured neighborhood. Any open ball is itself a neighborhood of z₀, so it intersects that punctured neighborhood non-trivially.

lemma AnalyticAt.exists_off_centre_value_ne
    {F : ℂ → ℂ} {z₀ : ℂ}
    (hF : AnalyticAt ℂ F z₀)
    (hne : ¬ ∀ᶠ z in 𝓝 z₀, F z = F z₀) :
    ∀ r : ℝ, 0 < r → ∃ z ∈ Metric.ball z₀ r, F z ≠ F z₀

ChartPullbackNotEventuallyConstHypothesis

Chart-pullback non-eventual-constancy hypothesis. For every non-constant C^ω map f : X → Y, every fibre point x of every y₀, the chart pullback F = (chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm is not eventually equal to (chartAt ℂ (f x)) (f x) at the chart image (chartAt ℂ x) x.

This is the manifold-side hypothesis-parameter that bridges ¬ IsConstantMap f to per-chart non-constancy of the pullback. The within-one-chart version of this bridge is supplied by chart_pullback_not_eventually_const_of_witness in AnalyticContinuationGlobalization.lean; the manifold-globalization step across chart overlaps is deferred elsewhere and is not the subject of this file.

def ChartPullbackNotEventuallyConstHypothesis
    (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

chartBallOffCentreWitness_of_chart_pullback_not_eventually_const

Discharge of ChartBallOffCentreWitnessHypothesis. From the chart-pullback non-eventual-constancy hypothesis-parameter and the ℂ-analyticity of chart pullbacks, every chart ball around the chart image of a fibre point contains an off-centre value witness.

Proof: the chart pullback is analytic at z₀ = (chartAt ℂ x) x by the bridge (contMDiff_omega_analyticAt_chart_pullback). Combined with the hypothesis "F is not eventually F z₀" (rewritten via the chart-left-inverse identity F z₀ = (chartAt ℂ (f x)) (f x)), the ℂ-side extractor AnalyticAt.exists_off_centre_value_ne produces a witness in any ball.

theorem chartBallOffCentreWitness_of_chart_pullback_not_eventually_const
    {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 : ChartPullbackNotEventuallyConstHypothesis X Y) :
    ChartBallOffCentreWitnessHypothesis X Y

fibres_finite_statement_holds_of_chart_pullback_not_eventually_const

End-to-end conditional discharge of fibres_finite_statement from chart-pullback non-eventual-constancy.

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