Skip to content

Jacobians of curves

DefinitionGenus of a smooth proper curve#●ready to state

For a field \(k\) and a curve \(C\) over \(k\), that is, a \(k\)-scheme that is proper, smooth of relative dimension \(1\) and geometrically irreducible, the genus of \(C\) is a natural number.

public def_wanted genus (C : Over (Spec (.of k))) [IsProper C.hom] [SmoothOfRelativeDimension 1 C.hom]
    [GeometricallyIrreducible C.hom] : ℕ
Sources
  • https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685. Problem jacobian_challenge_alggeo of the lean-eval benchmark.
Used by 2
Used byThe Jacobian has dimension equal to the genus · Uniform Mordell–Lang for curves

DefinitionJacobian of a smooth proper curve#●ready to state

For a field \(k\) and a curve \(C\) over \(k\), that is, a \(k\)-scheme that is proper, smooth of relative dimension \(1\) and geometrically irreducible, the Jacobian \(J(C)\) of \(C\) is a \(k\)-scheme.

public def_wanted Jacobian (C : Over (Spec (.of k))) [IsProper C.hom] [SmoothOfRelativeDimension 1 C.hom]
    [GeometricallyIrreducible C.hom] : Over (Spec (.of k))
Sources
  • https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685. Problem jacobian_challenge_alggeo of the lean-eval benchmark.
Used by 6
Used byThe Abel–Jacobi map sends the base point to zero · Universal property of the Jacobian · Group law on the rational points of the Jacobian · Abel–Jacobi map · The Jacobian has dimension equal to the genus · Uniform Mordell–Lang for curves
6 statement formalized3 ready to state1 planned

The Jacobian of C is an abelian variety.

TheoremThe Jacobian has dimension equal to the genus#●statement formalized

Let \(C\) be a proper, smooth, geometrically irreducible curve over a field \(k\). The Jacobian \(J(C)\) is smooth of relative dimension \(g\) over \(k\), where \(g\) is the genus of \(C\).

public theorem_wanted smoothOfRelativeDimension_genus :
    SmoothOfRelativeDimension (❰genus❱ C) (❰Jacobian❱ C).hom
Sources
  • https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685. Problem jacobian_challenge_alggeo of the lean-eval benchmark.
Uses 2
Statement usesJacobian of a smooth proper curve · Genus of a smooth proper curve

DefinitionAbel–Jacobi map#●planned

Let \(C\) be a proper, smooth, geometrically irreducible curve over a field \(k\). Each \(k\)-rational point \(P\) of \(C\) gives a morphism of \(k\)-schemes \(C \to J(C)\) from \(C\) to its Jacobian, the Abel–Jacobi map based at \(P\).

public def_wanted ofCurve (P : 𝟙_ (Over (Spec (.of k))) ⟶ C) : C ⟶ ❰Jacobian❱ C
Sources
  • https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685. Problem jacobian_challenge_alggeo of the lean-eval benchmark.
Uses 1 · Used by 2
Statement usesJacobian of a smooth proper curve
Used byThe Abel–Jacobi map sends the base point to zero · Universal property of the Jacobian

TheoremThe Abel–Jacobi map sends the base point to zero#●statement formalized

Let \(C\) be a proper, smooth, geometrically irreducible curve over a field \(k\), let \(J(C)\) be its Jacobian, and let \(P\) be a \(k\)-rational point of \(C\). The Abel–Jacobi map \(C \to J(C)\) based at \(P\) sends \(P\) to the identity point of \(J(C)\) for its group scheme structure.

public theorem_wanted comp_ofCurve (C : Over (Spec (.of k))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom]
    (P : 𝟙_ (Over (Spec (.of k))) ⟶ C) :
    P ≫ ❰ofCurve❱ P = η[❰Jacobian❱ C]
Sources
  • https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685. Problem jacobian_challenge_alggeo of the lean-eval benchmark.
Uses 2
Statement usesJacobian of a smooth proper curve · Abel–Jacobi map

TheoremUniversal property of the Jacobian#●statement formalized

Let \(C\) be a proper, smooth, geometrically irreducible curve over a field \(k\), let \(J(C)\) be its Jacobian, let \(P\) be a \(k\)-rational point of \(C\), and let \(\iota_P : C \to J(C)\) be the Abel–Jacobi map based at \(P\). Let \(A\) be a group scheme over \(k\) that is smooth, proper and geometrically irreducible. For every morphism of \(k\)-schemes \(f : C \to A\) sending \(P\) to the identity point of \(A\), there is a unique morphism of \(k\)-schemes \(g : J(C) \to A\) with \(f = g \circ \iota_P\).

