A machine-checked solution to the Jacobians challenge

30.7. Abel.AbelFinal🔗

Jacobians.Abel.AbelFinalsource

abelJacobi_twoPoint_ne_zero

Consequence of Abel's theorem + non-existence of degree-1 maps to ℙ¹ on positive-genus surfaces: the Abel–Jacobi image of a two-point divisor P - Q is nonzero when P ≠ Q on a surface of positive genus.

Classical argument: if abelJacobi (P - Q) = 0, then by Abel's theorem P - Q is principal — some meromorphic function f has a simple zero at P and a simple pole at Q and no other zeros/poles. Such an f is a degree-1 map X → ℙ¹, hence a biholomorphism (Riemann-Hurwitz). But then X ≃ ℙ¹, which has genus 0 — contradiction.

theorem abelJacobi_twoPoint_ne_zero
    (h : 0 < genus X) {P Q : X} (hPQ : P ≠ Q) :
    abelJacobi ⟨twoPointDivisor X P Q, twoPointDivisor_mem_degZero X P Q⟩ ≠ 0