6.26. MappingDegree.FibreCardWellDefinedAtRegular🔗

Jacobians.MappingDegree.FibreCardWellDefinedAtRegular — source

fibre_card_well_defined_at_regular_holds_of_locallyConstant_preconnected

Hurwitz constant fibre-cardinality from a locally-constant preconnected packaging. Conditional on a packaged existence (for every non-constant analytic f) of a regular-value subset R ⊆ Y carrying:

• support: every regular witness's value lies in R,

• locally-constant ncard on R (analytic / covering-space content),

• preconnected R (topological content).

Conclude the unfolded form of fibre_card_well_defined_at_regular_statement X Y.

Stated in the unfolded ∀ f hf hnc w₁ w₂, w₁.card = w₂.card shape rather than against the def, to avoid intro-time elaboration "typeclass instance problem is stuck" issues observed when applying the def directly. The underlying statement is identical (the def's body).

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