A machine-checked solution to the Jacobians challenge

3. holomorphic forms🔗

Global holomorphic 1-forms as a ContMDiffSection bundle, the genus as their dimension, and Montel-type compactness for form/function families.

11 modules, 3,709 lines, under Jacobians/Forms/.

References: Forster §§9–10.

  1. 3.1. Keystones
  2. 3.2. Forms
  3. 3.3. Forms.ChartNorm
  4. 3.4. Forms.ChartTransition
  5. 3.5. Forms.Compactness
  6. 3.6. Forms.Complete
  7. 3.7. Forms.Cover
  8. 3.8. Forms.Genus
  9. 3.9. Forms.HolomorphicForms
  10. 3.10. Forms.LocalRep
  11. 3.11. Forms.Montel
  12. 3.12. Forms.SupNorm