Elliptic curve definitions bridging LMFDB knowls to Lean

LeanBridge.lean

@@ -1 +1,2 @@
 import LeanBridge.Example
+import LeanBridge.ForMathlib.«4-EC»

LeanBridge/ForMathlib/4-EC.lean

@@ -0,0 +1,256 @@
+import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
+import Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
+import Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
+import Mathlib.NumberTheory.Height.NumberField
+import Mathlib.RingTheory.Radical.NatInt
+
+/-!
+# 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 a Weierstrass curve over a finite field
+`F`. -/
+noncomputable def traceOfFrobenius (E : WeierstrassCurve F) : ℤ :=
+  (Nat.card F : ℤ) + 1 - Nat.card E.toAffine.Point
+
+/-- 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
+
+/-- A Weierstrass curve over a finite field is **ordinary** if it is not supersingular. -/
+def IsOrdinary (E : WeierstrassCurve F) : Prop :=
+  ¬ E.IsSupersingular
+
+end FiniteField
+
+section Reduction
+
+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 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
+
+/-- 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 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)
+
+/-- 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)
+
+/-- 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. -/
+def IsNonsplitMultiplicativeReduction (W : WeierstrassCurve K) [IsMinimal R W] : Prop :=
+  HasMultiplicativeReduction R W ∧ ¬ HasSplitMultiplicativeReduction R W
+
+/-- 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** (split or non-split), or **additive**. -/
+inductive ReductionType
+  | good
+  | multiplicative (split : Bool)
+  | additive
+
+end Reduction
+
+section GlobalMinimal
+
+open IsDedekindDomain
+
+variable (O : Type*) [CommRing O] [IsDedekindDomain O]
+variable {K : Type*} [Field K] [Algebra O K] [IsFractionRing O K]
+
+/- 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 _
+
+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 K) : Prop :=
+  ∀ v : HeightOneSpectrum O, IsMinimal (Localization.AtPrime v.asIdeal) W
+
+/-- 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 K) : 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 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 K (W.minimal R).Δ)).toNat
+
+/-- 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 ℚ) : 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 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`). -/
+noncomputable def obstructionExponent (W : WeierstrassCurve O) (v : HeightOneSpectrum O) : ℕ :=
+  ((-WithZero.log (v.valuation (FractionRing O) (algebraMap O (FractionRing O) W.Δ))).toNat -
+    (-WithZero.log (v.valuation (FractionRing O)
+      ((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
+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,
+      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 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)
+
+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 `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 : ℕ =>
+    (match n • P with
+      | .zero => 0
+      | .some (x := x) .. => logHeight₁ x) / (n : ℝ) ^ 2
+
+end Height
+
+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 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
+  a₃ := 0
+  a₄ := -(A * B)
+  a₆ := 0
+
+end Frey
+
+section Quality
+
+/-- 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 : ℤ)
+  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 Weierstrass curve over `ℚ`: the
+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}
+
+end Points
+
+end WeierstrassCurve