A machine-checked solution to the Jacobians challenge

2.1. Definitions🔗

2.1.1. genus🔗

The genus of a compact Riemann surface.

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

submission surface · machine-check · spec

2.1.2. Jacobian🔗

The Jacobian of a compact Riemann surface.

example (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] : Type u := Jacobian X

submission surface · machine-check · spec

2.1.3. ofCurve🔗

The Abel-Jacobi map from a compact Riemann surface to its Jacobian.

example (P : X) : X → Jacobian X := ofCurve P

submission surface · machine-check · spec

2.1.4. pushforward🔗

The pushforward map between Jacobians associated to a map of the underlying curves.

example : Jacobian X →ₜ+ Jacobian Y := pushforward f hf

submission surface · machine-check · spec

2.1.5. pullback🔗

Pullback map between Jacobians associated to a map of the underlying curves. Equal to the zero map if the map on curves is constant.

example : Jacobian Y →ₜ+ Jacobian X := pullback f hf

submission surface · machine-check · spec

2.1.6. degree🔗

The degree of a holomorphic map between compact Riemann surfaces. Equal to zero for constant maps, otherwise equal to the usual degree.

example : ℕ := ContMDiff.degree f hf

submission surface · machine-check · spec