A Jacobian without a rational base point

Mathematical statement

Let $k$ be a field and let $C/k$ be smooth, proper, geometrically irreducible, and of relative dimension $1$. The definition constructs a scheme over $k$, denoted $J_C$, without requiring a point in $C(k)$.

The associated genus is the geometric function-field genus, denoted $g(C)$. The public construction uses finite faithfully flat descent to obtain the fixed object $J_C/k$.

Lean code

`AlgebraicGeometry.JacobianChallenge.Jacobian`

Published library source ↗Same source in NYLL ↗

def Jacobian (C : Over (Spec (CommRingCat.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom] :
    Over (Spec (CommRingCat.of k))

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

Full declaration and proof

/-- The Jacobian over the original field, with no rational basepoint required. -/
def Jacobian (C : Over (Spec (CommRingCat.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom] :
    Over (Spec (CommRingCat.of k)) :=
  Over.mk (JacobianVarieties.Picard.Unpointed.toBase k C.hom)

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

Alexander Grothendieck. Technique de descente et théorèmes d'existence en géométrie algébrique. V. Les schémas de Picard : théorèmes d'existence. Séminaire Bourbaki, Exposé 232, 143–161, 1962.