A machine-checked solution to the Jacobians challenge

26.6. ProperDegree.DegreeOneSphere🔗

Jacobians.ProperDegree.DegreeOneSphere — source

MeromorphicFunction.toSphere

The map X → ℂℙ¹ associated with a meromorphic function f and a chosen pole P: send finite points through the limit-repair holoRepr (composed with ℂ ↪ ℂℙ¹) and P to ∞. (We send *only* P to ∞; with a single simple pole at P this is the honest "graph" of f.)

We use f.holoRepr rather than the raw f.toFun because f.toFun is pinned only up to its meromorphic germ — at a removable singularity it may carry an arbitrary junk value (see Jacobians.MeromorphicLiouville) — which would make coe ∘ f.toFun discontinuous off P and toSphere *not* ContMDiff. The repair holoRepr x = limUnder (𝓝[≠] x) f.toFun discards that junk and is analytic wherever the order of f is ≥ 0.

def MeromorphicFunction.toSphere (f : MeromorphicFunction X) (P : X) :
    X → RiemannSphere

MeromorphicFunction.toSphere_pole

@[simp] lemma MeromorphicFunction.toSphere_pole {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X) (P : X) :
    f.toSphere P P = OnePoint.infty

MeromorphicFunction.toSphere_of_ne

lemma MeromorphicFunction.toSphere_of_ne {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X) {P x : X}
    (hx : x ≠ P) :
    f.toSphere P x = ((f.holoRepr x : ℂ) : RiemannSphere)

MeromorphicFunction.toSphere_preimage_infty

Preimage of ∞ under toSphere is exactly {P} (since coe never hits ∞ and we send only P to ∞).

lemma MeromorphicFunction.toSphere_preimage_infty {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X) (P : X) :
    f.toSphere P ⁻¹' {OnePoint.infty} = {P}

contMDiffAt_omega_of_analyticAt_chartPullback

Converse chart bridge AnalyticAt → ContMDiffAt … ω. For a map F : X → Y between complex-analytic manifolds modelled on ℂ, if F is continuous at x and its chart pullback (chartAt ℂ (F x)) ∘ F ∘ (chartAt ℂ x).symm is AnalyticAt ℂ at (chartAt ℂ x) x, then F is ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω at x. (Reverse of contMDiffAt_omega_analyticAt_chart_pullback.)

