13.5. SphereTopology.GenusZeroOfSphere🔗

Jacobians.SphereTopology.GenusZeroOfSphere — source

HasHolomorphicPrimitives

The de Rham wall, isolated. On a simply connected complex 1-manifold, every global holomorphic 1-form η admits a *global* holomorphic primitive F : X → ℂ (i.e. dF = η, expressed value-wise on tangent vectors to avoid the cotangent/trivial-bundle type diamond).

This is the holomorphic Poincaré lemma / monodromy theorem: simple connectivity makes ∫ η path-independent, so F(x) := ∫_{x₀}^{x} η is well defined and holomorphic with dF = η (Forster §10.5). Mathlib provides this only on balls in ℂ (Complex.DifferentiableOn.isExactOn_ball); the manifold globalisation (homotopy invariance of the line integral over loops in X) is absent from both Mathlib and this repo — the remaining de Rham gap. Isolated as an explicit hypothesis, not a gap, so the rest of the route is complete.

def HasHolomorphicPrimitives (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] : Prop

holomorphicOneForm_eq_zero_of_hasPrimitive

A holomorphic form with a *global* holomorphic primitive on a compact connected surface is 0. The primitive F is constant (MDifferentiable.exists_eq_const_of_compactSpace, the manifold maximum-modulus / Liouville theorem), so mfderiv F = 0, so η vanishes on every tangent vector, so η = 0.

theorem holomorphicOneForm_eq_zero_of_hasPrimitive
    (η : HolomorphicOneForms X) (F : X → ℂ) (hF : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) F)
    (hprim : ∀ (x : X) (v : TangentSpace 𝓘(ℂ) x), η.toFun x v = mfderiv 𝓘(ℂ) 𝓘(ℂ) F x v) :
    η = 0

genus_eq_zero_of_hasPrimitives_of_simplyConnected

#1b, abstract form. Given the de Rham input HasHolomorphicPrimitives X and that X is simply connected, genus X = 0. Every holomorphic 1-form has a primitive (input), hence vanishes (holomorphicOneForm_eq_zero_of_hasPrimitive), so the genus — finrank ℂ of the space of such forms — is 0.

theorem genus_eq_zero_of_hasPrimitives_of_simplyConnected
    (hPrim : HasHolomorphicPrimitives X) (hSC : SimplyConnectedSpace X) :
    genus X = 0

genus_zero_of_nonempty_homeo_sphere_of_hasPrimitives

#1b, the exact target — assembled. A surface homeomorphic to S² has genus 0, given the single remaining de Rham input HasHolomorphicPrimitives X.

The simple-connectivity input is supplied *unconditionally* by the repo: X ≃ₜ S² transports SimplyConnectedSpace from the now-proven SimplyConnectedSpace S² (Jacobians.VanKampen, twoOpenVanKampen_holds). Composing with genus_eq_zero_of_hasPrimitives_of_simplyConnected discharges the goal.

This has the exact signature of genus_zero_of_nonempty_homeo_sphere (Jacobians/ProperDegree/DegreeOneSphere.lean) *plus* the explicit de Rham hypothesis — supplying HasHolomorphicPrimitives X closes that headline obligation.

theorem genus_zero_of_nonempty_homeo_sphere_of_hasPrimitives
    (hPrim : HasHolomorphicPrimitives X)
    (h : Nonempty (X ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)) :
    genus X = 0