From 641a2d5add1e1e0c663be65f72df91a15501e27a Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Sun, 14 Jun 2026 23:16:34 -0400 Subject: [PATCH 01/12] feat(ForMathlib): elliptic-curve reduction-type definitions (LeanBridge 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) --- LeanBridge.lean | 1 + LeanBridge/ForMathlib/4-EC.lean | 112 ++++++++++++++++++++++++++++++++ 2 files changed, 113 insertions(+) create mode 100644 LeanBridge/ForMathlib/4-EC.lean diff --git a/LeanBridge.lean b/LeanBridge.lean index 9009ac5d..a91d2c3e 100644 --- a/LeanBridge.lean +++ b/LeanBridge.lean @@ -1 +1,2 @@ import LeanBridge.Example +import LeanBridge.ForMathlib.«4-EC» diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean new file mode 100644 index 00000000..00bf8e32 --- /dev/null +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -0,0 +1,112 @@ +import Mathlib.AlgebraicGeometry.EllipticCurve.Reduction +import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point + +/-! +# Elliptic curve definitions for LeanBridge (chapter 4) + +Definitions from the LMFDB elliptic-curve knowls that are not (yet) in mathlib, written here in +mathlib style for the LeanBridge blueprint audit. +-/ + +namespace WeierstrassCurve + +open IsLocalRing + +section FiniteField + +variable {F : Type*} [Field F] [Finite F] + +/-- The trace of Frobenius `aₚ = #F + 1 − #E(F)` of an elliptic curve over a finite field `F`. +(`Nat.card` gives the true cardinality since `F` is finite.) -/ +noncomputable def traceOfFrobenius (E : WeierstrassCurve F) [E.IsElliptic] : ℤ := + (Nat.card F : ℤ) + 1 - Nat.card E.toAffine.Point + +/-- An elliptic curve over a finite field is **ordinary** if its characteristic `p` does not divide +its trace of Frobenius `aₚ`. This is the divisibility `p ∤ aₚ`, *not* `aₚ ≠ 0`: for `p ≥ 5` the two +agree, but in characteristic 2 and 3 they differ, and divisibility is the correct criterion +(see `IsSupersingular`). -/ +def IsOrdinary (E : WeierstrassCurve F) [E.IsElliptic] : Prop := + ¬ (ringChar F : ℤ) ∣ traceOfFrobenius E + +/-- An elliptic curve over a finite field is **supersingular** if its characteristic `p` divides its +trace of Frobenius `aₚ`. The criterion is `p ∣ aₚ`, **not** `aₚ = 0`: for `p ≥ 5` these coincide +(Hasse gives `|aₚ| ≤ 2√q < p`), but in characteristic 2 and 3 `|aₚ|` can reach or exceed `p` +(e.g. `aₚ = ±2` at `p = 2`), where `aₚ = 0` would misclassify. `p ∣ aₚ` is correct in all +characteristics (Silverman, *Arithmetic of Elliptic Curves*, V.3.1). -/ +def IsSupersingular (E : WeierstrassCurve F) [E.IsElliptic] : Prop := + (ringChar F : ℤ) ∣ traceOfFrobenius E + +end FiniteField + +section Reduction + +variable (R : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] +variable {K : Type*} [Field K] [Algebra R K] [IsFractionRing R K] + +/-- A minimal Weierstrass curve over `K` has **additive reduction** (LMFDB `ec.additive_reduction`) +if its reduction over the residue field of `R` has a cuspidal singularity. Equivalently, both the +discriminant `Δ` and the invariant `c₄` of the reduced curve vanish: a singular Weierstrass curve +has a cusp iff `c₄ = 0` and a node iff `c₄ ≠ 0` (Silverman, *Arithmetic of Elliptic Curves*, III), +a criterion that is independent of the residue characteristic. -/ +@[mk_iff] +class IsAdditiveReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop where + additive : (W.reduction R).Δ = 0 ∧ (W.reduction R).c₄ = 0 + +/-- A minimal Weierstrass curve over `K` has **bad reduction** (LMFDB `ec.bad_reduction`) if its +reduction over the residue field of `R` is singular — equivalently, it does not have good +reduction. -/ +def IsBadReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop := + ¬ IsGoodReduction R W + +/-- A minimal Weierstrass curve over `K` has **multiplicative reduction** (LMFDB +`ec.multiplicative_reduction`) if its reduction over the residue field of `R` has a nodal +singularity: the discriminant `Δ` of the reduced curve vanishes but `c₄` does not. -/ +@[mk_iff] +class IsMultiplicativeReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop where + multiplicative : (W.reduction R).Δ = 0 ∧ (W.reduction R).c₄ ≠ 0 + +/-- A Weierstrass curve over `K` (with `R` a DVR, `K = Frac R`) has **potential good reduction** +(LMFDB `ec.potential_good_reduction`) if its `j`-invariant is integral, i.e. lies in `R`. By the +knowl / Silverman AEC VII.5.5 this is equivalent to `E` acquiring good reduction over a finite +extension. -/ +def IsPotentialGoodReduction (W : WeierstrassCurve K) [W.IsElliptic] : Prop := + ∃ r : R, algebraMap R K r = W.j + +/-- A minimal Weierstrass curve over `K` (with finite residue field) has **good ordinary reduction** +(LMFDB `ec.good_ordinary_reduction`) if it has good reduction and the reduced elliptic curve is +ordinary. (Ordinary uses `p ∤ aₚ`, the characteristic-independent criterion; see `IsOrdinary`.) -/ +def IsGoodOrdinaryReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) [IsMinimal R W] : + Prop := + ∃ h : (W.reduction R).IsElliptic, @IsOrdinary _ _ (W.reduction R) h + +/-- A minimal Weierstrass curve over `K` (with finite residue field) has **good supersingular +reduction** (LMFDB `ec.good_supersingular_reduction`) if it has good reduction and the reduced +elliptic curve is supersingular. (Uses `p ∣ aₚ`, not `aₚ = 0` — correct in char 2 and 3; see +`IsSupersingular`.) -/ +def IsGoodSupersingularReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) + [IsMinimal R W] : Prop := + ∃ h : (W.reduction R).IsElliptic, @IsSupersingular _ _ (W.reduction R) h + +/-- A minimal Weierstrass curve over `K` (with finite residue field) has **split multiplicative +reduction** (LMFDB `ec.split_multiplicative_reduction`) if it has multiplicative reduction whose +reduced curve's nonsingular points form `𝔾ₘ`, i.e. number `#𝔽 − 1`. This point-count criterion is +characteristic-independent: the smooth locus of a nodal cubic is `𝔾ₘ` (split) or the non-split +torus (non-split), of order `#𝔽 ∓ 1` in every characteristic — no tangent-cone analysis is +involved, so the char 2/3 subtleties do not arise. -/ +def IsSplitMultiplicativeReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) + [IsMinimal R W] : Prop := + IsMultiplicativeReduction R W ∧ + Nat.card (W.reduction R).toAffine.Point = Nat.card (ResidueField R) - 1 + +/-- A minimal Weierstrass curve over `K` (with finite residue field) has **non-split multiplicative +reduction** (LMFDB `ec.nonsplit_multiplicative_reduction`) if it has multiplicative reduction with +`#Ẽ_ns(𝔽) = #𝔽 + 1` (the non-split torus). Like `IsSplitMultiplicativeReduction`, this point count +is characteristic-independent. -/ +def IsNonsplitMultiplicativeReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) + [IsMinimal R W] : Prop := + IsMultiplicativeReduction R W ∧ + Nat.card (W.reduction R).toAffine.Point = Nat.card (ResidueField R) + 1 + +end Reduction + +end WeierstrassCurve From 4384c2f4c768a857add9374322be5a22c1c6f554 Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Thu, 18 Jun 2026 22:30:34 -0400 Subject: [PATCH 02/12] Add global minimal-model, height, Frey, and obstruction-class defs (ch.4 EC) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- LeanBridge/ForMathlib/4-EC.lean | 208 ++++++++++++++++++++++++++++++++ 1 file changed, 208 insertions(+) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index 00bf8e32..d849a4f9 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -1,5 +1,16 @@ import Mathlib.AlgebraicGeometry.EllipticCurve.Reduction import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point +import Mathlib.LinearAlgebra.FreeModule.PID +import Mathlib.Algebra.Module.Torsion +import Mathlib.RingTheory.DedekindDomain.Dvr +import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas +import Mathlib.RingTheory.Localization.LocalizationLocalization +import Mathlib.Algebra.BigOperators.Finprod +import Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms +import Mathlib.RingTheory.Radical +import Mathlib.RingTheory.UniqueFactorizationDomain.Nat +import Mathlib.Analysis.SpecialFunctions.Log.Basic +import Mathlib.RingTheory.ClassGroup /-! # Elliptic curve definitions for LeanBridge (chapter 4) @@ -107,6 +118,203 @@ def IsNonsplitMultiplicativeReduction [Finite (ResidueField R)] (W : Weierstrass IsMultiplicativeReduction R W ∧ Nat.card (W.reduction R).toAffine.Point = Nat.card (ResidueField R) + 1 +/-- The **local minimal discriminant** of `E` at the prime of the DVR `R` (LMFDB +`ec.local_minimal_discriminant`): the ideal `𝔭^e` of `R` generated by the discriminant of a local +minimal model `W.minimal R`, where `e` is that discriminant's valuation at the prime. -/ +noncomputable def localMinimalDiscriminant (W : WeierstrassCurve K) : Ideal R := + Ideal.span {(integralModel R (W.minimal R)).Δ} + +/-- The **reduction type** (LMFDB `ec.reduction_type`) of an elliptic curve at a prime: the +classification realized by the reduction-cluster predicates `IsGoodOrdinaryReduction`, +`IsGoodSupersingularReduction`, `IsSplitMultiplicativeReduction`, `IsNonsplitMultiplicativeReduction` +and `IsAdditiveReduction`. Assigning the type to a given `(curve, prime)` requires the trichotomy +that exactly one of these holds (a classification theorem), which is not provided here. -/ +inductive ReductionType + | goodOrdinary + | goodSupersingular + | splitMultiplicative + | nonsplitMultiplicative + | additive + end Reduction +section MordellWeil + +variable {K : Type*} [Field K] [DecidableEq K] + +/-- Given that `E(K)` is finitely generated — the **Mordell–Weil theorem**, taken here as the +hypothesis `[Module.Finite ℤ (Affine.Point W)]` since it is not proven in mathlib — the +**Mordell–Weil generators** (LMFDB `ec.mw_generators`) of `E/K` are a basis of the free part +`E(K) ⧸ torsion`. That quotient is finitely generated and torsion-free over the PID `ℤ`, hence free, +so it has a basis; these are the `rank`-many points generating `E(K)` modulo torsion. -/ +noncomputable def mordellWeilGenerators (W : WeierstrassCurve K) [W.IsElliptic] + [Module.Finite ℤ (Affine.Point W)] := + Module.Free.chooseBasis ℤ (Affine.Point W ⧸ Submodule.torsion ℤ (Affine.Point W)) + +end MordellWeil + +section GlobalMinimal + +open IsDedekindDomain + +variable {O : Type*} [CommRing O] [IsDomain O] [IsDedekindDomain O] + +/-- A Weierstrass model over `K = FractionRing O` (with `O` the ring of integers, a Dedekind domain) +is a **global minimal model** (LMFDB `ec.global_minimal_model`) if it is integral over `O` and is a +local minimal model at every nonzero prime of `O`. mathlib only has the *local* minimal-model theory +(`IsMinimal` over one DVR); this is the global assembly over all primes. The localization +`Localization.AtPrime v.asIdeal` of a Dedekind domain at a nonzero prime is a DVR with fraction field +`FractionRing O`, so `IsMinimal` applies at each `v`. -/ +def IsGlobalMinimalModel (W : WeierstrassCurve (FractionRing O)) : Prop := + IsIntegral O W ∧ ∀ v : HeightOneSpectrum O, + haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := + IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ + IsMinimal (Localization.AtPrime v.asIdeal) W + +/-- A Weierstrass model over `K = FractionRing O` is a **semi-global minimal model** (LMFDB +`ec.semi_global_minimal_model`) if it is integral over `O` and a local minimal model at every +nonzero prime of `O` except possibly one. Over a number field of class number greater than one an +elliptic curve may have no `IsGlobalMinimalModel`, but it always has a semi-global one; the +exceptional prime carries the obstruction class. (The knowl further records that at that prime the +discriminant valuation exceeds the minimal-discriminant valuation by `12`; that is a consequence +phrased via the minimal-discriminant ideal, so it is not part of this defining predicate.) -/ +def IsSemiGlobalMinimalModel (W : WeierstrassCurve (FractionRing O)) : Prop := + IsIntegral O W ∧ ∃ v₀ : HeightOneSpectrum O, ∀ v : HeightOneSpectrum O, v ≠ v₀ → + haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := + IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ + IsMinimal (Localization.AtPrime v.asIdeal) W + +/-- The **minimal discriminant ideal** (LMFDB `ec.minimal_discriminant`) of `E` over `O`: +`𝔡_min = ∏_v v ^ e_v`, the product over all nonzero primes `v` of `O` of `v ^ e_v`, where `e_v` is +the valuation of the discriminant of a local minimal model at `v` — the `v`-part of the local +minimal discriminant (cf. `localMinimalDiscriminant`). At a prime of good reduction `e_v = 0`, which +holds for all but finitely many `v`, so the (a priori infinite) product is finite. If `E` has a +`IsGlobalMinimalModel` then `𝔡_min = (Δ)`, the principal ideal of that model's discriminant. -/ +noncomputable def minimalDiscriminantIdeal (W : WeierstrassCurve (FractionRing O)) : Ideal O := + ∏ᶠ v : HeightOneSpectrum O, + v.asIdeal ^ + (haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := + IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ + ((IsDiscreteValuationRing.addVal (Localization.AtPrime v.asIdeal)) + ((integralModel _ (W.minimal (Localization.AtPrime v.asIdeal))).Δ)).toNat) + +/-- The unique **reduced minimal Weierstrass model** over `ℚ` (LMFDB +`ec.q.minimal_weierstrass_equation`): a global minimal model over `ℤ` whose coefficients are +normalized by `a₁, a₃ ∈ {0, 1}` and `a₂ ∈ {-1, 0, 1}`. These constraints single out the unique +representative among the global minimal models of `E / ℚ` (which differ by the integral variable +changes `[±1, r, s, t]`). The bare minimality is `IsGlobalMinimalModel` at `O := ℤ`; this adds the +canonical normal form. -/ +def IsReducedMinimalModel (W : WeierstrassCurve (FractionRing ℤ)) : Prop := + IsGlobalMinimalModel W ∧ + (W.a₁ = 0 ∨ W.a₁ = 1) ∧ (W.a₂ = -1 ∨ W.a₂ = 0 ∨ W.a₂ = 1) ∧ (W.a₃ = 0 ∨ W.a₃ = 1) + +/-- An elliptic curve over `K = FractionRing O` is **semistable** (LMFDB `ec.semistable`) if it has +no additive reduction at any prime of `O` — equivalently, good or multiplicative reduction +everywhere, i.e. multiplicative reduction at every bad prime. The reduction at `v` is read off the +local minimal model `W.minimal (Localization.AtPrime v.asIdeal)`. -/ +def IsSemistable (W : WeierstrassCurve (FractionRing O)) : Prop := + ∀ v : HeightOneSpectrum O, + haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := + IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ + ¬ IsAdditiveReduction (Localization.AtPrime v.asIdeal) + (W.minimal (Localization.AtPrime v.asIdeal)) + +/-- The **obstruction exponent** `fᵥ = (vᵥ(Δ) − eᵥ)/12` at a prime `v` for an integral model `W` +over `O`: the `v`-adic valuation of this model's discriminant minus the local minimal discriminant +valuation `eᵥ`, divided by `12` (an exact division, since two integral models' discriminant +valuations differ by a multiple of `12`). -/ +noncomputable def obstructionExponent (W : WeierstrassCurve O) (v : HeightOneSpectrum O) : ℕ := + haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := + IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ + ((IsDiscreteValuationRing.addVal (Localization.AtPrime v.asIdeal) + (algebraMap O (Localization.AtPrime v.asIdeal) W.Δ)).toNat - + (IsDiscreteValuationRing.addVal (Localization.AtPrime v.asIdeal) + (integralModel _ + ((W.baseChange (FractionRing O)).minimal (Localization.AtPrime v.asIdeal))).Δ).toNat) / 12 + +/-- The **obstruction class** (Silverman's *Weierstrass class*, LMFDB `ec.obstruction_class`) of an +integral model `W` over `O`: the ideal class `[∏ᵥ 𝔭ᵥ^{fᵥ}] ∈ ClassGroup O`, where `𝔞 = ∏ᵥ 𝔭ᵥ^{fᵥ}` +satisfies `𝔞¹² = (Δ)·𝔇_min⁻¹` (Silverman, *The Arithmetic of Elliptic Curves*, VIII.8). It is trivial +iff `E` has a global minimal model. The product is taken inside the non-zero-divisor submonoid, so +each `𝔭ᵥ^{fᵥ}` carries its own nonzero proof (`pow_mem` of the prime `𝔭ᵥ ≠ ⊥`). -/ +noncomputable def obstructionClass (W : WeierstrassCurve O) : ClassGroup O := + ClassGroup.mk0 (∏ᶠ v : HeightOneSpectrum O, + (⟨v.asIdeal ^ obstructionExponent W v, + pow_mem (mem_nonZeroDivisors_of_ne_zero (by simpa using v.ne_bot)) _⟩ : + nonZeroDivisors (Ideal O))) + +end GlobalMinimal + +section Height + +/-- The **naive height** (LMFDB `ec.q.naive_height`) of an elliptic curve over `ℚ` in short +Weierstrass form `y² = x³ + a₄x + a₆`: the quantity `max (4|a₄|³, 27|a₆|²)`. The `[W.IsShortNF]` +instance enforces the short-form requirement (`a₁ = a₂ = a₃ = 0`); a general curve must first be put +in short form (`W.toShortNF • W`) since the naive height depends on the chosen model. -/ +def naiveHeight (W : WeierstrassCurve ℚ) [W.IsShortNF] : ℚ := + max (4 * |W.a₄| ^ 3) (27 * |W.a₆| ^ 2) + +/-- The **naive height** of a rational point `P ∈ E(ℚ)`: `log max(|num x(P)|, |den x(P)|)`, the +height of its `x`-coordinate (and `0` at the point at infinity). -/ +noncomputable def naivePointHeight {W : WeierstrassCurve ℚ} : W.toAffine.Point → ℝ + | .zero => 0 + | @Affine.Point.some _ _ _ x _ _ => Real.log (max (x.num.natAbs : ℝ) (x.den : ℝ)) + +open Filter in +/-- The **canonical (Néron–Tate) height** (LMFDB `ec.q.canonical_height`) of a rational point: +`ĥ(P) = limₙ (1/n²) · log max(|Aₙ|, |Dₙ|)` where `x(nP) = Aₙ/Dₙ` in lowest terms — i.e. the limit of +`naivePointHeight (n • P) / n²`. (This is LMFDB's normalization; some sources halve it.) The limit +uses `limUnder`, which returns a junk value if the sequence diverges; convergence (the Néron–Tate +theorem) holds but is *not* proved here, so this definition captures the defining formula and gives +the correct real value, but is inert in proofs until convergence is established. -/ +noncomputable def canonicalHeight {W : WeierstrassCurve ℚ} [W.IsElliptic] + (P : W.toAffine.Point) : ℝ := + limUnder atTop (fun n : ℕ => naivePointHeight (n • P) / (n : ℝ) ^ 2) + +end Height + +section Frey + +/-- The **Frey–Hellegouarch curve** (LMFDB `ec.q.frey`) of a pair `A, B` (from a triple with +`A + B = C`): the curve `y² = x(x - A)(x + B)`. Expanding `x(x - A)(x + B) = x³ + (B - A)x² - A*B*x` +gives the Weierstrass coefficients `a₂ = B - A`, `a₄ = -A*B`, with `a₁ = a₃ = a₆ = 0`. Its +discriminant is `Δ = 16*A²*B²*(A + B)²`, so it is an elliptic curve exactly when `A`, `B`, `A + B` +are all nonzero. -/ +def freyCurve {R : Type*} [CommRing R] (A B : R) : WeierstrassCurve R where + a₁ := 0 + a₂ := B - A + a₃ := 0 + a₄ := -(A * B) + a₆ := 0 + +end Frey + +section Quality + +/-- The **abc quality** (LMFDB `ec.q.abc_quality`) of an elliptic curve over `ℚ`: +`log max(|a|, |b|, |c|) / log rad(abc)`, where `j/1728 = a/c` is in lowest terms and `b = c - a` +(`rad` is the radical, the product of the primes dividing its argument). The quality is undefined at +`j = 0` and `j = 1728`: there `a*b*c = 0`, so `rad = 1`, `log 1 = 0`, and the value is the junk `0` +(Lean's `x / 0 = 0`). Needs `[E.IsElliptic]` for the `j`-invariant. -/ +noncomputable def abcQuality (E : WeierstrassCurve ℚ) [E.IsElliptic] : ℝ := + let a := (E.j / 1728).num + let c := ((E.j / 1728).den : ℤ) + let b := c - a + Real.log ↑(max (max a.natAbs b.natAbs) c.natAbs) / + Real.log ↑(UniqueFactorizationMonoid.radical (a * b * c).natAbs) + +end Quality + +section Points + +/-- The **integral points** (LMFDB `ec.q.integral_points`) of a given model `W` of an elliptic curve +over `ℚ`: the affine points `(x, y)` of `W` with integral coordinates `x, y ∈ ℤ`. (The point at +infinity is excluded, having no affine coordinates.) The knowl's "integral points on a minimal model" +is then `integralPoints` of the global minimal model; the set is finite by Siegel's theorem, which is +not part of this definition. -/ +def integralPoints (W : WeierstrassCurve ℚ) : Set W.toAffine.Point := + {P | ∃ (x y : ℤ) (h : W.toAffine.Nonsingular (x : ℚ) (y : ℚ)), P = Affine.Point.some h} + +end Points + end WeierstrassCurve From f0c17b0b4c32bcba58806423af9298494de95e4b Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Thu, 18 Jun 2026 22:41:46 -0400 Subject: [PATCH 03/12] Clean up reduction/height defs to mathlib-idiomatic form (ch.4 EC) 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) --- LeanBridge/ForMathlib/4-EC.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index d849a4f9..7ec7909e 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -88,7 +88,7 @@ def IsPotentialGoodReduction (W : WeierstrassCurve K) [W.IsElliptic] : Prop := ordinary. (Ordinary uses `p ∤ aₚ`, the characteristic-independent criterion; see `IsOrdinary`.) -/ def IsGoodOrdinaryReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) [IsMinimal R W] : Prop := - ∃ h : (W.reduction R).IsElliptic, @IsOrdinary _ _ (W.reduction R) h + ∃ h : (W.reduction R).IsElliptic, haveI := h; (W.reduction R).IsOrdinary /-- A minimal Weierstrass curve over `K` (with finite residue field) has **good supersingular reduction** (LMFDB `ec.good_supersingular_reduction`) if it has good reduction and the reduced @@ -96,7 +96,7 @@ elliptic curve is supersingular. (Uses `p ∣ aₚ`, not `aₚ = 0` — correct `IsSupersingular`.) -/ def IsGoodSupersingularReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) [IsMinimal R W] : Prop := - ∃ h : (W.reduction R).IsElliptic, @IsSupersingular _ _ (W.reduction R) h + ∃ h : (W.reduction R).IsElliptic, haveI := h; (W.reduction R).IsSupersingular /-- A minimal Weierstrass curve over `K` (with finite residue field) has **split multiplicative reduction** (LMFDB `ec.split_multiplicative_reduction`) if it has multiplicative reduction whose @@ -258,7 +258,7 @@ def naiveHeight (W : WeierstrassCurve ℚ) [W.IsShortNF] : ℚ := height of its `x`-coordinate (and `0` at the point at infinity). -/ noncomputable def naivePointHeight {W : WeierstrassCurve ℚ} : W.toAffine.Point → ℝ | .zero => 0 - | @Affine.Point.some _ _ _ x _ _ => Real.log (max (x.num.natAbs : ℝ) (x.den : ℝ)) + | .some (x := x) .. => Real.log (max (x.num.natAbs : ℝ) (x.den : ℝ)) open Filter in /-- The **canonical (Néron–Tate) height** (LMFDB `ec.q.canonical_height`) of a rational point: From e899f9a1e2eb01c1cab2b131ff07bd2d72ddd019 Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Mon, 29 Jun 2026 00:50:56 +0100 Subject: [PATCH 04/12] Sync ForMathlib/4-EC.lean to mathlib v4.31.0 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) --- LeanBridge/ForMathlib/4-EC.lean | 27 +++++---------------------- 1 file changed, 5 insertions(+), 22 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index 7ec7909e..87f6df54 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -1,16 +1,14 @@ import Mathlib.AlgebraicGeometry.EllipticCurve.Reduction import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point -import Mathlib.LinearAlgebra.FreeModule.PID -import Mathlib.Algebra.Module.Torsion import Mathlib.RingTheory.DedekindDomain.Dvr import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas import Mathlib.RingTheory.Localization.LocalizationLocalization import Mathlib.Algebra.BigOperators.Finprod import Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms -import Mathlib.RingTheory.Radical +import Mathlib.RingTheory.Radical.NatInt import Mathlib.RingTheory.UniqueFactorizationDomain.Nat import Mathlib.Analysis.SpecialFunctions.Log.Basic -import Mathlib.RingTheory.ClassGroup +import Mathlib.RingTheory.ClassGroup.Basic /-! # Elliptic curve definitions for LeanBridge (chapter 4) @@ -67,7 +65,7 @@ class IsAdditiveReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop where reduction over the residue field of `R` is singular — equivalently, it does not have good reduction. -/ def IsBadReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop := - ¬ IsGoodReduction R W + ¬ HasGoodReduction R W /-- A minimal Weierstrass curve over `K` has **multiplicative reduction** (LMFDB `ec.multiplicative_reduction`) if its reduction over the residue field of `R` has a nodal @@ -138,26 +136,11 @@ inductive ReductionType end Reduction -section MordellWeil - -variable {K : Type*} [Field K] [DecidableEq K] - -/-- Given that `E(K)` is finitely generated — the **Mordell–Weil theorem**, taken here as the -hypothesis `[Module.Finite ℤ (Affine.Point W)]` since it is not proven in mathlib — the -**Mordell–Weil generators** (LMFDB `ec.mw_generators`) of `E/K` are a basis of the free part -`E(K) ⧸ torsion`. That quotient is finitely generated and torsion-free over the PID `ℤ`, hence free, -so it has a basis; these are the `rank`-many points generating `E(K)` modulo torsion. -/ -noncomputable def mordellWeilGenerators (W : WeierstrassCurve K) [W.IsElliptic] - [Module.Finite ℤ (Affine.Point W)] := - Module.Free.chooseBasis ℤ (Affine.Point W ⧸ Submodule.torsion ℤ (Affine.Point W)) - -end MordellWeil - section GlobalMinimal open IsDedekindDomain -variable {O : Type*} [CommRing O] [IsDomain O] [IsDedekindDomain O] +variable {O : Type*} [CommRing O] [IsDedekindDomain O] /-- A Weierstrass model over `K = FractionRing O` (with `O` the ring of integers, a Dedekind domain) is a **global minimal model** (LMFDB `ec.global_minimal_model`) if it is integral over `O` and is a @@ -313,7 +296,7 @@ infinity is excluded, having no affine coordinates.) The knowl's "integral point is then `integralPoints` of the global minimal model; the set is finite by Siegel's theorem, which is not part of this definition. -/ def integralPoints (W : WeierstrassCurve ℚ) : Set W.toAffine.Point := - {P | ∃ (x y : ℤ) (h : W.toAffine.Nonsingular (x : ℚ) (y : ℚ)), P = Affine.Point.some h} + {P | ∃ (x y : ℤ) (h : W.toAffine.Nonsingular (x : ℚ) (y : ℚ)), P = Affine.Point.some (x : ℚ) (y : ℚ) h} end Points From 943f9abe6c4effcd547e80f3fb22811e11e5b0da Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Mon, 29 Jun 2026 10:01:15 +0100 Subject: [PATCH 05/12] Address PR review: use mathlib reduction API, restructure ReductionType (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) --- LeanBridge/ForMathlib/4-EC.lean | 72 +++++++++------------------------ 1 file changed, 20 insertions(+), 52 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index 87f6df54..9280084b 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -30,13 +30,6 @@ variable {F : Type*} [Field F] [Finite F] noncomputable def traceOfFrobenius (E : WeierstrassCurve F) [E.IsElliptic] : ℤ := (Nat.card F : ℤ) + 1 - Nat.card E.toAffine.Point -/-- An elliptic curve over a finite field is **ordinary** if its characteristic `p` does not divide -its trace of Frobenius `aₚ`. This is the divisibility `p ∤ aₚ`, *not* `aₚ ≠ 0`: for `p ≥ 5` the two -agree, but in characteristic 2 and 3 they differ, and divisibility is the correct criterion -(see `IsSupersingular`). -/ -def IsOrdinary (E : WeierstrassCurve F) [E.IsElliptic] : Prop := - ¬ (ringChar F : ℤ) ∣ traceOfFrobenius E - /-- An elliptic curve over a finite field is **supersingular** if its characteristic `p` divides its trace of Frobenius `aₚ`. The criterion is `p ∣ aₚ`, **not** `aₚ = 0`: for `p ≥ 5` these coincide (Hasse gives `|aₚ| ≤ 2√q < p`), but in characteristic 2 and 3 `|aₚ|` can reach or exceed `p` @@ -45,6 +38,12 @@ characteristics (Silverman, *Arithmetic of Elliptic Curves*, V.3.1). -/ def IsSupersingular (E : WeierstrassCurve F) [E.IsElliptic] : Prop := (ringChar F : ℤ) ∣ traceOfFrobenius E +/-- An elliptic curve over a finite field is **ordinary** if it is not supersingular, i.e. its +characteristic `p` does not divide its trace of Frobenius `aₚ` (the divisibility `p ∤ aₚ`, *not* +`aₚ ≠ 0` — see `IsSupersingular`). -/ +def IsOrdinary (E : WeierstrassCurve F) [E.IsElliptic] : Prop := + ¬ E.IsSupersingular + end FiniteField section Reduction @@ -52,28 +51,12 @@ section Reduction variable (R : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] variable {K : Type*} [Field K] [Algebra R K] [IsFractionRing R K] -/-- A minimal Weierstrass curve over `K` has **additive reduction** (LMFDB `ec.additive_reduction`) -if its reduction over the residue field of `R` has a cuspidal singularity. Equivalently, both the -discriminant `Δ` and the invariant `c₄` of the reduced curve vanish: a singular Weierstrass curve -has a cusp iff `c₄ = 0` and a node iff `c₄ ≠ 0` (Silverman, *Arithmetic of Elliptic Curves*, III), -a criterion that is independent of the residue characteristic. -/ -@[mk_iff] -class IsAdditiveReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop where - additive : (W.reduction R).Δ = 0 ∧ (W.reduction R).c₄ = 0 - /-- A minimal Weierstrass curve over `K` has **bad reduction** (LMFDB `ec.bad_reduction`) if its reduction over the residue field of `R` is singular — equivalently, it does not have good reduction. -/ def IsBadReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop := ¬ HasGoodReduction R W -/-- A minimal Weierstrass curve over `K` has **multiplicative reduction** (LMFDB -`ec.multiplicative_reduction`) if its reduction over the residue field of `R` has a nodal -singularity: the discriminant `Δ` of the reduced curve vanishes but `c₄` does not. -/ -@[mk_iff] -class IsMultiplicativeReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop where - multiplicative : (W.reduction R).Δ = 0 ∧ (W.reduction R).c₄ ≠ 0 - /-- A Weierstrass curve over `K` (with `R` a DVR, `K = Frac R`) has **potential good reduction** (LMFDB `ec.potential_good_reduction`) if its `j`-invariant is integral, i.e. lies in `R`. By the knowl / Silverman AEC VII.5.5 this is equivalent to `E` acquiring good reduction over a finite @@ -96,25 +79,11 @@ def IsGoodSupersingularReduction [Finite (ResidueField R)] (W : WeierstrassCurve [IsMinimal R W] : Prop := ∃ h : (W.reduction R).IsElliptic, haveI := h; (W.reduction R).IsSupersingular -/-- A minimal Weierstrass curve over `K` (with finite residue field) has **split multiplicative -reduction** (LMFDB `ec.split_multiplicative_reduction`) if it has multiplicative reduction whose -reduced curve's nonsingular points form `𝔾ₘ`, i.e. number `#𝔽 − 1`. This point-count criterion is -characteristic-independent: the smooth locus of a nodal cubic is `𝔾ₘ` (split) or the non-split -torus (non-split), of order `#𝔽 ∓ 1` in every characteristic — no tangent-cone analysis is -involved, so the char 2/3 subtleties do not arise. -/ -def IsSplitMultiplicativeReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) - [IsMinimal R W] : Prop := - IsMultiplicativeReduction R W ∧ - Nat.card (W.reduction R).toAffine.Point = Nat.card (ResidueField R) - 1 - -/-- A minimal Weierstrass curve over `K` (with finite residue field) has **non-split multiplicative -reduction** (LMFDB `ec.nonsplit_multiplicative_reduction`) if it has multiplicative reduction with -`#Ẽ_ns(𝔽) = #𝔽 + 1` (the non-split torus). Like `IsSplitMultiplicativeReduction`, this point count -is characteristic-independent. -/ -def IsNonsplitMultiplicativeReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) - [IsMinimal R W] : Prop := - IsMultiplicativeReduction R W ∧ - Nat.card (W.reduction R).toAffine.Point = Nat.card (ResidueField R) + 1 +/-- A minimal Weierstrass curve over `K` has **non-split multiplicative reduction** (LMFDB +`ec.nonsplit_multiplicative_reduction`) if it has multiplicative reduction that is not split — the +complement of mathlib's `HasSplitMultiplicativeReduction` within `HasMultiplicativeReduction`. -/ +def IsNonsplitMultiplicativeReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop := + HasMultiplicativeReduction R W ∧ ¬ HasSplitMultiplicativeReduction R W /-- The **local minimal discriminant** of `E` at the prime of the DVR `R` (LMFDB `ec.local_minimal_discriminant`): the ideal `𝔭^e` of `R` generated by the discriminant of a local @@ -122,16 +91,15 @@ minimal model `W.minimal R`, where `e` is that discriminant's valuation at the p noncomputable def localMinimalDiscriminant (W : WeierstrassCurve K) : Ideal R := Ideal.span {(integralModel R (W.minimal R)).Δ} -/-- The **reduction type** (LMFDB `ec.reduction_type`) of an elliptic curve at a prime: the -classification realized by the reduction-cluster predicates `IsGoodOrdinaryReduction`, -`IsGoodSupersingularReduction`, `IsSplitMultiplicativeReduction`, `IsNonsplitMultiplicativeReduction` -and `IsAdditiveReduction`. Assigning the type to a given `(curve, prime)` requires the trichotomy -that exactly one of these holds (a classification theorem), which is not provided here. -/ +/-- The **reduction type** (LMFDB `ec.reduction_type`) of an elliptic curve at a prime: **good**, +**multiplicative** (carrying a `split` boolean), or **additive** — the genuine trichotomy of +`HasGoodReduction` / `HasMultiplicativeReduction` / `HasAdditiveReduction`. (The split/non-split +distinction is attached to multiplicative reduction here; note that additive reduction can also be +split or non-split over a non-perfect residue field, which this type does not model.) Assigning the +type to a given `(curve, prime)` requires that trichotomy, which is not provided here. -/ inductive ReductionType - | goodOrdinary - | goodSupersingular - | splitMultiplicative - | nonsplitMultiplicative + | good + | multiplicative (split : Bool) | additive end Reduction @@ -199,7 +167,7 @@ def IsSemistable (W : WeierstrassCurve (FractionRing O)) : Prop := ∀ v : HeightOneSpectrum O, haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ - ¬ IsAdditiveReduction (Localization.AtPrime v.asIdeal) + ¬ HasAdditiveReduction (Localization.AtPrime v.asIdeal) (W.minimal (Localization.AtPrime v.asIdeal)) /-- The **obstruction exponent** `fᵥ = (vᵥ(Δ) − eᵥ)/12` at a prime `v` for an integral model `W` From 5cfb4e8b805d7b99689e807478deeacfac42ffcc Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Mon, 29 Jun 2026 13:58:50 +0100 Subject: [PATCH 06/12] Reformulate IsPotentialGoodReduction as a base-change existential (ch.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) --- LeanBridge/ForMathlib/4-EC.lean | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index 9280084b..47b0f877 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -48,8 +48,9 @@ end FiniteField section Reduction -variable (R : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] -variable {K : Type*} [Field K] [Algebra R K] [IsFractionRing R K] +universe u v +variable (R : Type v) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] +variable {K : Type u} [Field K] [Algebra R K] [IsFractionRing R K] /-- A minimal Weierstrass curve over `K` has **bad reduction** (LMFDB `ec.bad_reduction`) if its reduction over the residue field of `R` is singular — equivalently, it does not have good @@ -58,11 +59,17 @@ def IsBadReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop := ¬ HasGoodReduction R W /-- A Weierstrass curve over `K` (with `R` a DVR, `K = Frac R`) has **potential good reduction** -(LMFDB `ec.potential_good_reduction`) if its `j`-invariant is integral, i.e. lies in `R`. By the -knowl / Silverman AEC VII.5.5 this is equivalent to `E` acquiring good reduction over a finite -extension. -/ -def IsPotentialGoodReduction (W : WeierstrassCurve K) [W.IsElliptic] : Prop := - ∃ r : R, algebraMap R K r = W.j +(LMFDB `ec.potential_good_reduction`) if it acquires good reduction over a finite extension: there is +a discrete valuation ring `S` extending `R` (compatibly, via the scalar towers `R → S → Frac S` and +`R → K → Frac S`) whose fraction field `Frac S` is a *finite* extension of `K`, over which `W` has +good reduction. `S` lives in `K`'s universe (every finite extension of `K` does). Equivalently, by +Silverman AEC VII.5.5, `j(E) ∈ R`; this takes the base-change form requested in review. -/ +def IsPotentialGoodReduction (W : WeierstrassCurve K) : Prop := + ∃ (S : Type u) (_ : CommRing S) (_ : IsDomain S) (_ : IsDiscreteValuationRing S) + (_ : Algebra R S) (_ : Algebra R (FractionRing S)) (_ : Algebra K (FractionRing S)) + (_ : IsScalarTower R S (FractionRing S)) (_ : IsScalarTower R K (FractionRing S)) + (_ : FiniteDimensional K (FractionRing S)), + HasGoodReduction S (W.baseChange (FractionRing S)) /-- A minimal Weierstrass curve over `K` (with finite residue field) has **good ordinary reduction** (LMFDB `ec.good_ordinary_reduction`) if it has good reduction and the reduced elliptic curve is From e06c82600d25d618c4c5de24b139f85d99406a62 Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Tue, 28 Jul 2026 16:33:46 -0400 Subject: [PATCH 07/12] fixed some comments: imports, [isElliptic], --- LeanBridge/ForMathlib/4-EC.lean | 36 ++++++++++++--------------------- 1 file changed, 13 insertions(+), 23 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index 47b0f877..04f6bb60 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -1,14 +1,8 @@ -import Mathlib.AlgebraicGeometry.EllipticCurve.Reduction import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point -import Mathlib.RingTheory.DedekindDomain.Dvr -import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas -import Mathlib.RingTheory.Localization.LocalizationLocalization -import Mathlib.Algebra.BigOperators.Finprod import Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms -import Mathlib.RingTheory.Radical.NatInt -import Mathlib.RingTheory.UniqueFactorizationDomain.Nat +import Mathlib.AlgebraicGeometry.EllipticCurve.Reduction import Mathlib.Analysis.SpecialFunctions.Log.Basic -import Mathlib.RingTheory.ClassGroup.Basic +import Mathlib.RingTheory.Radical.NatInt /-! # Elliptic curve definitions for LeanBridge (chapter 4) @@ -27,7 +21,7 @@ variable {F : Type*} [Field F] [Finite F] /-- The trace of Frobenius `aₚ = #F + 1 − #E(F)` of an elliptic curve over a finite field `F`. (`Nat.card` gives the true cardinality since `F` is finite.) -/ -noncomputable def traceOfFrobenius (E : WeierstrassCurve F) [E.IsElliptic] : ℤ := +noncomputable def traceOfFrobenius (E : WeierstrassCurve F) : ℤ := (Nat.card F : ℤ) + 1 - Nat.card E.toAffine.Point /-- An elliptic curve over a finite field is **supersingular** if its characteristic `p` divides its @@ -35,13 +29,13 @@ trace of Frobenius `aₚ`. The criterion is `p ∣ aₚ`, **not** `aₚ = 0`: fo (Hasse gives `|aₚ| ≤ 2√q < p`), but in characteristic 2 and 3 `|aₚ|` can reach or exceed `p` (e.g. `aₚ = ±2` at `p = 2`), where `aₚ = 0` would misclassify. `p ∣ aₚ` is correct in all characteristics (Silverman, *Arithmetic of Elliptic Curves*, V.3.1). -/ -def IsSupersingular (E : WeierstrassCurve F) [E.IsElliptic] : Prop := +def IsSupersingular (E : WeierstrassCurve F) : Prop := (ringChar F : ℤ) ∣ traceOfFrobenius E /-- An elliptic curve over a finite field is **ordinary** if it is not supersingular, i.e. its characteristic `p` does not divide its trace of Frobenius `aₚ` (the divisibility `p ∤ aₚ`, *not* `aₚ ≠ 0` — see `IsSupersingular`). -/ -def IsOrdinary (E : WeierstrassCurve F) [E.IsElliptic] : Prop := +def IsOrdinary (E : WeierstrassCurve F) : Prop := ¬ E.IsSupersingular end FiniteField @@ -64,27 +58,23 @@ a discrete valuation ring `S` extending `R` (compatibly, via the scalar towers ` `R → K → Frac S`) whose fraction field `Frac S` is a *finite* extension of `K`, over which `W` has good reduction. `S` lives in `K`'s universe (every finite extension of `K` does). Equivalently, by Silverman AEC VII.5.5, `j(E) ∈ R`; this takes the base-change form requested in review. -/ -def IsPotentialGoodReduction (W : WeierstrassCurve K) : Prop := - ∃ (S : Type u) (_ : CommRing S) (_ : IsDomain S) (_ : IsDiscreteValuationRing S) - (_ : Algebra R S) (_ : Algebra R (FractionRing S)) (_ : Algebra K (FractionRing S)) - (_ : IsScalarTower R S (FractionRing S)) (_ : IsScalarTower R K (FractionRing S)) - (_ : FiniteDimensional K (FractionRing S)), - HasGoodReduction S (W.baseChange (FractionRing S)) +def IsPotentialGoodReduction (W : WeierstrassCurve K) [W.IsElliptic] : Prop := + ∃ r : R, algebraMap R K r = W.j /-- A minimal Weierstrass curve over `K` (with finite residue field) has **good ordinary reduction** (LMFDB `ec.good_ordinary_reduction`) if it has good reduction and the reduced elliptic curve is ordinary. (Ordinary uses `p ∤ aₚ`, the characteristic-independent criterion; see `IsOrdinary`.) -/ -def IsGoodOrdinaryReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) [IsMinimal R W] : - Prop := - ∃ h : (W.reduction R).IsElliptic, haveI := h; (W.reduction R).IsOrdinary +def IsGoodOrdinaryReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) +[HasGoodReduction R W]: Prop := + IsOrdinary (W.reduction R) /-- A minimal Weierstrass curve over `K` (with finite residue field) has **good supersingular reduction** (LMFDB `ec.good_supersingular_reduction`) if it has good reduction and the reduced elliptic curve is supersingular. (Uses `p ∣ aₚ`, not `aₚ = 0` — correct in char 2 and 3; see `IsSupersingular`.) -/ def IsGoodSupersingularReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) - [IsMinimal R W] : Prop := - ∃ h : (W.reduction R).IsElliptic, haveI := h; (W.reduction R).IsSupersingular + [HasGoodReduction R W] : Prop := + IsSupersingular (W.reduction R) /-- A minimal Weierstrass curve over `K` has **non-split multiplicative reduction** (LMFDB `ec.nonsplit_multiplicative_reduction`) if it has multiplicative reduction that is not split — the @@ -210,7 +200,7 @@ Weierstrass form `y² = x³ + a₄x + a₆`: the quantity `max (4|a₄|³, 27|a instance enforces the short-form requirement (`a₁ = a₂ = a₃ = 0`); a general curve must first be put in short form (`W.toShortNF • W`) since the naive height depends on the chosen model. -/ def naiveHeight (W : WeierstrassCurve ℚ) [W.IsShortNF] : ℚ := - max (4 * |W.a₄| ^ 3) (27 * |W.a₆| ^ 2) + max (4 * |W.a₄| ^ 3) (27 * W.a₆ ^ 2) /-- The **naive height** of a rational point `P ∈ E(ℚ)`: `log max(|num x(P)|, |den x(P)|)`, the height of its `x`-coordinate (and `0` at the point at infinity). -/ From 14b9ce20164a9f514d77ac147dac1d2863e48322 Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Tue, 28 Jul 2026 17:05:45 -0400 Subject: [PATCH 08/12] removed addVal --- LeanBridge/ForMathlib/4-EC.lean | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index 04f6bb60..ebf02257 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -140,11 +140,10 @@ holds for all but finitely many `v`, so the (a priori infinite) product is finit `IsGlobalMinimalModel` then `𝔡_min = (Δ)`, the principal ideal of that model's discriminant. -/ noncomputable def minimalDiscriminantIdeal (W : WeierstrassCurve (FractionRing O)) : Ideal O := ∏ᶠ v : HeightOneSpectrum O, - v.asIdeal ^ - (haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := - IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ - ((IsDiscreteValuationRing.addVal (Localization.AtPrime v.asIdeal)) - ((integralModel _ (W.minimal (Localization.AtPrime v.asIdeal))).Δ)).toNat) + let R := Localization.AtPrime v.asIdeal + haveI : IsDiscreteValuationRing R := + IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ + v.asIdeal ^ (-WithZero.log (v.valuation (FractionRing O) (W.minimal R).Δ)).toNat /-- The unique **reduced minimal Weierstrass model** over `ℚ` (LMFDB `ec.q.minimal_weierstrass_equation`): a global minimal model over `ℤ` whose coefficients are @@ -172,13 +171,12 @@ over `O`: the `v`-adic valuation of this model's discriminant minus the local mi valuation `eᵥ`, divided by `12` (an exact division, since two integral models' discriminant valuations differ by a multiple of `12`). -/ noncomputable def obstructionExponent (W : WeierstrassCurve O) (v : HeightOneSpectrum O) : ℕ := - haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := + let R := Localization.AtPrime v.asIdeal + haveI : IsDiscreteValuationRing R := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ - ((IsDiscreteValuationRing.addVal (Localization.AtPrime v.asIdeal) - (algebraMap O (Localization.AtPrime v.asIdeal) W.Δ)).toNat - - (IsDiscreteValuationRing.addVal (Localization.AtPrime v.asIdeal) - (integralModel _ - ((W.baseChange (FractionRing O)).minimal (Localization.AtPrime v.asIdeal))).Δ).toNat) / 12 + ((-WithZero.log (v.valuation (FractionRing O) (algebraMap O (FractionRing O) W.Δ))).toNat - + (-WithZero.log (v.valuation (FractionRing O) + ((W.baseChange (FractionRing O)).minimal R).Δ)).toNat) / 12 /-- The **obstruction class** (Silverman's *Weierstrass class*, LMFDB `ec.obstruction_class`) of an integral model `W` over `O`: the ideal class `[∏ᵥ 𝔭ᵥ^{fᵥ}] ∈ ClassGroup O`, where `𝔞 = ∏ᵥ 𝔭ᵥ^{fᵥ}` From 783e6565b9ac5a08f0a3f4accc30de76e60fafb4 Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Tue, 28 Jul 2026 17:33:57 -0400 Subject: [PATCH 09/12] changed up the comments a bit --- LeanBridge/ForMathlib/4-EC.lean | 177 +++++++++++++------------------- 1 file changed, 73 insertions(+), 104 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index ebf02257..927a04ea 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -19,22 +19,18 @@ section FiniteField variable {F : Type*} [Field F] [Finite F] -/-- The trace of Frobenius `aₚ = #F + 1 − #E(F)` of an elliptic curve over a finite field `F`. -(`Nat.card` gives the true cardinality since `F` is finite.) -/ +/-- The **trace of Frobenius** `a = #F + 1 - #E(F)` of a Weierstrass curve over a finite field +`F`. -/ noncomputable def traceOfFrobenius (E : WeierstrassCurve F) : ℤ := (Nat.card F : ℤ) + 1 - Nat.card E.toAffine.Point -/-- An elliptic curve over a finite field is **supersingular** if its characteristic `p` divides its -trace of Frobenius `aₚ`. The criterion is `p ∣ aₚ`, **not** `aₚ = 0`: for `p ≥ 5` these coincide -(Hasse gives `|aₚ| ≤ 2√q < p`), but in characteristic 2 and 3 `|aₚ|` can reach or exceed `p` -(e.g. `aₚ = ±2` at `p = 2`), where `aₚ = 0` would misclassify. `p ∣ aₚ` is correct in all -characteristics (Silverman, *Arithmetic of Elliptic Curves*, V.3.1). -/ +/-- A Weierstrass curve over a finite field is **supersingular** if its characteristic divides its +trace of Frobenius. In characteristic `2` and `3` this is not equivalent to the vanishing of the +trace (Silverman, *The Arithmetic of Elliptic Curves*, V.3.1). -/ def IsSupersingular (E : WeierstrassCurve F) : Prop := (ringChar F : ℤ) ∣ traceOfFrobenius E -/-- An elliptic curve over a finite field is **ordinary** if it is not supersingular, i.e. its -characteristic `p` does not divide its trace of Frobenius `aₚ` (the divisibility `p ∤ aₚ`, *not* -`aₚ ≠ 0` — see `IsSupersingular`). -/ +/-- A Weierstrass curve over a finite field is **ordinary** if it is not supersingular. -/ def IsOrdinary (E : WeierstrassCurve F) : Prop := ¬ E.IsSupersingular @@ -46,54 +42,44 @@ universe u v variable (R : Type v) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] variable {K : Type u} [Field K] [Algebra R K] [IsFractionRing R K] -/-- A minimal Weierstrass curve over `K` has **bad reduction** (LMFDB `ec.bad_reduction`) if its -reduction over the residue field of `R` is singular — equivalently, it does not have good -reduction. -/ +/-- A minimal Weierstrass curve over `K` has **bad reduction** (LMFDB `ec.bad_reduction`) if it +does not have good reduction, i.e. its reduction over the residue field of `R` is singular. -/ def IsBadReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop := ¬ HasGoodReduction R W -/-- A Weierstrass curve over `K` (with `R` a DVR, `K = Frac R`) has **potential good reduction** -(LMFDB `ec.potential_good_reduction`) if it acquires good reduction over a finite extension: there is -a discrete valuation ring `S` extending `R` (compatibly, via the scalar towers `R → S → Frac S` and -`R → K → Frac S`) whose fraction field `Frac S` is a *finite* extension of `K`, over which `W` has -good reduction. `S` lives in `K`'s universe (every finite extension of `K` does). Equivalently, by -Silverman AEC VII.5.5, `j(E) ∈ R`; this takes the base-change form requested in review. -/ +/-- An elliptic curve over `K` has **potential good reduction** (LMFDB +`ec.potential_good_reduction`) if it has good reduction over some finite extension of `K`, +formalized via the equivalent condition that its `j`-invariant is integral over `R` +(Silverman, *The Arithmetic of Elliptic Curves*, VII.5.5). -/ def IsPotentialGoodReduction (W : WeierstrassCurve K) [W.IsElliptic] : Prop := ∃ r : R, algebraMap R K r = W.j -/-- A minimal Weierstrass curve over `K` (with finite residue field) has **good ordinary reduction** -(LMFDB `ec.good_ordinary_reduction`) if it has good reduction and the reduced elliptic curve is -ordinary. (Ordinary uses `p ∤ aₚ`, the characteristic-independent criterion; see `IsOrdinary`.) -/ +/-- A Weierstrass curve over `K` with good reduction has **good ordinary reduction** (LMFDB +`ec.good_ordinary_reduction`) if its reduction over the finite residue field of `R` is +ordinary. -/ def IsGoodOrdinaryReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) -[HasGoodReduction R W]: Prop := - IsOrdinary (W.reduction R) + [HasGoodReduction R W] : Prop := + IsOrdinary (W.reduction R) -/-- A minimal Weierstrass curve over `K` (with finite residue field) has **good supersingular -reduction** (LMFDB `ec.good_supersingular_reduction`) if it has good reduction and the reduced -elliptic curve is supersingular. (Uses `p ∣ aₚ`, not `aₚ = 0` — correct in char 2 and 3; see -`IsSupersingular`.) -/ +/-- A Weierstrass curve over `K` with good reduction has **good supersingular reduction** (LMFDB +`ec.good_supersingular_reduction`) if its reduction over the finite residue field of `R` is +supersingular. -/ def IsGoodSupersingularReduction [Finite (ResidueField R)] (W : WeierstrassCurve K) [HasGoodReduction R W] : Prop := - IsSupersingular (W.reduction R) + IsSupersingular (W.reduction R) /-- A minimal Weierstrass curve over `K` has **non-split multiplicative reduction** (LMFDB -`ec.nonsplit_multiplicative_reduction`) if it has multiplicative reduction that is not split — the -complement of mathlib's `HasSplitMultiplicativeReduction` within `HasMultiplicativeReduction`. -/ +`ec.nonsplit_multiplicative_reduction`) if it has multiplicative reduction that is not split. -/ def IsNonsplitMultiplicativeReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop := HasMultiplicativeReduction R W ∧ ¬ HasSplitMultiplicativeReduction R W -/-- The **local minimal discriminant** of `E` at the prime of the DVR `R` (LMFDB -`ec.local_minimal_discriminant`): the ideal `𝔭^e` of `R` generated by the discriminant of a local -minimal model `W.minimal R`, where `e` is that discriminant's valuation at the prime. -/ +/-- The **local minimal discriminant** (LMFDB `ec.local_minimal_discriminant`) of a Weierstrass +curve over `K`: the ideal of `R` generated by the discriminant of a local minimal model. -/ noncomputable def localMinimalDiscriminant (W : WeierstrassCurve K) : Ideal R := Ideal.span {(integralModel R (W.minimal R)).Δ} /-- The **reduction type** (LMFDB `ec.reduction_type`) of an elliptic curve at a prime: **good**, -**multiplicative** (carrying a `split` boolean), or **additive** — the genuine trichotomy of -`HasGoodReduction` / `HasMultiplicativeReduction` / `HasAdditiveReduction`. (The split/non-split -distinction is attached to multiplicative reduction here; note that additive reduction can also be -split or non-split over a non-perfect residue field, which this type does not model.) Assigning the -type to a given `(curve, prime)` requires that trichotomy, which is not provided here. -/ +**multiplicative** (split or non-split), or **additive**. -/ inductive ReductionType | good | multiplicative (split : Bool) @@ -107,37 +93,29 @@ open IsDedekindDomain variable {O : Type*} [CommRing O] [IsDedekindDomain O] -/-- A Weierstrass model over `K = FractionRing O` (with `O` the ring of integers, a Dedekind domain) -is a **global minimal model** (LMFDB `ec.global_minimal_model`) if it is integral over `O` and is a -local minimal model at every nonzero prime of `O`. mathlib only has the *local* minimal-model theory -(`IsMinimal` over one DVR); this is the global assembly over all primes. The localization -`Localization.AtPrime v.asIdeal` of a Dedekind domain at a nonzero prime is a DVR with fraction field -`FractionRing O`, so `IsMinimal` applies at each `v`. -/ +/-- A Weierstrass curve over `FractionRing O` is a **global minimal model** (LMFDB +`ec.global_minimal_model`) if it is integral over `O` and minimal over the discrete valuation ring +`Localization.AtPrime v.asIdeal` at every height-one prime `v` of `O`. -/ def IsGlobalMinimalModel (W : WeierstrassCurve (FractionRing O)) : Prop := IsIntegral O W ∧ ∀ v : HeightOneSpectrum O, haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ IsMinimal (Localization.AtPrime v.asIdeal) W -/-- A Weierstrass model over `K = FractionRing O` is a **semi-global minimal model** (LMFDB -`ec.semi_global_minimal_model`) if it is integral over `O` and a local minimal model at every -nonzero prime of `O` except possibly one. Over a number field of class number greater than one an -elliptic curve may have no `IsGlobalMinimalModel`, but it always has a semi-global one; the -exceptional prime carries the obstruction class. (The knowl further records that at that prime the -discriminant valuation exceeds the minimal-discriminant valuation by `12`; that is a consequence -phrased via the minimal-discriminant ideal, so it is not part of this defining predicate.) -/ +/-- A Weierstrass curve over `FractionRing O` is a **semi-global minimal model** (LMFDB +`ec.semi_global_minimal_model`) if it is integral over `O` and minimal at every height-one prime +of `O` except possibly one. An elliptic curve over a number field of class number greater than one +need not admit a global minimal model, but it always admits a semi-global one. -/ def IsSemiGlobalMinimalModel (W : WeierstrassCurve (FractionRing O)) : Prop := IsIntegral O W ∧ ∃ v₀ : HeightOneSpectrum O, ∀ v : HeightOneSpectrum O, v ≠ v₀ → haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ IsMinimal (Localization.AtPrime v.asIdeal) W -/-- The **minimal discriminant ideal** (LMFDB `ec.minimal_discriminant`) of `E` over `O`: -`𝔡_min = ∏_v v ^ e_v`, the product over all nonzero primes `v` of `O` of `v ^ e_v`, where `e_v` is -the valuation of the discriminant of a local minimal model at `v` — the `v`-part of the local -minimal discriminant (cf. `localMinimalDiscriminant`). At a prime of good reduction `e_v = 0`, which -holds for all but finitely many `v`, so the (a priori infinite) product is finite. If `E` has a -`IsGlobalMinimalModel` then `𝔡_min = (Δ)`, the principal ideal of that model's discriminant. -/ +/-- The **minimal discriminant ideal** (LMFDB `ec.minimal_discriminant`) of a Weierstrass curve +over `FractionRing O`: the finite product `∏ᵥ 𝔭ᵥ ^ eᵥ` over the height-one primes `v` of `O`, +where `eᵥ` is the `v`-adic valuation of the discriminant of a local minimal model at `v`. If `W` +admits a global minimal model, this is the principal ideal generated by its discriminant. -/ noncomputable def minimalDiscriminantIdeal (W : WeierstrassCurve (FractionRing O)) : Ideal O := ∏ᶠ v : HeightOneSpectrum O, let R := Localization.AtPrime v.asIdeal @@ -145,20 +123,17 @@ noncomputable def minimalDiscriminantIdeal (W : WeierstrassCurve (FractionRing O IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ v.asIdeal ^ (-WithZero.log (v.valuation (FractionRing O) (W.minimal R).Δ)).toNat -/-- The unique **reduced minimal Weierstrass model** over `ℚ` (LMFDB -`ec.q.minimal_weierstrass_equation`): a global minimal model over `ℤ` whose coefficients are -normalized by `a₁, a₃ ∈ {0, 1}` and `a₂ ∈ {-1, 0, 1}`. These constraints single out the unique -representative among the global minimal models of `E / ℚ` (which differ by the integral variable -changes `[±1, r, s, t]`). The bare minimality is `IsGlobalMinimalModel` at `O := ℤ`; this adds the -canonical normal form. -/ +/-- A Weierstrass curve over `FractionRing ℤ` is a **reduced minimal model** (LMFDB +`ec.q.minimal_weierstrass_equation`) if it is a global minimal model with `a₁, a₃ ∈ {0, 1}` and +`a₂ ∈ {-1, 0, 1}`. These normalizations single out a unique global minimal model of an elliptic +curve over `ℚ`. -/ def IsReducedMinimalModel (W : WeierstrassCurve (FractionRing ℤ)) : Prop := IsGlobalMinimalModel W ∧ (W.a₁ = 0 ∨ W.a₁ = 1) ∧ (W.a₂ = -1 ∨ W.a₂ = 0 ∨ W.a₂ = 1) ∧ (W.a₃ = 0 ∨ W.a₃ = 1) -/-- An elliptic curve over `K = FractionRing O` is **semistable** (LMFDB `ec.semistable`) if it has -no additive reduction at any prime of `O` — equivalently, good or multiplicative reduction -everywhere, i.e. multiplicative reduction at every bad prime. The reduction at `v` is read off the -local minimal model `W.minimal (Localization.AtPrime v.asIdeal)`. -/ +/-- A Weierstrass curve over `FractionRing O` is **semistable** (LMFDB `ec.semistable`) if it does +not have additive reduction at any height-one prime of `O`, the reduction at `v` being that of a +local minimal model at `v`. -/ def IsSemistable (W : WeierstrassCurve (FractionRing O)) : Prop := ∀ v : HeightOneSpectrum O, haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := @@ -166,10 +141,9 @@ def IsSemistable (W : WeierstrassCurve (FractionRing O)) : Prop := ¬ HasAdditiveReduction (Localization.AtPrime v.asIdeal) (W.minimal (Localization.AtPrime v.asIdeal)) -/-- The **obstruction exponent** `fᵥ = (vᵥ(Δ) − eᵥ)/12` at a prime `v` for an integral model `W` -over `O`: the `v`-adic valuation of this model's discriminant minus the local minimal discriminant -valuation `eᵥ`, divided by `12` (an exact division, since two integral models' discriminant -valuations differ by a multiple of `12`). -/ +/-- The **obstruction exponent** `fᵥ = (v(Δ) - eᵥ) / 12` of an integral Weierstrass curve `W` over +`O` at a height-one prime `v`: the `v`-adic valuation of the discriminant of `W` minus that of a +local minimal model, divided by `12` (the difference is a nonnegative multiple of `12`). -/ noncomputable def obstructionExponent (W : WeierstrassCurve O) (v : HeightOneSpectrum O) : ℕ := let R := Localization.AtPrime v.asIdeal haveI : IsDiscreteValuationRing R := @@ -178,11 +152,10 @@ noncomputable def obstructionExponent (W : WeierstrassCurve O) (v : HeightOneSpe (-WithZero.log (v.valuation (FractionRing O) ((W.baseChange (FractionRing O)).minimal R).Δ)).toNat) / 12 -/-- The **obstruction class** (Silverman's *Weierstrass class*, LMFDB `ec.obstruction_class`) of an -integral model `W` over `O`: the ideal class `[∏ᵥ 𝔭ᵥ^{fᵥ}] ∈ ClassGroup O`, where `𝔞 = ∏ᵥ 𝔭ᵥ^{fᵥ}` -satisfies `𝔞¹² = (Δ)·𝔇_min⁻¹` (Silverman, *The Arithmetic of Elliptic Curves*, VIII.8). It is trivial -iff `E` has a global minimal model. The product is taken inside the non-zero-divisor submonoid, so -each `𝔭ᵥ^{fᵥ}` carries its own nonzero proof (`pow_mem` of the prime `𝔭ᵥ ≠ ⊥`). -/ +/-- The **obstruction class** (LMFDB `ec.obstruction_class`; Silverman's *Weierstrass class*) of +an integral Weierstrass curve `W` over `O`: the class of the ideal `∏ᵥ 𝔭ᵥ ^ fᵥ` in `ClassGroup O`, +where `fᵥ` is the obstruction exponent at `v`. It is trivial if and only if the curve admits a +global minimal model (Silverman, *The Arithmetic of Elliptic Curves*, VIII.8.2). -/ noncomputable def obstructionClass (W : WeierstrassCurve O) : ClassGroup O := ClassGroup.mk0 (∏ᶠ v : HeightOneSpectrum O, (⟨v.asIdeal ^ obstructionExponent W v, @@ -194,25 +167,23 @@ end GlobalMinimal section Height /-- The **naive height** (LMFDB `ec.q.naive_height`) of an elliptic curve over `ℚ` in short -Weierstrass form `y² = x³ + a₄x + a₆`: the quantity `max (4|a₄|³, 27|a₆|²)`. The `[W.IsShortNF]` -instance enforces the short-form requirement (`a₁ = a₂ = a₃ = 0`); a general curve must first be put -in short form (`W.toShortNF • W`) since the naive height depends on the chosen model. -/ +Weierstrass form `y² = x³ + a₄x + a₆`: the maximum of `4|a₄|³` and `27a₆²`. -/ def naiveHeight (W : WeierstrassCurve ℚ) [W.IsShortNF] : ℚ := max (4 * |W.a₄| ^ 3) (27 * W.a₆ ^ 2) -/-- The **naive height** of a rational point `P ∈ E(ℚ)`: `log max(|num x(P)|, |den x(P)|)`, the -height of its `x`-coordinate (and `0` at the point at infinity). -/ +/-- The **naive height** of a rational point on a Weierstrass curve over `ℚ`: the logarithm of the +maximum of the absolute value of the numerator and the denominator of its `x`-coordinate, and `0` +at the point at infinity. -/ noncomputable def naivePointHeight {W : WeierstrassCurve ℚ} : W.toAffine.Point → ℝ | .zero => 0 | .some (x := x) .. => Real.log (max (x.num.natAbs : ℝ) (x.den : ℝ)) open Filter in -/-- The **canonical (Néron–Tate) height** (LMFDB `ec.q.canonical_height`) of a rational point: -`ĥ(P) = limₙ (1/n²) · log max(|Aₙ|, |Dₙ|)` where `x(nP) = Aₙ/Dₙ` in lowest terms — i.e. the limit of -`naivePointHeight (n • P) / n²`. (This is LMFDB's normalization; some sources halve it.) The limit -uses `limUnder`, which returns a junk value if the sequence diverges; convergence (the Néron–Tate -theorem) holds but is *not* proved here, so this definition captures the defining formula and gives -the correct real value, but is inert in proofs until convergence is established. -/ +/-- The **canonical height**, or Néron–Tate height, (LMFDB `ec.q.canonical_height`) of a rational +point `P` on an elliptic curve over `ℚ`: the limit of `naivePointHeight (n • P) / n ^ 2`. This is +LMFDB's normalization, twice that of some authors. The limit is taken via `limUnder`, whose value +is unspecified when the sequence does not converge; convergence is the content of the Néron–Tate +theorem, which is not proved here. -/ noncomputable def canonicalHeight {W : WeierstrassCurve ℚ} [W.IsElliptic] (P : W.toAffine.Point) : ℝ := limUnder atTop (fun n : ℕ => naivePointHeight (n • P) / (n : ℝ) ^ 2) @@ -221,11 +192,10 @@ end Height section Frey -/-- The **Frey–Hellegouarch curve** (LMFDB `ec.q.frey`) of a pair `A, B` (from a triple with -`A + B = C`): the curve `y² = x(x - A)(x + B)`. Expanding `x(x - A)(x + B) = x³ + (B - A)x² - A*B*x` -gives the Weierstrass coefficients `a₂ = B - A`, `a₄ = -A*B`, with `a₁ = a₃ = a₆ = 0`. Its -discriminant is `Δ = 16*A²*B²*(A + B)²`, so it is an elliptic curve exactly when `A`, `B`, `A + B` -are all nonzero. -/ +/-- The **Frey–Hellegouarch curve** (LMFDB `ec.q.frey`) `y² = x * (x - A) * (x + B)` of a pair +`A B : R`: the Weierstrass curve with `a₂ = B - A`, `a₄ = -A * B` and `a₁ = a₃ = a₆ = 0`. Its +discriminant is `16A²B²(A + B)²`, so it is an elliptic curve exactly when `A`, `B` and `A + B` are +all nonzero. -/ def freyCurve {R : Type*} [CommRing R] (A B : R) : WeierstrassCurve R where a₁ := 0 a₂ := B - A @@ -237,11 +207,11 @@ end Frey section Quality -/-- The **abc quality** (LMFDB `ec.q.abc_quality`) of an elliptic curve over `ℚ`: -`log max(|a|, |b|, |c|) / log rad(abc)`, where `j/1728 = a/c` is in lowest terms and `b = c - a` -(`rad` is the radical, the product of the primes dividing its argument). The quality is undefined at -`j = 0` and `j = 1728`: there `a*b*c = 0`, so `rad = 1`, `log 1 = 0`, and the value is the junk `0` -(Lean's `x / 0 = 0`). Needs `[E.IsElliptic]` for the `j`-invariant. -/ +/-- The **abc quality** (LMFDB `ec.q.abc_quality`) of an elliptic curve over `ℚ`: the quotient +`log max(|a|, |b|, |c|) / log rad(abc)`, where `j / 1728 = a / c` in lowest terms, `b = c - a` and +`rad` is the radical of an integer. The quality is mathematically undefined when `j = 0` or +`j = 1728`: there `abc = 0`, so the denominator `log (rad 0) = log 1` vanishes and the expression +evaluates to `0`, an artifact of division by zero in Lean rather than a meaningful value. -/ noncomputable def abcQuality (E : WeierstrassCurve ℚ) [E.IsElliptic] : ℝ := let a := (E.j / 1728).num let c := ((E.j / 1728).den : ℤ) @@ -253,13 +223,12 @@ end Quality section Points -/-- The **integral points** (LMFDB `ec.q.integral_points`) of a given model `W` of an elliptic curve -over `ℚ`: the affine points `(x, y)` of `W` with integral coordinates `x, y ∈ ℤ`. (The point at -infinity is excluded, having no affine coordinates.) The knowl's "integral points on a minimal model" -is then `integralPoints` of the global minimal model; the set is finite by Siegel's theorem, which is -not part of this definition. -/ +/-- The **integral points** (LMFDB `ec.q.integral_points`) of a Weierstrass curve over `ℚ`: the +affine points whose coordinates are integers. This depends on the choice of model; the LMFDB +lists integral points on a reduced minimal model. -/ def integralPoints (W : WeierstrassCurve ℚ) : Set W.toAffine.Point := - {P | ∃ (x y : ℤ) (h : W.toAffine.Nonsingular (x : ℚ) (y : ℚ)), P = Affine.Point.some (x : ℚ) (y : ℚ) h} + {P | ∃ (x y : ℤ) (h : W.toAffine.Nonsingular (x : ℚ) (y : ℚ)), + P = Affine.Point.some (x : ℚ) (y : ℚ) h} end Points From f1cef93785eac6445da14b37f3b19832dc99d579 Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Tue, 28 Jul 2026 19:26:00 -0400 Subject: [PATCH 10/12] height uses mathlib height now --- LeanBridge/ForMathlib/4-EC.lean | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index 927a04ea..2e735ae5 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -1,7 +1,7 @@ import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point import Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms import Mathlib.AlgebraicGeometry.EllipticCurve.Reduction -import Mathlib.Analysis.SpecialFunctions.Log.Basic +import Mathlib.NumberTheory.Height.NumberField import Mathlib.RingTheory.Radical.NatInt /-! @@ -167,26 +167,25 @@ end GlobalMinimal section Height /-- The **naive height** (LMFDB `ec.q.naive_height`) of an elliptic curve over `ℚ` in short -Weierstrass form `y² = x³ + a₄x + a₆`: the maximum of `4|a₄|³` and `27a₆²`. -/ +Weierstrass form `y² = x³ + a₄x + a₆`: the maximum of `4|a₄|³` and `27a₆²`. The LMFDB defines this +as a plain maximum; it is not a logarithmic height in the sense of `Height.logHeight₁`. -/ def naiveHeight (W : WeierstrassCurve ℚ) [W.IsShortNF] : ℚ := max (4 * |W.a₄| ^ 3) (27 * W.a₆ ^ 2) -/-- The **naive height** of a rational point on a Weierstrass curve over `ℚ`: the logarithm of the -maximum of the absolute value of the numerator and the denominator of its `x`-coordinate, and `0` -at the point at infinity. -/ -noncomputable def naivePointHeight {W : WeierstrassCurve ℚ} : W.toAffine.Point → ℝ - | .zero => 0 - | .some (x := x) .. => Real.log (max (x.num.natAbs : ℝ) (x.den : ℝ)) - -open Filter in +open Filter Height in /-- The **canonical height**, or Néron–Tate height, (LMFDB `ec.q.canonical_height`) of a rational -point `P` on an elliptic curve over `ℚ`: the limit of `naivePointHeight (n • P) / n ^ 2`. This is -LMFDB's normalization, twice that of some authors. The limit is taken via `limUnder`, whose value -is unspecified when the sequence does not converge; convergence is the content of the Néron–Tate -theorem, which is not proved here. -/ +point `P` on an elliptic curve over `ℚ`: the limit of `logHeight₁ (x (n • P)) / n ^ 2`, where +`logHeight₁` is the logarithmic height of the `x`-coordinate and the point at infinity contributes +`0`. This is LMFDB's normalization, twice that of some authors. Mathlib does not (yet) define the +canonical height. The limit is taken via `limUnder`, whose value is unspecified when the sequence +does not converge; convergence is the content of the Néron–Tate theorem, which is not proved +here. -/ noncomputable def canonicalHeight {W : WeierstrassCurve ℚ} [W.IsElliptic] (P : W.toAffine.Point) : ℝ := - limUnder atTop (fun n : ℕ => naivePointHeight (n • P) / (n : ℝ) ^ 2) + limUnder atTop fun n : ℕ => + (match n • P with + | .zero => 0 + | .some (x := x) .. => logHeight₁ x) / (n : ℝ) ^ 2 end Height From 2114839469593ef453156c12147f0b240bbb4412 Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Wed, 29 Jul 2026 16:57:33 -0400 Subject: [PATCH 11/12] Three changes 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 --- LeanBridge/ForMathlib/4-EC.lean | 80 ++++++++++++++++++--------------- 1 file changed, 43 insertions(+), 37 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index 2e735ae5..ab285af0 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -93,42 +93,51 @@ open IsDedekindDomain variable {O : Type*} [CommRing O] [IsDedekindDomain O] -/-- A Weierstrass curve over `FractionRing O` is a **global minimal model** (LMFDB -`ec.global_minimal_model`) if it is integral over `O` and minimal over the discrete valuation ring -`Localization.AtPrime v.asIdeal` at every height-one prime `v` of `O`. -/ -def IsGlobalMinimalModel (W : WeierstrassCurve (FractionRing O)) : Prop := - IsIntegral O W ∧ ∀ v : HeightOneSpectrum O, - haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := - IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ - IsMinimal (Localization.AtPrime v.asIdeal) W - -/-- A Weierstrass curve over `FractionRing O` is a **semi-global minimal model** (LMFDB -`ec.semi_global_minimal_model`) if it is integral over `O` and minimal at every height-one prime -of `O` except possibly one. An elliptic curve over a number field of class number greater than one -need not admit a global minimal model, but it always admits a semi-global one. -/ -def IsSemiGlobalMinimalModel (W : WeierstrassCurve (FractionRing O)) : Prop := - IsIntegral O W ∧ ∃ v₀ : HeightOneSpectrum O, ∀ v : HeightOneSpectrum O, v ≠ v₀ → - haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := - IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ - IsMinimal (Localization.AtPrime v.asIdeal) W +/- The localization of a Dedekind domain at a height-one prime is a discrete valuation ring, +provided locally so that the definitions below need not thread it by hand. -/ +local instance (v : HeightOneSpectrum O) : + IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := + IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ + +/-- A Weierstrass curve over `FractionRing O` is **globally minimal** (LMFDB +`ec.global_minimal_model`) if it is minimal over the discrete valuation ring +`Localization.AtPrime v.asIdeal` at every height-one prime `v` of `O`. Integrality over `O` is +not assumed; it follows (see the note below). -/ +def IsGlobalMinimal (W : WeierstrassCurve (FractionRing O)) : Prop := + ∀ v : HeightOneSpectrum O, IsMinimal (Localization.AtPrime v.asIdeal) W + +/-- A Weierstrass curve over `FractionRing O` is **semi-globally minimal** (LMFDB +`ec.semi_global_minimal_model`) if, for some height-one prime `v₀` of `O`, it is integral over the +localization at `v₀` and minimal at every other height-one prime. (Integrality at `v₀` cannot be +dropped: minimality away from `v₀` says nothing about the denominators at `v₀`.) An elliptic curve +over a number field of class number greater than one need not admit a globally minimal model, but +it always admits a semi-globally minimal one. -/ +def IsSemiGlobalMinimal (W : WeierstrassCurve (FractionRing O)) : Prop := + ∃ v₀ : HeightOneSpectrum O, IsIntegral (Localization.AtPrime v₀.asIdeal) W ∧ + ∀ v : HeightOneSpectrum O, v ≠ v₀ → IsMinimal (Localization.AtPrime v.asIdeal) W + +/- Note: `IsIntegral O W` follows from either definition above, but not by `inferInstance`: +mathlib's `[IsMinimal R W] : IsIntegral R W` instance gives integrality over each localization +only; descending to `O` is a coefficient-by-coefficient argument via `O = ⋂ᵥ Oᵥ` +(`mem_integers_of_valuation_le_one`). The derivation was formalized and axiom-checked in this +repository's history, then removed to keep this file definitions-only. -/ + /-- The **minimal discriminant ideal** (LMFDB `ec.minimal_discriminant`) of a Weierstrass curve over `FractionRing O`: the finite product `∏ᵥ 𝔭ᵥ ^ eᵥ` over the height-one primes `v` of `O`, where `eᵥ` is the `v`-adic valuation of the discriminant of a local minimal model at `v`. If `W` -admits a global minimal model, this is the principal ideal generated by its discriminant. -/ +admits a globally minimal model, this is the principal ideal generated by its discriminant. -/ noncomputable def minimalDiscriminantIdeal (W : WeierstrassCurve (FractionRing O)) : Ideal O := ∏ᶠ v : HeightOneSpectrum O, let R := Localization.AtPrime v.asIdeal - haveI : IsDiscreteValuationRing R := - IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ v.asIdeal ^ (-WithZero.log (v.valuation (FractionRing O) (W.minimal R).Δ)).toNat -/-- A Weierstrass curve over `FractionRing ℤ` is a **reduced minimal model** (LMFDB -`ec.q.minimal_weierstrass_equation`) if it is a global minimal model with `a₁, a₃ ∈ {0, 1}` and -`a₂ ∈ {-1, 0, 1}`. These normalizations single out a unique global minimal model of an elliptic +/-- A Weierstrass curve over `FractionRing ℤ` is **reduced minimal** (LMFDB +`ec.q.minimal_weierstrass_equation`) if it is globally minimal with `a₁, a₃ ∈ {0, 1}` and +`a₂ ∈ {-1, 0, 1}`. These normalizations single out a unique globally minimal model of an elliptic curve over `ℚ`. -/ -def IsReducedMinimalModel (W : WeierstrassCurve (FractionRing ℤ)) : Prop := - IsGlobalMinimalModel W ∧ +def IsReducedMinimal (W : WeierstrassCurve (FractionRing ℤ)) : Prop := + IsGlobalMinimal W ∧ (W.a₁ = 0 ∨ W.a₁ = 1) ∧ (W.a₂ = -1 ∨ W.a₂ = 0 ∨ W.a₂ = 1) ∧ (W.a₃ = 0 ∨ W.a₃ = 1) /-- A Weierstrass curve over `FractionRing O` is **semistable** (LMFDB `ec.semistable`) if it does @@ -136,8 +145,6 @@ not have additive reduction at any height-one prime of `O`, the reduction at `v` local minimal model at `v`. -/ def IsSemistable (W : WeierstrassCurve (FractionRing O)) : Prop := ∀ v : HeightOneSpectrum O, - haveI : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := - IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ ¬ HasAdditiveReduction (Localization.AtPrime v.asIdeal) (W.minimal (Localization.AtPrime v.asIdeal)) @@ -145,17 +152,14 @@ def IsSemistable (W : WeierstrassCurve (FractionRing O)) : Prop := `O` at a height-one prime `v`: the `v`-adic valuation of the discriminant of `W` minus that of a local minimal model, divided by `12` (the difference is a nonnegative multiple of `12`). -/ noncomputable def obstructionExponent (W : WeierstrassCurve O) (v : HeightOneSpectrum O) : ℕ := - let R := Localization.AtPrime v.asIdeal - haveI : IsDiscreteValuationRing R := - IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ ((-WithZero.log (v.valuation (FractionRing O) (algebraMap O (FractionRing O) W.Δ))).toNat - (-WithZero.log (v.valuation (FractionRing O) - ((W.baseChange (FractionRing O)).minimal R).Δ)).toNat) / 12 + ((W.baseChange (FractionRing O)).minimal (Localization.AtPrime v.asIdeal)).Δ)).toNat) / 12 /-- The **obstruction class** (LMFDB `ec.obstruction_class`; Silverman's *Weierstrass class*) of an integral Weierstrass curve `W` over `O`: the class of the ideal `∏ᵥ 𝔭ᵥ ^ fᵥ` in `ClassGroup O`, where `fᵥ` is the obstruction exponent at `v`. It is trivial if and only if the curve admits a -global minimal model (Silverman, *The Arithmetic of Elliptic Curves*, VIII.8.2). -/ +globally minimal model (Silverman, *The Arithmetic of Elliptic Curves*, VIII.8.2). -/ noncomputable def obstructionClass (W : WeierstrassCurve O) : ClassGroup O := ClassGroup.mk0 (∏ᶠ v : HeightOneSpectrum O, (⟨v.asIdeal ^ obstructionExponent W v, @@ -193,8 +197,9 @@ section Frey /-- The **Frey–Hellegouarch curve** (LMFDB `ec.q.frey`) `y² = x * (x - A) * (x + B)` of a pair `A B : R`: the Weierstrass curve with `a₂ = B - A`, `a₄ = -A * B` and `a₁ = a₃ = a₆ = 0`. Its -discriminant is `16A²B²(A + B)²`, so it is an elliptic curve exactly when `A`, `B` and `A + B` are -all nonzero. -/ +discriminant is `16A²B²(A + B)²`, so over a field of characteristic not `2` it is an elliptic +curve exactly when `A`, `B` and `A + B` are all nonzero (in general, when that discriminant is a +unit). -/ def freyCurve {R : Type*} [CommRing R] (A B : R) : WeierstrassCurve R where a₁ := 0 a₂ := B - A @@ -223,8 +228,9 @@ end Quality section Points /-- The **integral points** (LMFDB `ec.q.integral_points`) of a Weierstrass curve over `ℚ`: the -affine points whose coordinates are integers. This depends on the choice of model; the LMFDB -lists integral points on a reduced minimal model. -/ +affine points whose coordinates are integers. The knowl defines these for a given model, so the +set depends on the chosen model; it is finite by Siegel's theorem, which is not part of this +definition. -/ def integralPoints (W : WeierstrassCurve ℚ) : Set W.toAffine.Point := {P | ∃ (x y : ℤ) (h : W.toAffine.Nonsingular (x : ℚ) (y : ℚ)), P = Affine.Point.some (x : ℚ) (y : ℚ) h} From d84dd305b5f36a27dde49d07110cc1e7266e0fff Mon Sep 17 00:00:00 2001 From: Shi Shi Date: Wed, 29 Jul 2026 17:23:37 -0400 Subject: [PATCH 12/12] AKLB setup is done --- LeanBridge/ForMathlib/4-EC.lean | 58 +++++++++++++++++++++------------ 1 file changed, 37 insertions(+), 21 deletions(-) diff --git a/LeanBridge/ForMathlib/4-EC.lean b/LeanBridge/ForMathlib/4-EC.lean index ab285af0..c1e02e31 100644 --- a/LeanBridge/ForMathlib/4-EC.lean +++ b/LeanBridge/ForMathlib/4-EC.lean @@ -91,28 +91,41 @@ section GlobalMinimal open IsDedekindDomain -variable {O : Type*} [CommRing O] [IsDedekindDomain O] +variable (O : Type*) [CommRing O] [IsDedekindDomain O] +variable {K : Type*} [Field K] [Algebra O K] [IsFractionRing O K] -/- The localization of a Dedekind domain at a height-one prime is a discrete valuation ring, -provided locally so that the definitions below need not thread it by hand. -/ +/- Local instances (AKLB setting): the localization of `O` at a height-one prime is a discrete +valuation ring sitting inside the abstract fraction field `K`; mathlib has the latter three +instances only for `K = FractionRing O`. -/ local instance (v : HeightOneSpectrum O) : IsDiscreteValuationRing (Localization.AtPrime v.asIdeal) := IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain O v.ne_bot _ -/-- A Weierstrass curve over `FractionRing O` is **globally minimal** (LMFDB -`ec.global_minimal_model`) if it is minimal over the discrete valuation ring +noncomputable local instance (v : HeightOneSpectrum O) : + Algebra (Localization.AtPrime v.asIdeal) K := + IsLocalization.localizationAlgebraOfSubmonoidLe _ _ _ _ v.asIdeal.primeCompl_le_nonZeroDivisors + +local instance (v : HeightOneSpectrum O) : IsScalarTower O (Localization.AtPrime v.asIdeal) K := + IsLocalization.localization_isScalarTower_of_submonoid_le _ _ _ _ + v.asIdeal.primeCompl_le_nonZeroDivisors + +local instance (v : HeightOneSpectrum O) : IsFractionRing (Localization.AtPrime v.asIdeal) K := + IsFractionRing.isFractionRing_of_isDomain_of_isLocalization v.asIdeal.primeCompl _ K + +/-- A Weierstrass curve over a fraction field `K` of the Dedekind domain `O` is **globally +minimal** (LMFDB `ec.global_minimal_model`) if it is minimal over the discrete valuation ring `Localization.AtPrime v.asIdeal` at every height-one prime `v` of `O`. Integrality over `O` is not assumed; it follows (see the note below). -/ -def IsGlobalMinimal (W : WeierstrassCurve (FractionRing O)) : Prop := +def IsGlobalMinimal (W : WeierstrassCurve K) : Prop := ∀ v : HeightOneSpectrum O, IsMinimal (Localization.AtPrime v.asIdeal) W -/-- A Weierstrass curve over `FractionRing O` is **semi-globally minimal** (LMFDB +/-- A Weierstrass curve over a fraction field `K` of `O` is **semi-globally minimal** (LMFDB `ec.semi_global_minimal_model`) if, for some height-one prime `v₀` of `O`, it is integral over the localization at `v₀` and minimal at every other height-one prime. (Integrality at `v₀` cannot be dropped: minimality away from `v₀` says nothing about the denominators at `v₀`.) An elliptic curve over a number field of class number greater than one need not admit a globally minimal model, but it always admits a semi-globally minimal one. -/ -def IsSemiGlobalMinimal (W : WeierstrassCurve (FractionRing O)) : Prop := +def IsSemiGlobalMinimal (W : WeierstrassCurve K) : Prop := ∃ v₀ : HeightOneSpectrum O, IsIntegral (Localization.AtPrime v₀.asIdeal) W ∧ ∀ v : HeightOneSpectrum O, v ≠ v₀ → IsMinimal (Localization.AtPrime v.asIdeal) W @@ -124,30 +137,33 @@ repository's history, then removed to keep this file definitions-only. -/ /-- The **minimal discriminant ideal** (LMFDB `ec.minimal_discriminant`) of a Weierstrass curve -over `FractionRing O`: the finite product `∏ᵥ 𝔭ᵥ ^ eᵥ` over the height-one primes `v` of `O`, -where `eᵥ` is the `v`-adic valuation of the discriminant of a local minimal model at `v`. If `W` -admits a globally minimal model, this is the principal ideal generated by its discriminant. -/ -noncomputable def minimalDiscriminantIdeal (W : WeierstrassCurve (FractionRing O)) : Ideal O := +over a fraction field `K` of `O`: the finite product `∏ᵥ 𝔭ᵥ ^ eᵥ` over the height-one primes `v` +of `O`, where `eᵥ` is the `v`-adic valuation of the discriminant of a local minimal model at `v`. +If `W` admits a globally minimal model, this is the principal ideal generated by its +discriminant. -/ +noncomputable def minimalDiscriminantIdeal (W : WeierstrassCurve K) : Ideal O := ∏ᶠ v : HeightOneSpectrum O, let R := Localization.AtPrime v.asIdeal - v.asIdeal ^ (-WithZero.log (v.valuation (FractionRing O) (W.minimal R).Δ)).toNat + v.asIdeal ^ (-WithZero.log (v.valuation K (W.minimal R).Δ)).toNat -/-- A Weierstrass curve over `FractionRing ℤ` is **reduced minimal** (LMFDB -`ec.q.minimal_weierstrass_equation`) if it is globally minimal with `a₁, a₃ ∈ {0, 1}` and +/-- A Weierstrass curve over `ℚ` is **reduced minimal** (LMFDB +`ec.q.minimal_weierstrass_equation`) if it is globally minimal over `ℤ` with `a₁, a₃ ∈ {0, 1}` and `a₂ ∈ {-1, 0, 1}`. These normalizations single out a unique globally minimal model of an elliptic curve over `ℚ`. -/ -def IsReducedMinimal (W : WeierstrassCurve (FractionRing ℤ)) : Prop := - IsGlobalMinimal W ∧ +def IsReducedMinimal (W : WeierstrassCurve ℚ) : Prop := + IsGlobalMinimal ℤ W ∧ (W.a₁ = 0 ∨ W.a₁ = 1) ∧ (W.a₂ = -1 ∨ W.a₂ = 0 ∨ W.a₂ = 1) ∧ (W.a₃ = 0 ∨ W.a₃ = 1) -/-- A Weierstrass curve over `FractionRing O` is **semistable** (LMFDB `ec.semistable`) if it does -not have additive reduction at any height-one prime of `O`, the reduction at `v` being that of a -local minimal model at `v`. -/ -def IsSemistable (W : WeierstrassCurve (FractionRing O)) : Prop := +/-- A Weierstrass curve over a fraction field of `O` is **semistable** (LMFDB `ec.semistable`) if +it does not have additive reduction at any height-one prime of `O`, the reduction at `v` being +that of a local minimal model at `v`. -/ +def IsSemistable (W : WeierstrassCurve K) : Prop := ∀ v : HeightOneSpectrum O, ¬ HasAdditiveReduction (Localization.AtPrime v.asIdeal) (W.minimal (Localization.AtPrime v.asIdeal)) +variable {O} + /-- The **obstruction exponent** `fᵥ = (v(Δ) - eᵥ) / 12` of an integral Weierstrass curve `W` over `O` at a height-one prime `v`: the `v`-adic valuation of the discriminant of `W` minus that of a local minimal model, divided by `12` (the difference is a nonnegative multiple of `12`). -/