6.51. MappingDegree.WithinChartWitnessReduction🔗

Jacobians.MappingDegree.WithinChartWitnessReduction — source

exists_preconnected_open_ball_of_analyticAt

AnalyticAt provides a preconnected open neighborhood of analyticity. If F : ℂ → ℂ is AnalyticAt ℂ at z₀, then there exists an open ball around z₀ on which F is AnalyticOnNhd ℂ. Open balls in ℂ are convex hence preconnected.

The proof uses AnalyticAt.eventually_analyticAt to extract analyticity on a neighborhood, and Metric.eventually_nhds_iff to pin down a metric ball inside that neighborhood.

lemma exists_preconnected_open_ball_of_analyticAt
    {F : ℂ → ℂ} {z₀ : ℂ} (hF : AnalyticAt ℂ F z₀) :
    ∃ r : ℝ, 0 < r ∧ IsPreconnected (Metric.ball z₀ r) ∧
      z₀ ∈ Metric.ball z₀ r ∧
      AnalyticOnNhd ℂ F (Metric.ball z₀ r)

PerChartNonConstancyHypothesis

Per-chart non-constancy hypothesis. For every non-constant C^ω map f : X → Y and every fibre point x of every y₀ : Y, the chart pullback of f takes a value other than the chart image of f x in every neighborhood of the chart image of x.

This is strictly weaker (and strictly different in shape) than WithinChartWitnessHypothesis: the caller does not need to provide a preconnected open U, an analyticity statement, or a specific witness point. The analyticity of the chart pullback on a small open ball around the chart image follows from contMDiff_omega_analyticAt_chart_pullback; the witness point z₁ is extracted as a value-difference inside that ball.

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

withinChartWitness_of_perChartNonConstancy

Reduction. The per-chart non-constancy hypothesis implies the within-chart witness hypothesis. The proof:

1. Get analyticity of the chart pullback at (chartAt ℂ x) x from the bridge.

2. Extract a preconnected open ball U = Metric.ball ((chartAt ℂ x) x) r on which the pullback is AnalyticOnNhd, via exists_preconnected_open_ball_of_analyticAt.

3. The ball U is in 𝓝 ((chartAt ℂ x) x) (it is open and contains the centre); apply per-chart non-constancy at V := U to extract a witness z₁ ∈ U with F z₁ ≠ c.

theorem withinChartWitness_of_perChartNonConstancy
    {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 : PerChartNonConstancyHypothesis X Y) :
    WithinChartWitnessHypothesis X Y

fibres_finite_statement_holds_of_perChartNonConstancy

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

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