The pointed Abel–Jacobi morphism

Mathematical statement

Let $k$ be a field and let $C/k$ be smooth, proper, geometrically irreducible, and of relative dimension $1$. For $P\in C(k)$, the definition gives a $k$-morphism $a_P:C\to J_C$ to the fixed descended Jacobian, the point-minus-basepoint Abel–Jacobi morphism. Its normalization is proved:

$$a_P(P)=0.$$

The motivating divisor-class formula is $Q\mapsto[\mathcal O_C(Q-P)]$; the implementation constructs an actual morphism of schemes over $k$.

Lean code

`AlgebraicGeometry.JacobianChallenge.Jacobian.ofCurve`

Published library source ↗Same source in NYLL ↗

def ofCurve (P : 𝟙_ (Over (Spec (CommRingCat.of k))) ⟶ C) : C ⟶ Jacobian C

In-scope Lean context

noncomputable section

universe u

open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory

open NeronModelInfra GoodReductionJacobian

open scoped CategoryTheory.MonObj

namespace AlgebraicGeometry.JacobianChallenge

variable {k : Type u} [Field k] {C : Over (Spec (CommRingCat.of k))}
  [SmoothOfRelativeDimension 1 C.hom] [IsProper C.hom] [GeometricallyIrreducible C.hom]

local instance curveIntegral : GeometricallyIntegral C.hom := by
  have _ : GeometricallyConnected C.hom :=
    GeometricallyIrreducible.geometricallyConnected C.hom
  exact geometricallyIntegral_of_smooth_of_geometricallyConnected C.hom

namespace Jacobian

Full declaration and proof

/-- The actual point-minus-basepoint Abel--Jacobi morphism in the over category. -/
def ofCurve (P : 𝟙_ (Over (Spec (CommRingCat.of k))) ⟶ C) : C ⟶ Jacobian C :=
  let ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) C.hom := ⟨P.left, Over.w P⟩
  let aj : SchemeHomOver C.hom (JacobianVarieties.Picard.Unpointed.toBase k C.hom) :=
    JacobianVarieties.Picard.Unpointed.abelJacobi C.hom ε
  Over.homMk aj.1 aj.2

Source credits and license

Copyright (c) 2026 Christian Merten. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Merten

Statements adapted from LeanEval/AlgebraicGeometry/JacobianChallenge.lean:
https://github.com/leanprover/lean-eval/blob/38361be884302c7edce1908c4aef8296eb2cb27e/LeanEval/AlgebraicGeometry/JacobianChallenge.lean

Local constructions and proofs:
Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729).
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

J. S. Milne. Jacobian Varieties. Springer, New York, in Arithmetic Geometry (Storrs, Conn., 1984), Chapter VII, 167–212, 1986. Author's revised version dated June 12, 2021; original numbering retained.