The minimal-pair short equation of an elliptic curve over ℚ, and its naïve height

An elliptic curve E over ℚ has infinitely many short Weierstrass equations y² = x³ + Ax + B: the scaling x = u²x', y = u³y' replaces (A, B) by (u⁻⁴A, u⁻⁶B) for every u ∈ ℚˣ. Among the equations with A, B ∈ ℤ exactly one is a minimal pair, meaning that no prime ℓ has both ℓ⁴ ∣ A and ℓ⁶ ∣ B; the residual freedom u = ±1 acts trivially on it. This file constructs that equation, proves it unique, and defines the naïve height of E as max (4|A|³) (27B²) computed from it. The height is the quantity by which tables of elliptic curves over ℚ are ordered, and the bounded-height finiteness theorem is what makes such a table finite.

Main definitions

• WeierstrassCurve.shortEquationHeight W: max (4|a₄|³) (27a₆²) for a short equation W over ℤ. A property of the equation, not of the curve.
• WeierstrassCurve.IsMinimalPairNF W: W is short and (a₄, a₆) is a minimal pair.
• WeierstrassCurve.MinimalPairModel E: a minimal-pair equation over ℤ whose base change is isomorphic to E, with a chosen change of variables WeierstrassCurve.MinimalPairModel.variableChange realising the isomorphism, and WeierstrassCurve.MinimalPairModel.height, the height of its equation.
• WeierstrassCurve.minimalPairModel E: a chosen such model, and WeierstrassCurve.naiveHeight E, its height: the curve-level invariant.

Main results