In other words, the Jacobian of \(C\) is the Albanese variety of \(C\).

public theorem_wanted exists_unique_ofCurve_comp (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
Sources
  • https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685. Problem jacobian_challenge_alggeo of the lean-eval benchmark.
Uses 2
Statement usesJacobian of a smooth proper curve · Abel–Jacobi map

Uniform Mordell–Lang (co-located with the Jacobian interface it uses)

TheoremGroup law on the rational points of the Jacobian#●statement formalized

Let \(C\) be a proper, smooth, geometrically irreducible curve over a field \(k\). The commutative group structure on the set of \(k\)-rational points of the Jacobian \(J(C)\) is the one induced by its commutative group scheme structure: the product of two \(k\)-points \(x\) and \(y\) is \(\mu \circ (x, y)\), where \(\mu\) is the multiplication morphism of \(J(C)\).

This pins down the group law rather than allowing an arbitrary commutative group structure.

public theorem_wanted instCommGroup_eq {k : Type u} [Field k]
    {C : Over (Spec (.of k))} [SmoothOfRelativeDimension 1 C.hom]
    [IsProper C.hom] [GeometricallyIrreducible C.hom] :
    (❰instCommGroup❱ : CommGroup (𝟙_ (Over (Spec (.of k))) ⟶ ❰Jacobian❱ C)) =
      @CategoryTheory.Hom.commGroup
        (Over (Spec (.of k)))
        (CategoryTheory.instCategoryOver)
        (AlgebraicGeometry.instCartesianMonoidalCategoryOverScheme)
        (❰Jacobian❱ C)
        (𝟙_ (Over (Spec (.of k))))
        (❰Jacobian.instGrpObj❱)
        (AlgebraicGeometry.instBraidedCategoryOverScheme)
        (❰instIsCommMonObj❱)
Sources
  • https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge/near/587802685. Problem jacobian_challenge_alggeo of the lean-eval benchmark.
Uses 1
Statement usesJacobian of a smooth proper curve

Theorem 1.1

DefinitionUniform Mordell–Lang constant#●ready to state

For natural numbers \(g\) and \(d\), \(c(g, d)\) is a natural number: the constant in the uniform bound on rational points of curves in Theorem 1.1 of Dimitrov, Gao and Habegger.

public def_wanted c (g : ℕ) (d : ℕ) : ℕ
Sources
  • V. Dimitrov, Z. Gao, and P. Habegger, Uniformity in Mordell–Lang for curves, Annals of Math, 194 (1) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_uniform_mordell_lang of the lean-eval benchmark.
Used by 2
Used byThe uniform Mordell–Lang constant is at least one · Uniform Mordell–Lang for curves

TheoremThe uniform Mordell–Lang constant is at least one#●statement formalized

For all natural numbers \(g\) and \(d\), the uniform constant satisfies \(c(g, d) \ge 1\).

public theorem_wanted c_pos (g d : ℕ) : 1 ≤ ❰c❱ g d
Uses 1
Statement usesUniform Mordell–Lang constant

TheoremUniform Mordell–Lang for curves#●statement formalized

Let \(g \ge 2\) and \(d \ge 1\) be natural numbers, let \(F\) be a number field with \([F : \mathbb{Q}] \le d\), and let \(C\) be a proper, smooth, geometrically irreducible curve over \(F\). If \(C\) has genus \(g\), then the number of \(F\)-rational points of \(C\), possibly infinite, is at most \(c(g, d)^{1 + \rho}\), where \(c\) is the uniform constant and \(\rho\) is the free rank of the group of \(F\)-rational points of the Jacobian of \(C\).

public theorem_wanted theorem_1_1 (g d : ℕ) (hg : g ≥ 2) (hd : d ≥ 1) {F : Type*} [Field F] [NumberField F]
    (hF : finrank ℚ F ≤ d) (C : Over (Spec (.of F))) [IsProper C.hom]
    [SmoothOfRelativeDimension 1 C.hom] [GeometricallyIrreducible C.hom] :
    ❰genus❱ C = g → ENat.card (𝟙_ (Over (Spec (.of F))) ⟶ C) ≤
      ❰c❱ g d ^ (1 + freeRank (𝟙_ (Over (Spec (.of F))) ⟶ ❰Jacobian❱ C))
Sources
  • V. Dimitrov, Z. Gao, and P. Habegger, Uniformity in Mordell–Lang for curves, Annals of Math, 194 (1) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_uniform_mordell_lang of the lean-eval benchmark.
Uses 3
Statement usesJacobian of a smooth proper curve · Genus of a smooth proper curve · Uniform Mordell–Lang constant

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.