A machine-checked solution to the Jacobians challenge

6.49. MappingDegree.RegularValueExistsUnconditional🔗

Jacobians.MappingDegree.RegularValueExistsUnconditional — source

exists_regularValueWitness

Existence of a regular-value witness (regular_value_exists_statement, with no remaining hypotheses). For compact connected complex 1-manifolds X, Y, every non-constant C^ω map f : X → Y admits a regular value witness.

The proof composes:

  • clopennessOfLocallyConst_holds: the locally-constant locus of any C^ω map onto a fixed value is closed (chart-local identity theorem).

  • fibres_finite_statement_holds_of_clopennessOfLocallyConst: fibres-finite reduces to clopen-ness of the locally-constant locus.

  • regular_value_exists_of_fibres_finite: regular-value-exists reduces to fibres-finite via "pick any y : Y".

theorem exists_regularValueWitness
    {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 → Nonempty (RegularValueWitness f)