6.20. MappingDegree.CriticalValueSetFinite🔗

Jacobians.MappingDegree.CriticalValueSetFinite — source

critical_value_set_finite

Finite critical-value set headline. For non-constant analytic f : X → Y between compact connected complex 1-manifolds, the set of critical values is finite and contains no value of any RegularValueWitnessReg f.

This is the h_critical ingredient of the h_pkg packaging consumed by fibre_card_well_defined_at_regular_holds_of_finiteCriticalValues (HurwitzWellDefinedUnconditionalTopo.lean).

theorem critical_value_set_finite
    {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) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnc : ¬ Jacobians.Discharge.IsConstantMap f) :
    ∃ C : Set Y, C.Finite ∧
      (∀ w : Jacobians.Discharge.ContMDiff.RegularValueWitnessReg f,
        w.toWitness.value ∈ (Cᶜ : Set Y))