3.8. Forms.Genus🔗

Jacobians.Forms.Genus — source

HolomorphicOneForms

The ℂ-vector space of global analytic sections of the cotangent bundle of a compact connected complex 1-manifold.

Mathematically: global holomorphic 1-forms on X. Defined here (rather than in HolomorphicForms.lean) so that genus below can refer to it.

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

genus

The genus of a compact Riemann surface, defined as the ℂ-dimension of global holomorphic 1-forms. Since Module.finrank returns 0 for non-finite-dimensional modules, this is well-defined unconditionally; the FiniteDimensional ℂ (HolomorphicOneForms X) instance (in HolomorphicForms.lean, content-gated) is required for genus to be the "right" number.

noncomputable def genus (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
  [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] : ℕ