6.17. MappingDegree.ConnectivityGlobalizationReduction🔗

Jacobians.MappingDegree.ConnectivityGlobalizationReduction — source

WithinChartWitnessHypothesis

Within-chart witness hypothesis. For every non-constant C^ω map f : X → Y and every fibre point x of every y₀ : Y, there exists an open preconnected set U ⊆ ℂ containing the chart image of x, on which the chart pullback of f is AnalyticOnNhd, plus a witness z₁ ∈ U whose chart pullback value differs from (chartAt ℂ (f x)) (f x).

This hypothesis is strictly weaker (and strictly different in shape) than ConnectivityGlobalizationHypothesis: that one quantifies a filter ("not eventually equal"); this one provides an explicit (U, z₁) pair from which the filter statement is derived via the classical identity theorem.

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

connectivityGlobalization_of_withinChartWitness

Reduction. The within-chart witness hypothesis implies the connectivity-globalization hypothesis. The proof is a direct application of not_eventually_const_of_not_constOn (the classical identity-theorem contrapositive in this file's companion).

theorem connectivityGlobalization_of_withinChartWitness
    {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 : WithinChartWitnessHypothesis X Y) :
    ConnectivityGlobalizationHypothesis X Y

fibres_finite_statement_holds_of_withinChartWitness

End-to-end: the within-chart witness hypothesis suffices for the full fibres_finite_statement.

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