theorem contMDiffAt_omega_of_analyticAt_chartPullback {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {F : X → Y} {x : X} (hcont : ContinuousAt F x)
    (hana : AnalyticAt ℂ ((chartAt ℂ (F x)) ∘ F ∘ (chartAt ℂ x).symm) ((chartAt ℂ x) x)) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω F x

MeromorphicFunction.contMDiffAt_toSphere_of_ne

Off P, toSphere is ContMDiff … ω. For x ≠ P the order of f is ≥ 0, so holoRepr is analytic in the chart there; toSphere = coe ∘ holoRepr reads, in the affine chart chartCoe at the finite value coe (holoRepr x), as holoRepr ∘ (chartAt x).symm, which is analytic (analyticAt_holoRepr_chartPullback_of_orderNonneg).

theorem MeromorphicFunction.contMDiffAt_toSphere_of_ne {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) {P x : X}
    (hP : f.HasSingleSimplePole P) (hx : x ≠ P) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω (f.toSphere P) x

MeromorphicFunction.contMDiffAt_toSphere_at_pole

At the simple pole P, toSphere is ContMDiffAt … ω. Reading in the ∞-chart chartInfty at toSphere P = ∞, the chart pullback G = chartInfty ∘ toSphere ∘ φ.symm (φ = chartAt P) equals, near φ P, the inverse of the normal-form representative Nw⁻¹ of the pullback F = f.toFun ∘ φ.symm. Since F has meromorphicOrderAt = -1 (the simple pole), its normal form N has order -1, so N⁻¹ (which = the chart pullback) is in normal form of order +1 ≥ 0, hence analytic at φ P with value 0.

theorem MeromorphicFunction.contMDiffAt_toSphere_at_pole {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X) {P : X}
    (hP : f.HasSingleSimplePole P) :
    ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω (f.toSphere P) P

MeromorphicFunction.contMDiff_toSphere

Holomorphy of toSphere (Step 1). Off P, toSphere = coe ∘ holoRepr, which is analytic where the order of f is ≥ 0 (contMDiffAt_toSphere_of_ne). At P, reading in chartInfty, toSphere is z ↦ 1/f, which is analytic with value 0 because the pole is simple (contMDiffAt_toSphere_at_pole). Together these give ContMDiff … ω everywhere.

theorem MeromorphicFunction.contMDiff_toSphere {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) {P : X}
    (hP : f.HasSingleSimplePole P) :
    ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (f.toSphere P)

exists_ne_of_chartedSpace_complex

Every charted space over ℂ is nontrivial at each point: there is always a second point. Proof: the chart e at P is an open embedding into ℂ; its target is a nonempty open set, which cannot be the singleton {e P} (singletons are not open in ℂ), so it contains some w ≠ e P, whose preimage e.symm w differs from P.

theorem exists_ne_of_chartedSpace_complex {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (P : X) : ∃ x : X, x ≠ P

MeromorphicFunction.toSphere_not_isConstant

toSphere is non-constant: it takes the value ∞ (at P) and a finite value coe (holoRepr x) at any x ≠ P (such an x exists by exists_ne_of_chartedSpace_complex), and coe _ ≠ ∞. This uses the genuine IsConstantMap predicate (∃ c, ∀ x, f x = c), which is non-vacuous since X is nonempty.

theorem MeromorphicFunction.toSphere_not_isConstant {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X)
    {P : X} (_hP : f.HasSingleSimplePole P) :
    ¬ IsConstantMap (f.toSphere P)

MeromorphicFunction.toSphere_regular_at_pole

The pole is a regular point of F = toSphere f P (Step 2's analytic core, and the genuine consumer of *simplicity*). Reading F near P in the ∞-chart, F is z ↦ 1/f whose derivative at P is nonzero precisely because the pole is simple (orderAtPoint P = -1): a double pole would give a vanishing derivative here (chart-pullback z ↦ z²-shaped), so its fibre-degree would be 2, not 1. This is the chart-pullback-derivative-nonzero certificate the regular-witness bundle (RegularValueWitnessReg.is_regular) requires at the unique preimage P of ∞.

theorem MeromorphicFunction.toSphere_regular_at_pole {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] (f : MeromorphicFunction X)
    {P : X} (hP : f.HasSingleSimplePole P) :
    ∀ x ∈ (f.toSphere P) ⁻¹' {OnePoint.infty},
      deriv ((chartAt ℂ (OnePoint.infty : RiemannSphere)) ∘ (f.toSphere P) ∘
          (chartAt ℂ x).symm) ((chartAt ℂ x) x) ≠ 0

MeromorphicFunction.degreeFiber_toSphere_eq_one

Degree one (Step 2). ∞ is a regular value of F = toSphere f P with the single preimage P (toSphere_preimage_infty), and P is a regular point (toSphere_regular_at_pole, consuming pole simplicity). Packaging this as a RegularValueWitnessReg whose fibre {P} has cardinality 1, witness-independence of the fibre degree (degreeFiber_eq_card_of_regularWitness) gives degreeFiber F hF = 1.

theorem MeromorphicFunction.degreeFiber_toSphere_eq_one (f : MeromorphicFunction X)
    {P : X} (hP : f.HasSingleSimplePole P)
    (hF : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω (f.toSphere P)) :
    degreeFiber (f.toSphere P) hF = 1

infinite_of_isOpen_nonempty

A nonempty open subset of a complex 1-manifold Y is infinite: it is locally homeomorphic to a nonempty open subset of ℂ, and those are infinite.

theorem infinite_of_isOpen_nonempty {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {W : Set Y} (hW : IsOpen W) (hne : W.Nonempty) : W.Infinite

exists_mem_open_notMem_finite

In a complex 1-manifold, removing a finite set from a nonempty open set leaves a nonempty set (open sets are infinite, finite sets removable).

theorem exists_mem_open_notMem_finite {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {W C : Set Y} (hW : IsOpen W) (hne : W.Nonempty) (hC : C.Finite) :
    ∃ y ∈ W, y ∉ C

degreeOne_homeo

Degree-one ⟹ homeomorphism (Step 3). A non-constant degree-one holomorphic map F : X → Y between compact connected Riemann surfaces is bijective and a local biholomorphism, hence a homeomorphism.

Proof:

  • Surjective — surjective_of_nonconstant (open + closed image, connected target).

  • Injective — every regular value y (off the finite critical-value set) has a *singleton* fibre, because degreeFiber F hF = (F⁻¹{y}).ncard = 1 by witness- independence of the degree. If F a = F b = c with a ≠ b, take disjoint opens U ∋ a, V ∋ b (Hausdorff); their open images F '' U, F '' V (open mapping) both contain c, so the open intersection contains a regular value y; then y has preimages in U and in V, contradicting the singleton fibre.

  • Continuous open bijection ⟹ homeomorphism (Equiv.toHomeomorphOfContinuousOpen).

theorem degreeOne_homeo {Y : Type*} [TopologicalSpace Y] [T2Space Y]
    [CompactSpace Y] [ConnectedSpace Y] [Nonempty Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y]
    (F : X → Y) (hF : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω F)
    (hnc : ¬ IsConstantMap F)
    (hdeg : degreeFiber F hF = 1) :
    Nonempty (X ≃ₜ Y)

nonempty_homeo_sphere_of_singleSimplePole

Degree-one ⟹ sphere. If a meromorphic function f on a compact connected Riemann surface X has a single simple pole at some P, then X is homeomorphic to the Euclidean 2-sphere S² ⊆ ℝ³.

Proof: F := f.toSphere P : X → ℂℙ¹ is holomorphic (Step 1), non-constant, and has degree 1 because F⁻¹(∞) = {P} (Step 2). A degree-one holomorphic map of compact connected Riemann surfaces is a homeomorphism (Step 3), so X ≃ₜ ℂℙ¹, and ℂℙ¹ ≃ₜ S² via RiemannSphere.homeoSphere (Step 4).

theorem nonempty_homeo_sphere_of_singleSimplePole
    (f : MeromorphicFunction X) {P : X} (hP : f.HasSingleSimplePole P) :
    Nonempty (X ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)

genus_zero_of_nonempty_homeo_sphere

The backward half. A surface homeomorphic to S² has genus 0.

genus X = Module.finrank ℂ (HolomorphicOneForms X) is analytic, while X ≃ₜ S² is purely topological; the bridge is the contrapositive route (Jacobians.GenusSphereBackward): X ≃ₜ S² makes X simply connected, on which every holomorphic 1-form has a global primitive, hence (being constant on compact X, Liouville) vanishes, so genus X = 0.

The three ingredients: S² is simply connected (van Kampen, Jacobians.VanKampen.twoOpenVanKampen_holds), transported to X along the homeomorphism; Liouville / max-modulus (MDifferentiable.exists_eq_const_of_compactSpace); and the holomorphic Poincaré lemma / monodromy theorem (Jacobians.hasHolomorphicPrimitives), a discrete analytic-continuation build with no integration.

theorem genus_zero_of_nonempty_homeo_sphere {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (h : Nonempty (X ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)) :
    genus X = 0