6.32. MappingDegree.HurwitzWellDefinedFromHPath🔗

Jacobians.MappingDegree.HurwitzWellDefinedFromHPath — source

fibre_card_well_defined_at_regular_holds_of_pathConnected_compl

Hurwitz constant fibre-cardinality, staged on path-connected complements. Given:

• h_path — the complement of any finite set in Y is path-connected (when nonempty); isPreconnected_compl_of_isPathConnected_compl turns it into the IsPreconnected hypothesis consumed downstream.

• h_pkg — per-f packaging: existence of a finite C ⊆ Y with

  • regular witnesses' values in Cᶜ,

  • locally-constant fibre-ncard on Cᶜ.

Conclude the unfolded form of fibre_card_well_defined_at_regular_statement.

theorem fibre_card_well_defined_at_regular_holds_of_pathConnected_compl
    {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_path : ∀ C : Set Y, C.Finite → (Cᶜ : Set Y).Nonempty →
      IsPathConnected (Cᶜ : Set 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