The group scheme and its dimension

The same descended Jacobian is smooth, proper, geometrically irreducible, and has dimension equal to the curve's genus.

The genus becomes the dimension of a group variety, so a numerical invariant of the curve determines the size of the geometric setting in which its torsion and maps to abelian varieties can be studied. In the classical complex construction, this dimension comes from periods of differentials. Milne's Jacobian Varieties connects that analytic picture with the algebraic construction over arbitrary fields.

Mathematical statement

Let $k$ be a field and let $C/k$ be smooth, proper, geometrically irreducible, and of relative dimension $1$. The public declarations give the fixed descended Jacobian $J_C$ a group-object structure and prove

$$J_C/k\ \text{smooth and proper},\qquad J_C\ \text{geometrically irreducible},\qquad \dim J_C=g(C).$$

Lean code

`AlgebraicGeometry.JacobianChallenge.Jacobian.smoothOfRelativeDimension_genus`

Published library source ↗Same source in NYLL ↗

instance smoothOfRelativeDimension_genus :
    SmoothOfRelativeDimension (genus C) (Jacobian C).hom

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 Jacobian has smooth relative dimension equal to the geometric genus. -/
instance smoothOfRelativeDimension_genus :
    SmoothOfRelativeDimension (genus C) (Jacobian C).hom :=
  JacobianVarieties.Picard.Unpointed.smoothOfRelativeDimension 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)

Mathematical statement

Lean code

AlgebraicGeometry.JacobianChallenge.Jacobian.smoothOfRelativeDimension_genus

References

`AlgebraicGeometry.JacobianChallenge.Jacobian.smoothOfRelativeDimension_genus`