The abc quality of an elliptic curve over ℚ

Let E be an elliptic curve over ℚ with j-invariant j. Write j / 1728 = a / c in lowest terms with c > 0, and set b = c - a. Then a + b = c with a, b, c pairwise coprime. Since j = c₄³ / Δ and 1728 Δ = c₄³ - c₆², the triple (a, b, c) is the reduced form of (c₄³, -c₆², 1728 Δ). The abc quality of E is the quality of that triple, log max(|a|, |b|, |c|) / log rad(a b c).

The quality is defined only for j ≠ 0 and j ≠ 1728, which is exactly the condition a b c ≠ 0 (a = 0 exactly when j = 0, by Rat.num_ne_zero, and b = 0 exactly when j = 1728, by Rat.den_sub_num_ne_zero), and WeierstrassCurve.abcQuality takes it as a hypothesis. At j = 0 or j = 1728 the radical is rad 0 = 1, and the quotient would evaluate to 0 by division by zero: a meaningful-looking number where there is no invariant.

Main definitions

• WeierstrassCurve.abcQuality E h: the abc quality of E, for h : E.j ≠ 0 ∧ E.j ≠ 1728.

Main results

• WeierstrassCurve.abcQuality_eq_of_j_div_eq: the quality is computed by any triple of integers a + b = c with a and c coprime and j / 1728 = a / c, whatever the sign of c.
• WeierstrassCurve.abcQuality_eq_of_j_eq: the quality depends on j alone. In particular it is invariant under an admissible change of variables, WeierstrassCurve.variableChange_abcQuality.
• WeierstrassCurve.abcQuality_pos: the quality is positive.

Implementation notes

The radical is taken in ℕ, of |a b c|, and then cast to ℝ. Taken in ℝ it would be 1 for every nonzero argument, since every nonzero real number is a unit.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., GTM 106, Springer, 2009, §III.1: j = c₄³ / Δ and 1728 Δ = c₄³ - c₆².
• LMFDB, column abc_quality of ec_curvedata: "quality of the abc-triple associated to the j-invariant".

Provenance

abcQuality 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 defined for every elliptic curve over ℚ. Here it takes the hypothesis j ≠ 0 ∧ j ≠ 1728.

noncomputable def WeierstrassCurve.abcQuality (E : WeierstrassCurve ℚ) [E.IsElliptic] (_h : E.j ≠ 0 ∧ E.j ≠ 1728) : ℝ

The abc quality of an elliptic curve E over ℚ: with j / 1728 = a / c in lowest terms and b = c - a, the quality log max(|a|, |b|, |c|) / log rad(a b c) of the abc triple (a, b, c). The hypothesis j ≠ 0 ∧ j ≠ 1728 is exactly a b c ≠ 0; without it the quotient would be 0 by division by zero.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.abcQuality_def (E : WeierstrassCurve ℚ) [E.IsElliptic] (h : E.j ≠ 0 ∧ E.j ≠ 1728) : E.abcQuality h = Real.log (max (max ↑(E.j / 1728).num.natAbs ↑(↑(E.j / 1728).den - (E.j / 1728).num).natAbs) ↑(↑(E.j / 1728).den).natAbs) / Real.log ↑(UniqueFactorizationMonoid.radical ((E.j / 1728).num * (↑(E.j / 1728).den - (E.j / 1728).num) * ↑(E.j / 1728).den).natAbs)

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

theorem WeierstrassCurve.abcQuality_eq_of_j_div_eq (E : WeierstrassCurve ℚ) [E.IsElliptic] (h : E.j ≠ 0 ∧ E.j ≠ 1728) {a b c : ℤ} (hac : IsCoprime a c) (habc : a + b = c) (hj : E.j / 1728 = ↑a / ↑c) : E.abcQuality h = Real.log (max (max ↑a.natAbs ↑b.natAbs) ↑c.natAbs) / Real.log ↑(UniqueFactorizationMonoid.radical (a * b * c).natAbs)

The abc quality is the quality of any reduced triple for j / 1728: if a + b = c with a and c coprime and j / 1728 = a / c, then the abc quality of E is log max(|a|, |b|, |c|) / log rad(a b c). The sign of c is arbitrary.

theorem WeierstrassCurve.abcQuality_eq_of_j_eq (E : WeierstrassCurve ℚ) [E.IsElliptic] (h : E.j ≠ 0 ∧ E.j ≠ 1728) {E' : WeierstrassCurve ℚ} [E'.IsElliptic] (h' : E'.j ≠ 0 ∧ E'.j ≠ 1728) (hj : E.j = E'.j) : E.abcQuality h = E'.abcQuality h'

The abc quality depends on j alone: two elliptic curves over ℚ with the same j-invariant have the same abc quality.

theorem WeierstrassCurve.variableChange_abcQuality (E : WeierstrassCurve ℚ) [E.IsElliptic] (C : VariableChange ℚ) (h' : (C • E).j ≠ 0 ∧ (C • E).j ≠ 1728) (h : E.j ≠ 0 ∧ E.j ≠ 1728) : (C • E).abcQuality h' = E.abcQuality h

The abc quality is invariant under an admissible change of variables over ℚ.

theorem WeierstrassCurve.abcQuality_pos (E : WeierstrassCurve ℚ) [E.IsElliptic] (h : E.j ≠ 0 ∧ E.j ≠ 1728) : 0 < E.abcQuality h

The abc quality is positive.