A machine-checked solution to the Jacobians challenge

27. serre duality tails🔗

Serre duality through Laurent tails (Miranda VI.3): multiplication action on H¹-tails, surjectivity, the order downgrade, and h¹(D) = l(K−D).

11 modules, 3,156 lines, under Jacobians/TailDuality/.

References: Miranda Lemma 3.6 · Miranda Ch. VI · Forster §17.4 · Miranda Ch. VI p. 187.

  1. 27.1. Keystones
  2. 27.2. Builds on
  3. 27.3. TailDuality
  4. 27.4. TailDuality.PairDualityInjective
  5. 27.5. TailDuality.PairDualitySurjective
  6. 27.6. TailDuality.RiemannRochGenusPos
  7. 27.7. TailDuality.RiemannRochUnconditional
  8. 27.8. TailDuality.TailDualityInjective
  9. 27.9. TailDuality.TailDualitySurjective
  10. 27.10. TailDuality.TailDualitySurjectiveAssembly
  11. 27.11. TailDuality.TailMultiplication
  12. 27.12. TailDuality.TailMultiplicationH1
  13. 27.13. TailDuality.TailResidue