30.7. Abel.AbelFinal
Jacobians.Abel.AbelFinal — source
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