Elliptic curve definitions bridging LMFDB knowls to Lean - #71
Open
JaneShi99 wants to merge 13 commits into
Open
Conversation
…ge ch.4) Mathlib-style definitions from LMFDB elliptic-curve knowls that are not yet in mathlib: additive / multiplicative / bad / potential-good reduction; good-ordinary / good-supersingular reduction; split / non-split multiplicative reduction; plus the finite-field building blocks traceOfFrobenius / IsOrdinary / IsSupersingular. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…h.4 EC) Extends ForMathlib/4-EC.lean with the global (Dedekind-domain) minimal-model cluster — IsGlobalMinimalModel, IsSemiGlobalMinimalModel, minimalDiscriminantIdeal, IsReducedMinimalModel, IsSemistable, and obstructionExponent/obstructionClass (Silverman's Weierstrass class) — plus the ReductionType enum and the one-offs naiveHeight, naivePointHeight/canonicalHeight, freyCurve, abcQuality, and integralPoints. All compile. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Replaces @IsOrdinary/@IsSupersingular instance passing in IsGoodOrdinaryReduction / IsGoodSupersingularReduction with 'haveI := h; (W.reduction R).IsOrdinary' (dot notation), and the brittle positional pattern '@Affine.Point.some _ _ _ x _ _' in naivePointHeight with the named binder '.some (x := x) ..'. No change in meaning; compiles. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Multramate
requested changes
Jun 19, 2026
Multramate
left a comment
Collaborator
There was a problem hiding this comment.
Some preliminary comments for reductions.
This was referenced Jun 28, 2026
Compile fixes after merging main (v4.23.0 -> v4.31.0): update moved/deprecated imports (RingTheory.Radical -> .NatInt, RingTheory.ClassGroup -> .Basic; drop the split Module.Torsion imports); IsGoodReduction -> HasGoodReduction (deprecated); Affine.Point.some now takes coordinates explicitly; drop redundant [IsDomain O] (IsDedekindDomain implies it). Remove mordellWeilGenerators: its Module.Free (M / torsion) instance chain no longer synthesizes in v4.31.0, and it is the def flagged in PR review (do we need the basis of generators?) - set aside pending that decision. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…pe (ch.4 EC) Following review by Multramate (mathlib EC maintainer), now that the branch is on mathlib v4.31.0 which has the reduction API: drop IsAdditiveReduction/IsMultiplicativeReduction/IsSplitMultiplicativeReduction in favour of mathlib's HasAdditiveReduction/HasMultiplicativeReduction/HasSplitMultiplicativeReduction; rebuild IsNonsplitMultiplicativeReduction as HasMultiplicativeReduction and not HasSplitMultiplicativeReduction (drops the [Finite] hypothesis and point-count); IsSemistable uses HasAdditiveReduction; IsBadReduction = not HasGoodReduction. Define IsSupersingular first, IsOrdinary := not IsSupersingular. Restructure ReductionType to good | multiplicative (split : Bool) | additive. IsPotentialGoodReduction keeps the j-invariant criterion (the base-change form needs the finite-extension/DVR-tower machinery; j integral is the equivalent characterization, Silverman AEC VII.5.5). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
….4 EC) Replace the j-invariant criterion with the base-change form requested in PR review: there exists a DVR S extending R (compatible R->S->Frac S and R->K->Frac S towers) whose fraction field is a finite extension of K over which W has good reduction. Expressed as a single existential over S (no helper structure / Nonempty wrapper); S is universe-pinned to K. Silverman AEC VII.5.5 gives the equivalence with j(E) integral. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
tb65536
reviewed
Jun 29, 2026
tb65536
reviewed
Jun 29, 2026
tb65536
reviewed
Jun 29, 2026
Multramate
reviewed
Jun 30, 2026
Multramate
reviewed
Jun 30, 2026
Multramate
reviewed
Jun 30, 2026
Multramate
reviewed
Jun 30, 2026
Multramate
reviewed
Jun 30, 2026
Multramate
reviewed
Jun 30, 2026
Multramate
reviewed
Jun 30, 2026
Multramate
reviewed
Jun 30, 2026
|
|
||
| variable {O : Type*} [CommRing O] [IsDedekindDomain O] | ||
|
|
||
| /-- A Weierstrass model over `K = FractionRing O` (with `O` the ring of integers, a Dedekind domain) |
Collaborator
There was a problem hiding this comment.
If you notice in the definition of IsMinimal etc, we want to have an "AKLB" construction rather than a fixed ring and a fixed fraction ring. So the assumptions will need to be a Dedekind domain R, a field K such that IsFractionRing R K (not K = FractionRing R), etc
Author
There was a problem hiding this comment.
@Multramate I did have the AKLB construction, but it costed a few lines of local instance. See the updated file.
Multramate
reviewed
Jun 30, 2026
1. used "isGalobalMinimal" instead of "isGlobalMinimalModel" to match
the mathlib naming for "isMinimal"
2. local instance to get rid of the "HaveI"s
3. since IsMinimal -> IsIntegral, no longer has IsIntegral in the
hypothesis
Multramate
approved these changes
Sep 1, 2026
Multramate
left a comment
Collaborator
There was a problem hiding this comment.
I will approve this for now, because we want to get this merged asap (sorry for the delays!), and I don't know if this will ever be superseded by stuff in Tau Ceti. We want to get this into mathlib eventually, but you would have to make the PR there instead of here anyway.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds Lean definitions to
LeanBridge/ForMathlib/4-EC.leanfor LMFDB elliptic-curve knowls (blueprint chapter 4) that are not yet in mathlib, written in mathlib style.What's added
IsAdditiveReduction,IsMultiplicativeReduction,IsBadReduction,IsPotentialGoodReduction,IsGood{Ordinary,Supersingular}Reduction,Is{Split,NonsplitMultiplicative}Reduction, the finite-field blockstraceOfFrobenius,IsOrdinary,IsSupersingular, and theReductionTypeenum.IsGlobalMinimalModel,IsSemiGlobalMinimalModel,minimalDiscriminantIdeal,localMinimalDiscriminant,IsReducedMinimalModel(/ℚ),IsSemistable, andobstructionClass/obstructionExponent(Silverman's Weierstrass class, AEC §VIII.8).
mordellWeilGenerators,naiveHeight,naivePointHeight/canonicalHeight,freyCurve,abcQuality,integralPoints.All compile (
lake build LeanBridge.ForMathlib.«4-EC»). Each docstring documents the modelingchoices and caveats (totality/junk-value conventions, unproven facts taken as hypotheses).
🤖 Generated with Claude Code