6.30. MappingDegree.HPkgUnconditional🔗

Jacobians.MappingDegree.HPkgUnconditional — source

exists_finiteCriticalValues_fibreCard_isLocallyConstant

The finite-critical-values packaging. For every non-constant analytic f : X → Y there is a finite set C ⊆ Y (the critical values of f) such that every RegularValueWitnessReg f takes its value in Cᶜ and the fibre-cardinality function y ↦ (f ⁻¹' {y}).ncard is locally constant on Cᶜ.

theorem exists_finiteCriticalValues_fibreCard_isLocallyConstant
    {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] :
    ∀ (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)