6.33. MappingDegree.HurwitzWellDefinedUnconditionalTopo🔗

Jacobians.MappingDegree.HurwitzWellDefinedUnconditionalTopo — source

fibre_card_well_defined_at_regular_holds_of_finiteCriticalValues

Hurwitz constant fibre-cardinality, from the finite-critical-values packaging. fibre_card_well_defined_at_regular_statement from only the analytic per-f packaging h_pkg (a finite critical-value set off which the fibre cardinality is locally constant) — the topological path-connectedness residual is supplied unconditionally by isPathConnected_compl_finite_of_connected_chartedSpace_complex.

theorem fibre_card_well_defined_at_regular_holds_of_finiteCriticalValues
    {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_pkg : ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f →
      ¬ Jacobians.Discharge.IsConstantMap f →
      ∃ (C : Set Y), C.Finite ∧
        (∀ w : RegularValueWitnessReg f, w.toWitness.value ∈ (Cᶜ : Set Y)) ∧
        IsLocallyConstant
          (fun y : (Cᶜ : Set Y) => (f ⁻¹' {y.val}).ncard)) :
    ∀ (f : X → Y), ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f → ¬ Jacobians.Discharge.IsConstantMap f →
      ∀ (w₁ w₂ : RegularValueWitnessReg f), w₁.card = w₂.card