Unique factorization through Abel–Jacobi

Mathematical statement

Let $k$ be a field, let $C/k$ be smooth, proper, geometrically irreducible, and of relative dimension $1$, and choose $P\in C(k)$. Let $A/k$ be a smooth proper geometrically irreducible group scheme. For a $k$-morphism $f:C\to A$ with $f(P)=0$,

$$\exists!\,g:J_C\longrightarrow A\quad\text{such that}\quad f=g\circ a_P.$$

The quantified $g$ in the cited declaration is a morphism in the category of schemes over $k$.

Lean code

`AlgebraicGeometry.JacobianChallenge.Jacobian.exists_unique_ofCurve_comp`

Published library source ↗Same source in NYLL ↗

theorem exists_unique_ofCurve_comp
    {k : Type u} [Field k]
    (C : Over (Spec (.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (.of k))) ⟶ C)
    {A : Over (Spec (.of k))} [Smooth A.hom] [IsProper A.hom] [GrpObj A]
    [GeometricallyIrreducible A.hom] (f : C ⟶ A) (hf : P ≫ f = η[A]) :
    ∃! (g : Jacobian C ⟶ A), f = ofCurve P ≫ g

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

/-- Every pointed morphism to an abelian variety factors uniquely through the
same Abel--Jacobi morphism and the fixed Jacobian, over the original field. -/
theorem exists_unique_ofCurve_comp
    {k : Type u} [Field k]
    (C : Over (Spec (.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (.of k))) ⟶ C)
    {A : Over (Spec (.of k))} [Smooth A.hom] [IsProper A.hom] [GrpObj A]
    [GeometricallyIrreducible A.hom] (f : C ⟶ A) (hf : P ≫ f = η[A]) :
    ∃! (g : Jacobian C ⟶ A), f = ofCurve P ≫ g := by
  have : GeometricallyConnected A.hom :=
    GeometricallyIrreducible.geometricallyConnected A.hom
  have : GeometricallyIntegral A.hom :=
    geometricallyIntegral_of_smooth_of_geometricallyConnected A.hom
  let ε : SchemeHomOver (𝟙 (Spec (.of k))) C.hom := ⟨P.left, Over.w P⟩
  let q : SchemeHomOver C.hom A.hom := ⟨f.left, Over.w f⟩
  let : GrpObj (Over.mk A.hom) := inferInstanceAs (GrpObj A)
  let G : RelativeGroupLaw k A.hom := relativeGroupLawOfGrpObj k A.hom
  have hq : NeronModelInfra.schemeHomOverComp ε q = G.one (𝟙 _) := by
    apply Subtype.ext
    change P.left ≫ f.left = (1 : Over.mk (𝟙 (Spec (.of k))) ⟶ Over.mk A.hom).left
    rw [← MonObj.one_eq_one]
    exact congrArg (fun h => h.left) hf
  obtain ⟨g, hg, hu⟩ :=
    JacobianVarieties.Picard.Unpointed.exists_unique_abelJacobi_factorization
      C.hom ε A.hom G q hq
  let g' : Jacobian C ⟶ A := Over.homMk g.1 g.2
  refine ⟨g', ?_, ?_⟩
  · apply Over.OverMorphism.ext
    exact hg.symm
  · intro h hh
    let h' : SchemeHomOver (JacobianVarieties.Picard.Unpointed.toBase k C.hom) A.hom :=
      ⟨h.left, Over.w h⟩
    have he : h' = g := hu h' (congrArg (fun e => e.left) hh).symm
    apply Over.OverMorphism.ext
    exact congrArg Subtype.val he

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.