6.48. MappingDegree.RegularValueExistsRegUnconditional🔗

Jacobians.MappingDegree.RegularValueExistsRegUnconditional — source

infinite_of_chartedSpace_complex

A connected complex 1-manifold is infinite. From ChartedSpace ℂ Y plus T2Space Y plus Nonempty Y (via ConnectedSpace Y), there is a chart at any point whose source is open in Y and homeomorphic to an open set of ℂ. Open sets of ℂ are infinite, so Y is infinite.

theorem infinite_of_chartedSpace_complex
    {Y : Type v} [TopologicalSpace Y] [T2Space Y] [ConnectedSpace Y]
    [ChartedSpace ℂ Y] : Infinite Y

deriv_chart_pullback_ne_zero_of_inj_on_neighbourhood

Auxiliary: local injectivity of f at x plus analyticity of the chart pullback at c x (where c = chartAt ℂ x) implies the chart pullback's derivative at c x is nonzero, provided we additionally know the pullback is not eventually constant at c x (delivered by the clopenness-of-locally-const machinery for non-constant f).

This packages the planar bridge notInjOn_iff_deriv_zero_of_analytic_of_order specialised to the situation we are in: at a non-critical preimage of a non-critical-value y, both analyticity and non-eventual-constancy hold.

lemma deriv_chart_pullback_ne_zero_of_inj_on_neighbourhood
    {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) (x : X)
    (h_inj : ∃ U ∈ 𝓝 x, Set.InjOn f U) :
    deriv ((chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm)
      ((chartAt ℂ x) x) ≠ 0

exists_regularValueWitnessReg_value_eq

Witness at a prescribed regular value. A value y₀ off the critical-value set yields a regularity-certified witness *with that exact value* — so its fibre cardinality can be identified with y₀'s. (This is steps 4–7 of exists_regularValueWitnessReg at a caller-chosen y₀ instead of a Classical.choice-picked one.)

lemma exists_regularValueWitnessReg_value_eq
    {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)
    {y₀ : Y} (hy₀ : y₀ ∉ Jacobians.Discharge.Manifold.criticalValuesGeneral f) :
    ∃ w : RegularValueWitnessReg f, w.toWitness.value = y₀

exists_regularValueWitnessReg

Headline existence. For every non-constant analytic f : X → Y between compact connected complex 1-manifolds, Nonempty (RegularValueWitnessReg f).

theorem exists_regularValueWitnessReg
    {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) :
    Nonempty (RegularValueWitnessReg f)