Add roadmap: elliptic curves

[CBirkbeck]

A new roadmap for developing the theory of elliptic curves, for the most part (but not exclusively) following Silverman's The Arithmetic of Elliptic Curves (AEC) and Advanced Topics in the Arithmetic of Elliptic Curves (ATAEC), built on Mathlib's WeierstrassCurve + IsElliptic model.

Scope

Two headline theorems — the Hasse bound over 𝔽_q (landable now from existing sorry-free work) and the complex uniformisation ℂ/Λ ≅ E(ℂ) — with the intervening theory (isogenies, torsion, the Weil pairing) built first, so nothing in the roadmap is a leap.

Six dependency-ordered build layers:

0. isogenies, the dual isogeny, the invariant differential, formal groups (AEC III.4–5, IV)
1. torsion E[N] ≅ (ℤ/N)², the Weil pairing, the Tate module (III.6–8)
2. finiteness of E(𝔽_q) and the Hasse bound (V.1)
3. complex uniformisation (VI)
4. local fields: reduction, the Tate curve, Tate's algorithm / Kodaira types / conductor exponent (VII, ATAEC IV–V)
5. twists (X.5)

The Weierstrass model, group law, division polynomials, DVR reduction, heights, and the ℘-function are consumed from Mathlib — collected in a "What Mathlib already has (consume)" section, not made a numbered layer. Out of scope, deliberately: Mordell–Weil, BSD, Selmer/Sha, and modular curves / moduli / the scheme-theoretic reformulation.

Conventions pinned

• The object is WeierstrassCurve K with [W.IsElliptic] (Mathlib has no standalone EllipticCurve type); points are W.toAffine.Point; E[N] is Submodule.torsionBy ℤ (E.Point) N; the Weil pairing lands in μ_N.
• Each layer is stated over the base its mathematics needs — a perfect field / 𝔽_q / ℂ / the fraction field of a DVR / a general field — decided up front, never over a ring more general than the theorem holds over.

Suggested.lean

Builds green (sorry-only) against the pinned Mathlib. Seeds the load-bearing milestones: hasse_bound, finite_point, torsion_addEquiv_prod (E[N]≅(ℤ/N)²), weilPairing + weilPairing_pow_eq_one + weilPairing_nondegenerate, smul_surjective, the two uniformisation isomorphisms, and quadraticTwist + j_quadraticTwist + quadraticTwistPointEquiv. Per the writing guide, the Layer 0/4 objects that need new types (the isogeny type, the Kodaira type, the Tate-curve isomorphism) are specified in the README and built there, not pinned here as sorry-typed junk types.

Provenance (secondary — sources of proofs to migrate)

• Hasse bound — sorry-free and axiom-clean (propext, Classical.choice, Quot.sound) in the AINTLIB HasseWeil project.
• Quadratic twists — FLT #1088 (quadraticTwist, quadraticTwistPointEquiv, j_quadraticTwist, split-after-unramified-twist).
• Tate curve — FLT #1069 / #1085 / #1099.
• ℘-uniformisation — WilliamCoram/LeanBridge (branch work); the open piece there is exactly the bijectivity of φ this roadmap seeds.
• E[N] ≅ (ℤ/N)² — a scheme-theoretic proof exists in the AINTLIB modular-curves development; restated here intrinsically over WeierstrassCurve.

🤖 Generated with Claude Code

[CBirkbeck]

(This again is claude, not me (Chris))

@kbuzzard Thanks for the thorough review — all 24 threads now have replies. The short version: your comments anchored to the pre-rebuild diff, and the 5cb9f4d rebuild had already adopted the big structural points (the projective scheme as the foundation with isogenies/Néron models/twists defined on it; Mordell–Weil, Nagell–Lutz, and Selmer/Sha in scope; complex uniformisation dropped — your observation that the stated iso was vacuous without holomorphy is recorded in the README; separable closures throughout; rank-1 valuation base for reduction; the integer Hasse form; the bilinear μ_N-valued pairing with base-change functoriality as its named API). The remaining per-thread replies note the two deliberate divergences (NeZero retained with a documented reason; Silverman as citation rather than specification). If Stoll is open to contributing the Mordell–Weil material, the roadmap now gives it a home.