• WeierstrassCurve.exists_minimalPairModel: every elliptic curve over ℚ has a minimal-pair model.
• WeierstrassCurve.minimalPairModel_unique: any two minimal-pair models of E have the same equation, so MinimalPairModel E is a subsingleton. Hence WeierstrassCurve.naiveHeight_eq (every model computes the curve's height) and WeierstrassCurve.naiveHeight_variableChange (invariance under ℚ-isomorphism).
• WeierstrassCurve.finite_shortEquations_bounded_height and WeierstrassCurve.finite_minimalPairEquations_bounded_height: finitely many short equations over ℤ, in particular finitely many minimal-pair equations, have height at most H.
• WeierstrassCurve.shortEquationHeight_le_of_natAbs_le and WeierstrassCurve.natAbs_Δ_le_mul_shortEquationHeight: the height is monotone in |a₄| and |a₆|, and bounds the discriminant, |Δ| ≤ 32 · H.

Design

• The carrier is the content. On short equations over ℚ the expression max (4|A|³) (27B²) is not an invariant: scaling by u divides it by |u|¹², so one curve has rational short equations of arbitrarily small height and bounded-height finiteness fails. Pinning the equation to the minimal pair over ℤ is what makes the height well defined, which is why shortEquationHeight takes an equation over ℤ and only naiveHeight is curve-level.
• A minimal pair is not a minimal Weierstrass equation. At 2 and 3 the minimal-pair short equation need not be minimal in the sense of WeierstrassCurve.IsMinimal, and the globally minimal equation of a curve over ℚ is in general a long one. The two canonical equations serve different purposes, and neither replaces the other.
• The equation is the only data. A MinimalPairModel records the equation and the existence of an isomorphism to E, not a particular change of variables: that is unique only up to the automorphisms of E, and composing it with [-1] gives another. minimalPairModel_unique makes the type a subsingleton, and MinimalPairModel.variableChange recovers a witness when a computation needs one.
• The naïve height on points, WeierstrassCurve.Affine.Point.naiveHeight, is a different quantity on a different type.

References

• J. S. Balakrishnan, W. Ho, N. Kaplan, S. Spicer, W. Stein, J. Weigandt, Databases of elliptic curves ordered by height and distributions of Selmer groups and ranks, LMS J. Comput. Math. 19 (2016), 351–370: the minimal-pair convention and the height computed from it.
• LMFDB knowl ec.q.naive_height.

Provenance

naiveHeight is adapted from LeanBridge (github.com/CBirkbeck/LeanBridge, Apache-2.0), file LeanBridge/ForMathlib/4-EC.lean at JaneShi99/LeanBridge@d84dd305 (branch formalize/ec-defs), by Jane Shi, where it is the ℚ-valued expression max (4|a₄|³) (27a₆²) on any short equation over ℚ. Here it is ℕ-valued and pinned to the minimal-pair equation over ℤ; the minimal-pair normal form, the bundled model, and the existence, uniqueness and finiteness theorems are new.

The height of an integral short equation

def WeierstrassCurve.shortEquationHeight (W : WeierstrassCurve ℤ) : ℕ

The height of a short Weierstrass equation y² = x³ + a₄x + a₆ over ℤ: max (4|a₄|³) (27a₆²). The formula is stated for every Weierstrass equation over ℤ, but it is the height of the equation only when the equation is short, which is how it is used. It is a function of the equation, not of the curve it defines: over ℚ, the scaling x = u²x', y = u³y' sends (a₄, a₆) to (u⁻⁴a₄, u⁻⁶a₆) and divides the same expression by |u|¹². It becomes an invariant of the curve once the equation is pinned to the minimal pair, which is naiveHeight.

Equations

• W.shortEquationHeight = max (4 * W.a₄.natAbs ^ 3) (27 * W.a₆.natAbs ^ 2)

@[simp]

theorem WeierstrassCurve.shortEquationHeight_def (W : WeierstrassCurve ℤ) : W.shortEquationHeight = max (4 * W.a₄.natAbs ^ 3) (27 * W.a₆.natAbs ^ 2)

shortEquationHeight, unfolded. This is the interface to WeierstrassCurve.shortEquationHeight outside its defining module.

theorem WeierstrassCurve.natAbs_a₄_le_shortEquationHeight (W : WeierstrassCurve ℤ) : W.a₄.natAbs ≤ W.shortEquationHeight

The height of a short equation bounds |a₄|.

theorem WeierstrassCurve.natAbs_a₆_le_shortEquationHeight (W : WeierstrassCurve ℤ) : W.a₆.natAbs ≤ W.shortEquationHeight

The height of a short equation bounds |a₆|.

theorem WeierstrassCurve.shortEquationHeight_le_of_natAbs_le (W : WeierstrassCurve ℤ) {W' : WeierstrassCurve ℤ} (h₄ : W.a₄.natAbs ≤ W'.a₄.natAbs) (h₆ : W.a₆.natAbs ≤ W'.a₆.natAbs) : W.shortEquationHeight ≤ W'.shortEquationHeight

The height of a short equation is monotone in |a₄| and |a₆|.

theorem WeierstrassCurve.natAbs_Δ_le_mul_shortEquationHeight (W : WeierstrassCurve ℤ) [W.IsShortNF] : W.Δ.natAbs ≤ 32 * W.shortEquationHeight

The height of a short equation bounds its discriminant: Δ = -16(4a₄³ + 27a₆²) has |Δ| ≤ 32 · max (4|a₄|³) (27a₆²).

The minimal-pair normal form

def WeierstrassCurve.IsMinimalPairNF (W : WeierstrassCurve ℤ) : Prop

The minimal-pair normal form of an integral short equation: W is short, and no prime ℓ has both ℓ⁴ ∣ a₄ and ℓ⁶ ∣ a₆. This is the condition that kills the scaling freedom (a₄, a₆) ↦ (u⁴a₄, u⁶a₆) of short equations over ℤ, so that the equation, and with it shortEquationHeight, is determined by the curve (minimalPairModel_unique). It is a condition on the pair (a₄, a₆), not minimality of the Weierstrass equation in the sense of WeierstrassCurve.IsMinimal: at 2 and 3 the two notions differ.

Equations

• W.IsMinimalPairNF = (W.IsShortNF ∧ ∀ (ℓ : ℕ), Nat.Prime ℓ → ¬(↑ℓ ^ 4 ∣ W.a₄ ∧ ↑ℓ ^ 6 ∣ W.a₆))

@[simp]

theorem WeierstrassCurve.isMinimalPairNF_iff {W : WeierstrassCurve ℤ} : W.IsMinimalPairNF ↔ W.IsShortNF ∧ ∀ (ℓ : ℕ), Nat.Prime ℓ → ¬(↑ℓ ^ 4 ∣ W.a₄ ∧ ↑ℓ ^ 6 ∣ W.a₆)

The minimal-pair normal form, unfolded. This is the interface to WeierstrassCurve.IsMinimalPairNF outside its defining module.

theorem WeierstrassCurve.IsMinimalPairNF.isShortNF {W : WeierstrassCurve ℤ} (h : W.IsMinimalPairNF) : W.IsShortNF

A minimal-pair equation is short.

theorem WeierstrassCurve.IsMinimalPairNF.not_dvd_and_dvd {W : WeierstrassCurve ℤ} (h : W.IsMinimalPairNF) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) : ¬(↑ℓ ^ 4 ∣ W.a₄ ∧ ↑ℓ ^ 6 ∣ W.a₆)

No prime ℓ has both ℓ⁴ ∣ a₄ and ℓ⁶ ∣ a₆ for a minimal-pair equation.

theorem WeierstrassCurve.IsMinimalPairNF.of_forall_not_dvd {W : WeierstrassCurve ℤ} [W.IsShortNF] (h : ∀ (ℓ : ℕ), Nat.Prime ℓ → ¬(↑ℓ ^ 4 ∣ W.a₄ ∧ ↑ℓ ^ 6 ∣ W.a₆)) : W.IsMinimalPairNF

A short equation over ℤ such that no prime ℓ has both ℓ⁴ ∣ a₄ and ℓ⁶ ∣ a₆ is in minimal-pair normal form.

theorem WeierstrassCurve.IsMinimalPairNF.isUnit_of_pow_dvd {W : WeierstrassCurve ℤ} (h : W.IsMinimalPairNF) {x : ℤ} (h₄ : x ^ 4 ∣ W.a₄) (h₆ : x ^ 6 ∣ W.a₆) : IsUnit x

The only integers x with x⁴ ∣ a₄ and x⁶ ∣ a₆ for a minimal pair are ±1. This is the form in which the minimal-pair condition is consumed: it rules out every scaling of the equation but the sign.

theorem WeierstrassCurve.IsMinimalPairNF.eq_of_intCast_eq_pow_mul {W W' : WeierstrassCurve ℤ} (hW : W.IsMinimalPairNF) (hW' : W'.IsMinimalPairNF) {q : ℚ} (h₄ : ↑W'.a₄ = q ^ 4 * ↑W.a₄) (h₆ : ↑W'.a₆ = q ^ 6 * ↑W.a₆) : W' = W

Two minimal-pair equations related by a rational scaling coincide. If (a₄', a₆') = (q⁴a₄, q⁶a₆) for some q ∈ ℚ and both pairs are minimal, then q = ±1 and the equations are equal.

Bundled minimal-pair models

structure WeierstrassCurve.MinimalPairModel (E : WeierstrassCurve ℚ) [E.IsElliptic] : Type

A minimal-pair model of an elliptic curve E over ℚ: a minimal-pair short equation over ℤ whose base change is isomorphic to E over ℚ. The equation is unique (minimalPairModel_unique), so the type is a subsingleton. A change of variables realising the isomorphism is available as MinimalPairModel.variableChange; it is not part of the data, since it is unique only up to the automorphisms of E.

• model : WeierstrassCurve ℤ

  The integral short equation.

• isMinimalPair : self.model.IsMinimalPairNF

  It is short and a minimal pair.

• isomorphic : ∃ (C : VariableChange ℚ), C • self.model.baseChange ℚ = E

  Some change of variables carries the base-changed model to E.

theorem WeierstrassCurve.MinimalPairModel.ext_iff {E : WeierstrassCurve ℚ} {inst✝ : E.IsElliptic} {x y : E.MinimalPairModel} : x = y ↔ x.model = y.model

theorem WeierstrassCurve.MinimalPairModel.ext {E : WeierstrassCurve ℚ} {inst✝ : E.IsElliptic} {x y : E.MinimalPairModel} (model : x.model = y.model) : x = y

noncomputable def WeierstrassCurve.MinimalPairModel.variableChange {E : WeierstrassCurve ℚ} [E.IsElliptic] (M : E.MinimalPairModel) : VariableChange ℚ

A change of variables carrying the base change of the model to E, chosen from MinimalPairModel.isomorphic. It is not unique: composing it with an automorphism of E gives another.

Equations

• M.variableChange = ⋯.choose

@[simp]

theorem WeierstrassCurve.MinimalPairModel.variableChange_smul_baseChange {E : WeierstrassCurve ℚ} [E.IsElliptic] (M : E.MinimalPairModel) : M.variableChange • M.model.baseChange ℚ = E

The chosen change of variables carries the base change of the model to E.

instance WeierstrassCurve.MinimalPairModel.isElliptic_baseChange_model {E : WeierstrassCurve ℚ} [E.IsElliptic] (M : E.MinimalPairModel) : (M.model.baseChange ℚ).IsElliptic

The base change of a minimal-pair model is an elliptic curve, being isomorphic to E.

def WeierstrassCurve.MinimalPairModel.height {E : WeierstrassCurve ℚ} [E.IsElliptic] (M : E.MinimalPairModel) : ℕ

The height of a minimal-pair model: the shortEquationHeight of its equation.

Equations

• M.height = M.model.shortEquationHeight

@[simp]

theorem WeierstrassCurve.MinimalPairModel.height_def {E : WeierstrassCurve ℚ} [E.IsElliptic] (M : E.MinimalPairModel) : M.height = max (4 * M.model.a₄.natAbs ^ 3) (27 * M.model.a₆.natAbs ^ 2)

MinimalPairModel.height, unfolded. This is the interface to WeierstrassCurve.MinimalPairModel.height outside its defining module.

theorem WeierstrassCurve.MinimalPairModel.height_eq_of_model_eq {E : WeierstrassCurve ℚ} [E.IsElliptic] (M : E.MinimalPairModel) {N : E.MinimalPairModel} (h : M.model = N.model) : M.height = N.height

The height of a minimal-pair model depends only on its equation.

Existence

theorem WeierstrassCurve.exists_minimalPairModel (E : WeierstrassCurve ℚ) [E.IsElliptic] : Nonempty E.MinimalPairModel

Existence of a minimal-pair model: every elliptic curve over ℚ is isomorphic over ℚ to the base change of a minimal-pair short equation over ℤ.

noncomputable def WeierstrassCurve.minimalPairModel (E : WeierstrassCurve ℚ) [E.IsElliptic] : E.MinimalPairModel

A chosen minimal-pair model of an elliptic curve over ℚ. Its equation and its height do not depend on the choice (minimalPairModel_unique, naiveHeight_eq).

Equations

• E.minimalPairModel = Classical.choice ⋯

Uniqueness, and the naïve height of a curve

theorem WeierstrassCurve.minimalPairModel_unique (E : WeierstrassCurve ℚ) [E.IsElliptic] (M N : E.MinimalPairModel) : M.model = N.model

Uniqueness of the minimal-pair equation: any two minimal-pair models of E have the same equation, not merely isomorphic ones. Together with existence, this makes the height of the equation an invariant of the curve.

instance WeierstrassCurve.MinimalPairModel.instSubsingleton (E : WeierstrassCurve ℚ) [E.IsElliptic] : Subsingleton E.MinimalPairModel

Minimal-pair models of E form a subsingleton: their only data is the equation, and that is unique.

noncomputable def WeierstrassCurve.naiveHeight (E : WeierstrassCurve ℚ) [E.IsElliptic] : ℕ

The naïve height of an elliptic curve over ℚ: the height max (4|A|³) (27B²) of its minimal-pair equation y² = x³ + Ax + B. It can be computed from any minimal-pair model (naiveHeight_eq), is invariant under ℚ-isomorphism (naiveHeight_variableChange), and is the quantity by which tables of elliptic curves over ℚ are ordered.

Equations

• E.naiveHeight = E.minimalPairModel.height

theorem WeierstrassCurve.naiveHeight_eq {E : WeierstrassCurve ℚ} [E.IsElliptic] (M : E.MinimalPairModel) : E.naiveHeight = M.height

Every minimal-pair model computes the naïve height of the curve.

theorem WeierstrassCurve.naiveHeight_variableChange (E : WeierstrassCurve ℚ) [E.IsElliptic] (C : VariableChange ℚ) : (C • E).naiveHeight = E.naiveHeight

The naïve height is invariant under an admissible change of variables over ℚ.

Finiteness

theorem WeierstrassCurve.finite_shortEquations_bounded_height (H : ℕ) : {W : WeierstrassCurve ℤ | W.IsShortNF ∧ max (4 * W.a₄.natAbs ^ 3) (27 * W.a₆.natAbs ^ 2) ≤ H}.Finite

There are only finitely many short equations over ℤ of bounded height: the bound max (4|a₄|³) (27a₆²) ≤ H leaves |a₄|, |a₆| ≤ H, and the two coefficients determine a short equation.

theorem WeierstrassCurve.finite_minimalPairEquations_bounded_height (H : ℕ) : {W : WeierstrassCurve ℤ | W.IsMinimalPairNF ∧ (W.baseChange ℚ).IsElliptic ∧ max (4 * W.a₄.natAbs ^ 3) (27 * W.a₆.natAbs ^ 2) ≤ H}.Finite

There are only finitely many minimal-pair short equations of bounded height. The statement is about equations over ℤ in minimal-pair normal form: the set of all rational equations of a single curve is infinite, so finiteness of bounded-height ℚ-isomorphism classes is a consequence of this statement, not a statement about terms E : WeierstrassCurve ℚ.