6.12. MappingDegree.ChartPullbackNotEventuallyConstDischarge🔗

Jacobians.MappingDegree.ChartPullbackNotEventuallyConstDischarge — source

ChartOverlapPropagationHypothesis

Chart-overlap propagation hypothesis. For every C^ω map f : X → Y, every y₀ : Y, every x₀ : X with f x₀ = y₀, and every open set V ⊆ X containing x₀ on which f is identically y₀, the map f is identically y₀ on all of X.

This is the manifold-globalization content deferred by the path-walking analytic-continuation argument. It contains no filter algebra, no chart coordinates, no eventual equality — purely the topological/analytic statement "local-constancy at a single point lifts to global-constancy".

The standard proof uses PathConnectedSpace X (true for connected manifolds) and chains AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq across overlapping charts along a path γ from x₀ to any other point.

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

exists_preconnected_open_ball_eqOn_const_of_eventuallyEq

Identity-theorem packaging. If F : ℂ → ℂ is analytic at z₀ and eventually equal to c at z₀, then there is a preconnected open ball around z₀ of positive radius on which F is identically c.

lemma exists_preconnected_open_ball_eqOn_const_of_eventuallyEq
    {F : ℂ → ℂ} {z₀ : ℂ} {c : ℂ}
    (hF : AnalyticAt ℂ F z₀)
    (hev : ∀ᶠ z in 𝓝 z₀, F z = c) :
    ∃ r : ℝ, 0 < r ∧ IsPreconnected (Metric.ball z₀ r)
      ∧ z₀ ∈ Metric.ball z₀ r ∧ EqOn F (fun _ => c) (Metric.ball z₀ r)

chartPullbackNotEventuallyConst_of_chartOverlapPropagation

Discharge of ChartPullbackNotEventuallyConstHypothesis. From the chart-overlap propagation hypothesis (the path-walking analytic-continuation step) and the ZZ24 analyticity of chart pullbacks, the chart pullback at every fibre point of every y₀ is not eventually equal to (chartAt ℂ y₀) y₀.

Argument: if it were, then by ZZ24 + the identity theorem the pullback is identically c := (chartAt ℂ y₀) y₀ on a preconnected open ball B ⊆ (chartAt ℂ x).target around (chartAt ℂ x) x. Pulling back along (chartAt ℂ x), this gives an open neighborhood of x in X on which the chart-image of f is identically c. Pulling back further along (chartAt ℂ y₀).left_inv, we get f ≡ y₀ on that neighborhood. The chart-overlap propagation hypothesis then upgrades this to f ≡ y₀ on all of X, contradicting ¬ IsConstantMap f.

theorem chartPullbackNotEventuallyConst_of_chartOverlapPropagation
    {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 : ChartOverlapPropagationHypothesis X Y) :
    ChartPullbackNotEventuallyConstHypothesis X Y

fibres_finite_statement_holds_of_chartOverlapPropagation

End-to-end conditional discharge of fibres_finite_statement from chart-overlap propagation. Composing through ZZ38 + ZZ36 + ZZ34 + ZZ32 + ZZ30.

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