[CBirkbeck]

Ran a full accuracy audit of the seeds and provenance against the actual sources (pinned Mathlib, the AINTLIB modular-curves + HasseWeil projects, and the merged FLT #1088) — the same kind of source-reconciliation that caught real errors in the contour roadmap. Fixes pushed in 87ada3b:

Layer 5 (FLT twists) — the one substantive correction. The seeds pinned Module.finrank K L = 2 with a note that Algebra.IsQuadraticExtension isn't upstream yet. It is upstream (pinned Mathlib, LinearAlgebra/Dimension/StrongRankCondition), and the merged FLT #1088 uses the class directly — so I switched quadraticTwist/j_quadraticTwist/quadraticTwistPointEquiv/exists_quadraticTwist_hasSplitMultiplicativeReduction to [Algebra.IsQuadraticExtension K L], dropped the hL threading, and added the [DecidableEq M] the point-equiv needs. Builds green. (The Δ⁶/c₄²/c₆³ formulas, the CommRing base, and the sorry-free claim all checked out against merged main — a stale local FLT clone had briefly suggested otherwise.)

Layer 0 (AINTLIB scheme). projModel_points identifies K-points with (W.baseChange K).toAffine.Point, not W.toAffine.Point — fixed the worked example to match. Noted the EllipticCurve S object's canonical group-enrichment (abelEnrichment_*) is still sorry upstream (to build, not inherit), and that torsion_geometricFibre_rank_two is over algebraically-closed geometric fibres (the intrinsic torsion_addEquiv_prod milestone correctly generalises it to separably closed).

Layer 3 (Hasse). Corrected the provenance path to the real capstone HasseWeil/WeilPairing/HasseBound.lean (hasse_bound/hasse_bound_unconditional, the real form |#E−q−1|≤2√q; the count convention Fintype.card W.toAffine.Point matches the seed). Softened 'sorry-free/axiom-clean' to the flagship term + its #print axioms gate, and flagged the maxHeartbeats override to remove on port.

Mathlib names. EllipticDivisibilitySequence and ModelsWithJ are module names, not declarations — now cite IsEllDivSequence/normEDS and ofJ. Everything else in the consume-list (reduction predicates E.HasMultiplicativeReduction R/.minimal R, Submodule.torsionBy, the 9 typeclasses) verified exact.

[kim-em]

🤖 Codex says:

Thanks—this is a strong roadmap overall, but two seeded theorems are false as stated, and several definitions, dependencies, and provenance claims need correction before it lands.

Blocking mathematical corrections

1. smul_surjective is too general. Over [IsSepClosed K], multiplication by n is surjective only when it is separable, so the theorem needs (hn : (n : K) ≠ 0). [NeZero n] does not exclude char K ∣ n. For arbitrary nonzero n, use [IsAlgClosed K] instead. The existing torsion theorem already has the needed characteristic hypothesis, so the narrower separably closed statement should suffice.

2. isElliptic_quadraticTwistOf is false over an arbitrary CommRing with only D ≠ 0. Since
   Δ(E_{t,n}) = D⁶ Δ(E),
   ellipticity requires D to be a unit. Please either assume IsUnit (t² − 4n) or state the theorem over a field, where nonzero implies invertible. The discriminant, c₄, and c₆ identities can remain over CommRing.

Definitions and mathematical scope

3. Pin the general-base definition of isogeny correctly. Over the general base scheme introduced in Layer 0, “finite surjective” does not imply flatness and is insufficient for the kernel, degree, and dual-isogeny theory used later. Define an isogeny as a finite locally free and surjective group-scheme homomorphism—equivalently finite faithfully flat—and note that over a field this reduces to finite surjective.

4. Separate pointed twists from genus-one torsors. H¹(Gal(Kˢᵉᵖ/K), Aut(E,O)) classifies twists of the pointed elliptic curve; these retain a rational identity point. Genus-one curves without a rational point are torsors classified by H¹(Gal(Kˢᵉᵖ/K), E), belonging with Weil–Châtelet and Sha in Layer 7. The current prose conflates these two theories and consequently overstates why the scheme layer is needed for Layer 5.

5. Qualify the square-class description by characteristic. The description by Kˣ/(Kˣ)² is the characteristic-not-two Kummer picture. In characteristic two, separable quadratic extensions are Artin–Schreier and are described by K/(x²−x). Likewise, the generic Aut E = {±1} discussion needs suitable characteristic and j hypotheses. Please distinguish these cases while retaining the characteristic-free Algebra.IsQuadraticExtension formulation for the concrete construction.

6. Split the local-field hypotheses. Néron models, Kodaira types, component groups, conductors, and Tate’s algorithm belong over a DVR—normally complete or Henselian, with any required residue-field hypotheses stated explicitly. The Tate curve and p-adic analytic material can instead use complete rank-one valued fields, including ℂ_p where appropriate. A single rank-one valuation hypothesis does not support both strands: ℂ_p is nondiscretely valued and does not have a classical Néron model.

Dependency and API corrections

7. Repair the Layer 6→7 backward dependency. The roadmap says its ordering is the dependency order, but Layer 6 consumes Selmer finiteness supplied by Layer 7. This is not a logical cycle, but it is a backward edge that unnecessarily makes Mordell–Weil depend on the continuous-cohomology stack. A cleaner order is to prove weak Mordell–Weil directly using the Kummer argument plus finiteness of the relevant class-group and unit data, then introduce Selmer groups in Layer 7 as the effective refinement.

8. Describe the continuous-cohomology gap precisely. Pinned Mathlib already contains continuousCohomology, ordinary groupCohomology, and nonabelian H¹. The missing work is the Galois-specific packaging: profinite Galois modules, the Kummer/descent connecting map and exact sequence, restriction and inflation–restriction, localization at places and local conditions, and the required finite-level comparison results. Please cite the existing APIs and list these concrete missing pieces instead of saying continuous Galois cohomology is merely “still settling.”

9. Clarify the torsion-module target. The existing AddEquiv is mathematically adequate—an additive equivalence between these N-torsion groups is automatically ZMod N-linear—so this is not a correctness defect. However, later Tate-module and Galois-representation layers consume the statement that E[N] is a free ZMod N-module of rank two. Please expose that structure directly, either as freeness plus rank two or as a ZMod N-linear equivalence, and explain that the equivalence is wrapped in Nonempty because a basis is noncanonical.

Provenance and specification corrections

10. Make the external dependencies reproducible. The Michael Stoll development needs a public source, pinned revision, license, and coordination status before it can serve as the model to migrate. Please provide the same revision and licensing information for the AINTLIB and FLT material that the roadmap proposes bringing into Tau Ceti.

11. Correct the pinned-Mathlib and Hasse provenance. Algebra.IsQuadraticExtension is already present in pinned Mathlib, so “being upstreamed” is stale. The README names HasseWeil/WeilPairing/HasseBound.lean, while Suggested.lean names HasseWeil/HasseBound.lean; reconcile those paths and pin the external revision supporting the claims about axioms, sorry, and heartbeat requirements.

12. Expose the Hasse theorem’s finiteness dependency. Since the seed uses Nat.card, hasse_bound should either take [Finite W.toAffine.Point] explicitly or be presented together with finite_point as a required dependency. Please also state that the nondegenerate Weil-pairing and full N-torsion theory require char K ∤ N.

Once these are corrected, the overall layering and the decision to consume existing Mathlib infrastructure rather than rebuild it look sound.

[CBirkbeck]

FYI all my replies to the comments are from Claude (if thats not obvious)

[CBirkbeck]

Thanks — all 12 points are addressed in 419b326, each verified against the actual sources first (FLT at the #1088 merge commit, the two AINTLIB branches, pinned Mathlib, and Stoll's repository). Point by point:

Blocking corrections — both adopted.

1. smul_surjective now takes (hn : (n : K) ≠ 0) and stays separably closed, as you suggest ( [NeZero n] dropped — it is implied by hn). The docstring records the counterexample shape (inseparable [n] over an imperfect separably closed field like 𝔽_p(t)ˢᵉᵖ) and notes the IsAlgClosed variant we deliberately don't seed.

2. isElliptic_quadraticTwistOf is restated over a field with hD : t² − 4n ≠ 0 — which turns out to be FLT's exact statement (its proof goes through isUnit_iff_ne_zero), so this also restores statement fidelity to the source; the seed had over-generalised to CommRing. The Δ/c₄/c₆ identities stay ring-level, as in FLT. j_quadraticTwistOf likewise now matches FLT's shape (field, twist-ellipticity as an explicit hypothesis).

Definitions and scope.

3. Isogenies are pinned as finite locally free + surjective (= finite faithfully flat) group-scheme homomorphisms, with the field-case reduction to finite surjective noted (conventions, Layer 1, and the Suggested.lean section header). This also matches the provenance: AINTLIB's EndomorphismDegree.lean works with [Flat]+[IsFinite] hypotheses and proves surjectivity, and endDeg is Scheme.Hom.finrank — which only means anything locally free.

4. Pointed twists vs. torsors are now separated exactly as you describe: Layer 5 is H¹(Gal, Aut(E, O)) — every twist keeps its rational point and Weierstrass model — and the genus-one torsors (H¹(Gal, E(Kˢᵉᵖ)), Weil–Châtelet) moved to Layer 7 next to Ш, which is also where the scheme-is-indispensable claim now honestly points.

5. Characteristic split added: K^×/(K^×)² labelled as the char ≠ 2 Kummer picture, char 2 classified by Artin–Schreier K/℘(K); the Aut(E,O) ≅ {±1} line notes j = 0 = 1728 coincide in characteristics 2 and 3; the concrete Algebra.IsQuadraticExtension construction stays characteristic-free.

6. Layer 4 split into two strands: Néron models / Kodaira types / component groups / conductors / Tate's algorithm over a DVR (complete or Henselian per statement, residue-field hypotheses explicit — Ogg's formula flagged as Saito's theorem in residue characteristic 2, 3), and the Tate curve over a complete rank-1 valued field including ℂ_p, with the "ℂ_p has no Néron model" point stated. The consume-section note about generalising Mathlib's reduction predicates now targets the Tate-curve strand specifically. BLR and Saito added to the references.

Dependencies and API.

7. The Layer 6→7 backward edge is gone. Weak Mordell–Weil is now proved within Layer 6 by the Kummer x − θ argument into A(S, 2), finite by S-class-group finiteness + S-unit finite generation (with a pointer to Mathlib's DedekindDomain.SelmerGroup K(S,n) and its finiteness TODO); Sel_m(E/K) is Layer 7's effective refinement. Having found Stoll's repository (point 10), I checked: this is exactly his formalised route (Heights/WeakMordellWeil.lean, finite_index_range_nsmulAddMonoidHom_two). The Ordering section now truthfully says the ordering is the dependency order.

8. The cohomology gap is now stated precisely, citing what pinned Mathlib has (Algebra/Category/ContinuousCohomology/, the RepresentationTheory/Homological/GroupCohomology/ suite with low-degree API, LES, Shapiro, Hilbert 90, and CategoryTheory/Sites/NonabelianCohomology/H1.lean) and listing the four missing Galois-specific pieces: profinite groups on discrete modules with the finite-level comparison, the Kummer connecting map/exact sequence for [m], inflation–restriction in that setting, and localisation at places for the local conditions.

9. Torsion milestone restated as the module fact: torsion_linearEquiv_prod is now a ZMod N-linear equivalence with (ZMod N)² (free of rank 2), using Mathlib's AddSubgroup.torsionBy.zmodModule as a local instance (it is a plain def upstream — reducibly the same subgroup as the Submodule.torsionBy convention); the docstring explains the Nonempty wrapper (noncanonical basis) and the automatic-linearity remark. Elaborates against pinned Mathlib; build green.

Provenance.

10. Pinned sources block added: AINTLIB dev/modular-curves @ 50d5f9d3 and dev/hasse-weil @ 513e8387 (public; no license file — it's my repository, and Apache-2.0 licensing of the migrated material is stated as part of the migration contract); FLT #1088 merged as bc2fe8ff (Apache-2.0); and Stoll's development located at MichaelStollBayreuth/Heights @ 678f4614 — fg_point / fg_point_of_numberField, sorry-free, under [W.IsShortNF] (porting note added for the reduction to short normal form). ⚠ That repo is GPL-2.0, which is incompatible with Apache-2.0, so the roadmap explicitly treats it as a model-to-follow rather than code-to-copy until relicensing/contribution is agreed (Kevin has offered to coordinate, above in this thread).

11. Both staleness bugs fixed: Algebra.IsQuadraticExtension is stated as being in pinned Mathlib (LinearAlgebra/Dimension/StrongRankCondition.lean) with FLT consuming it directly — no porting adjustment at all; and the HasseBound paths are reconciled — the capstone is HasseWeil/WeilPairing/HasseBound.lean (README was right, Suggested.lean pointed at the sibling HasseWeil/HasseBound.lean, which is the conditional skeleton — now disambiguated in both). The axiom claim (propext, Classical.choice, Quot.sound) is tied to the pinned revision and marked as a documented in-repo check to become a CI gate on porting.

12. hasse_bound's finiteness dependency is explicit: the docstring (and Layer 3) now present finite_point as the required companion — Nat.card of an infinite type is 0, so the inequality would be false-not-vacuous, and any proof necessarily establishes finiteness. I kept the statement free of a redundant [Finite …] hypothesis, per your "presented together" alternative. And char K ∤ N is now stated wherever the nondegenerate pairing / full N-torsion theory is invoked.

One more fix of the same species, found while auditing point 10: the pinned modular-curves branch has a sorry-free construction of the invariant differential ω_{E/S} as a glued line bundle (InvariantDifferential.lean), so the closing "not yet formalised anywhere" claim now covers only its isogeny functoriality, the formal group, Néron models, and Tate's algorithm.

[Multramate]

I think this roadmap is still far too broad and includes many subprojects, in accordance to @kbuzzard's comment that we should have a separate roadmap for complex uniformisation. Primarily, most of the theory here can be developed orthogonally to developing group schemes and models, including isogenies and the Weil pairing. I don't know if this in scope of TauCeti, but the definitions in mathlib are still subpar and could use some improvement, so maybe it's possible to experiment here.

[CBirkbeck]

[Comment written by Claude Fable 5, the AI agent working on this roadmap, posting from Chris's account — not by Chris.]

@Multramate — responding to the review verdict: the roadmap has been rebuilt to do what it asks, in 1a5a138 + 3ec5ceb.

• Orthogonal to group schemes and models. The scheme layer is gone entirely. An isogeny is now your function-field definition (pullback : W₂.FunctionField →ₐ[K] W₁.FunctionField with inducedPlace pullback W₁.infinityPlace = W₂.infinityPlace); Layer 0 is the places/divisors dictionary over Mathlib's existing CoordinateRing/FunctionField/toClass (new seed: toClass_surjective); the Weil pairing and everything downstream is developed with no schemes anywhere. Degrees become Module.finrank, separability becomes field theory, and Frobenius is f ↦ f^q.
• Narrower. Néron models are out of scope (a future scheme-facing roadmap), complex uniformisation was already dropped, and the mathlib-track items — the E[N] structure, the Tate module, Tate's algorithm/conductor, the division-polynomial [n]-formulas — are kept only under an explicit build-then-dedupe convention, so nothing here competes with upstream work.
• "Maybe it's possible to experiment here." That is now explicitly this roadmap's job: it adopts your definition and coordinates with your in-flight isogeny/Weil-pairing development rather than forking it — wherever your upstream lands first, the roadmap consumes it and deletes the duplication.

Every inline comment has a threaded reply describing the specific change. One open ask: the PR number for the finite-extension twist point isomorphism (thread on the Layer 5 bullet).