Uniformity in Mordell–Lang for curves
Problem statement
Notes: AnnalsChallenge states this theorem on top of Christian Merten's Jacobian challenge (`AnnalsChallenge/Definitions/AlgebraicJacobian.lean`). LeanEval's existing port of that file, problem `jacobian_challenge_alggeo`, omits the four declarations at its end, including the instances that supply the `CommGroup` and `Group.FG` structures used by `freeRank`. This module therefore carries a namespaced copy of the full upstream Jacobian characterisation and its derived point-group structure. Proof-valued instance holes are expressed as instance-reducible definitions so comparator can traverse the derived instances without comparing placeholder proof bodies; their types and the statement of Theorem 1.1 are unchanged. The upstream `instCommGroup := inferInstance` is spelled as the same explicit, reducible `CategoryTheory.Hom.commGroup` instance so Challenge and Solution elaborate it with identical reducibility hints; it remains derived rather than becoming a solver hole.
Source: 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 (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-194-1-UniformMordellLang.lean
Informal solution: Unavailable.
/-- The genus of a smooth proper curve. -/
def declaration uses `sorry`genus (C : Over (Spec (.of k))) [IsProper C.hom] [SmoothOfRelativeDimension 1 C.hom]
[GeometricallyIrreducible C.hom] : ℕ :=
sorry/-- The Jacobian of a smooth, proper curve over a field `k`. -/
def declaration uses `sorry`Jacobian (C : Over (Spec (.of k))) [IsProper C.hom] [SmoothOfRelativeDimension 1 C.hom]
[GeometricallyIrreducible C.hom] : Over (Spec (.of k)) :=
sorry/-- The group scheme structure on the Jacobian of the curve `C`. -/
instance declaration uses `sorry`instGrpObj : GrpObj (Jacobian C) :=
sorry/-- The Jacobian of `C` is smooth of relative dimension `g` over `k`, where `g` is the
genus of `C`. -/
@[instance_reducible, instance]
noncomputable def declaration uses `sorry`smoothOfRelativeDimension_genus :
SmoothOfRelativeDimension (genus C) (Jacobian C).hom :=
sorry/-- The Jacobian of `C` is proper over `k`. -/
@[instance_reducible, instance]
noncomputable def declaration uses `sorry`instIsProper : IsProper (Jacobian C).hom :=
sorry/-- The Jacobian of `C` is geometrically irreducible over `k`. -/
@[instance_reducible, instance]
noncomputable def declaration uses `sorry`instGeometricallyIrreducible :
GeometricallyIrreducible (Jacobian C).hom :=
sorry/-- The Abel-Jacobi map from a smooth, proper curve to its Jacobian associated
to a `k`-rational point of `C`. -/
def declaration uses `sorry`ofCurve (P : 𝟙_ (Over (Spec (.of k))) ⟶ C) : C ⟶ Jacobian C :=
sorry/-- The Abel-Jacobi map sends the `k`-rational point `P` to `0`, where `0` (denoted by `η` below) is
the neutral element of the group scheme `Jacobian C`. -/
theorem declaration uses `sorry`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] :=
sorry/--
The universal property of the Jacobian variety: For any abelian variety `A`,
any morphism `f : C ⟶ A` such that `f(P) = 0` factors uniquely through the
Jacobian of `C`.
In other words, `Jacobian C` is the Albanese variety of `C`.
-/
theorem declaration uses `sorry`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 :=
sorry/-- The Jacobian of `C` is geometrically integral over `k`. -/
@[instance_reducible, instance]
noncomputable def declaration uses `sorry`instGeometricallyIntegral : GeometricallyIntegral (Jacobian C).hom :=
sorry/-- If `k` is a number field, then the `k`-points of the Jacobian of `C` are finitely generated.
This is the Mordell-Weil theorem; it is what gives Theorem 1.1's `ρ` a meaning. Anonymous
upstream, named here so that it can be addressed as a hole. -/
@[instance_reducible, instance]
noncomputable def declaration uses `sorry`instFG [NumberField k] :
@Group.FG (𝟙_ (Over (Spec (.of k))) ⟶ Jacobian C)
(instCommGroup (k := k) (C := C)).toGroup :=
sorry/-- The function `c` of Theorem 1.1 of the paper. -/
noncomputable def declaration uses `sorry`c (g : ℕ) (d : ℕ) : ℕ :=
sorry/--
Statement of Theorem 1.1:
Let `g ≥ 2` and `d ≥ 1` be integers. Then there exists a constant `c = c(g, d) ≥ 1` with the
following property. If `C` is a smooth curve of genus `g` defined over a number field `F` with
`[F : Q] ≤ d`, then `#C(F) ≤ c^(1+ρ)`, where `ρ` is the rank of `Jac(C)(F)`.
We do not give a complete definition of the Jacobian of `C`. Instead, a characterization can be
found in `UniformMordellLang.JacobianChallenge` above whose sorries must be filled.
Note however that the characterization of the Jacobian of `C` is only correct when the `C` has an
`F`-point, but Theorem 1.1 is trivial when `C` has no `F`-points, so this is not a problem.
-/
theorem declaration uses `sorry`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] (hC : genus C = g) :
ENat.card (𝟙_ (Over (Spec (.of F))) ⟶ C) ≤
c g d ^ (1 + freeRank (𝟙_ (Over (Spec (.of F))) ⟶ Jacobian C)) := g:ℕd:ℕhg:g ≥ 2hd:d ≥ 1F:Type u_1inst✝⁴:Field Finst✝³:NumberField FhF:finrank ℚ F ≤ dC:Over (Spec (CommRingCat.of F))inst✝²:IsProper C.hominst✝¹:SmoothOfRelativeDimension 1 C.hominst✝:GeometricallyIrreducible C.homhC:genus C = g⊢ ENat.card (𝟙_ (Over (Spec (CommRingCat.of F))) ⟶ C) ≤
↑(c g d) ^ (1 + freeRank (𝟙_ (Over (Spec (CommRingCat.of F))) ⟶ Jacobian C))
All goals completed! 🐙