31.3. GenusSphereHeadline🔗

Jacobians.GenusSphereHeadline — source

exists_singleSimplePole_of_genus_zero

Riemann–Roch consequence l(P) = 2. Genus 0 yields a meromorphic function with a single simple pole (Forster §16: l(P) = deg P + 1 − g + l(K−P) = 1 + 1 − 0 + 0 = 2). The single-simple-pole extraction from l(P) = 2 is fully proven in Jacobians.RiemannRoch; the only remaining inputs are the classical exists_riemannRoch_divisor (Dolbeault/Serre) and MeromorphicFunction.deg_div (argument principle), isolated there.

theorem exists_singleSimplePole_of_genus_zero {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (h : genus X = 0) :
    ∃ (P : X) (f : Jacobians.MeromorphicFunction X), f.HasSingleSimplePole P

genus_eq_zero_iff_homeo

A compact Riemann surface has genus 0 iff it is homeomorphic to the 2-sphere — the challenge theorem (the "anti-hack" constraint preventing ∀ X, genus X = 0).

The forward direction is the genuine content: genus 0 ⟹ a single-simple-pole meromorphic function (exists_singleSimplePole_of_genus_zero, Riemann–Roch) ⟹ a degree-1 map X → ℂℙ¹ ⟹ X ≃ₜ S² (Jacobians.nonempty_homeo_sphere_of_singleSimplePole). The backward direction is Ω(ℂℙ¹) = 0 (genus_zero_of_nonempty_homeo_sphere).

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