genus (CC1, design §2.1) — root-level, exact challenge signature

Unit: holomorphic-forms (docs/design/holomorphic-forms.md). genus X is the dimension of the space of global holomorphic 1-forms RS.Form1 X. This is the most load-bearing definition of the project: it is stated at the root namespace with the exact signature demanded by docs/Jacobian_challenge.lean (ConnectedSpace X is carried only to match that signature — it is not needed for finiteness, see Jacobian/Forms/Finiteness.lean).

Main declarations:

• genus — Module.finrank ℂ (RS.Form1 X), honest by the FiniteDimensional instance of Jacobian/Forms/Finiteness.lean.
• genus_eq_zero_iff_subsingleton — genus X = 0 ↔ Subsingleton (RS.Form1 X).

noncomputable def genus (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : ℕ

The genus of a compact Riemann surface: the dimension of the space of global holomorphic 1-forms.

Equations

• genus X = Module.finrank ℂ (RS.Form1 X)

theorem genus_eq_zero_iff_subsingleton {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : genus X = 0 ↔ Subsingleton (RS.Form1 X)

The genus vanishes iff there are no nonzero global holomorphic 1-forms.