13.4. SphereTopology.GenusSphereBackward🔗

Jacobians.SphereTopology.GenusSphereBackward — source

exists_ne_zero_holomorphicOneForm_of_genus_pos

Step 1. If genus X ≥ 1 then there is a nonzero global holomorphic 1-form. Pure linear algebra: a positive finrank over the field ℂ forces the module to be nontrivial, hence to contain an element distinct from 0.

theorem exists_ne_zero_holomorphicOneForm_of_genus_pos (h : 1 ≤ genus X) :
    ∃ η : HolomorphicOneForms X, η ≠ 0

genus_eq_zero_of_forall_holomorphicOneForm_eq_zero

Step 1, contrapositive form — the exact logical shape the headline proof consumes. If *every* global holomorphic 1-form vanishes, the genus is 0. (This is the conclusion the route delivers: route steps 2–5 show, under X ≃ₜ S², that no nonzero form can exist.)

theorem genus_eq_zero_of_forall_holomorphicOneForm_eq_zero
    (h : ∀ η : HolomorphicOneForms X, η = 0) : genus X = 0

simplyConnectedSpace_of_homeo

Step 5 (transport). A homeomorphism transports simple connectivity: if Y is simply connected and X ≃ₜ Y, then X is simply connected. Via Homeomorph.toHomotopyEquiv and ContinuousMap.HomotopyEquiv.simplyConnectedSpace.

theorem simplyConnectedSpace_of_homeo {X : Type*} [TopologicalSpace X] {Y : Type*}
    [TopologicalSpace Y] [SimplyConnectedSpace Y] (e : X ≃ₜ Y) : SimplyConnectedSpace X