The Szpiro ratio and Szpiro's conjectures over ℚ

Let E be an elliptic curve over ℚ, with minimal discriminant Δ_min and conductor N. Here |Δ_min| is the norm of the minimal discriminant ideal WeierstrassCurve.minimalDiscriminantIdeal of E over ℤ, which is also |Δ| of the reduced minimal model (WeierstrassCurve.absNorm_minimalDiscriminantIdeal), and N is the norm of the algorithmic conductor WeierstrassCurve.algorithmicConductor, the product of the prime powers p ^ f_p whose exponents f_p = v_p(Δ_min) - m_p + 1 are read off Tate's algorithm.

The Szpiro ratio of E is log |Δ_min| / log N, defined when N > 1, that is, when E has bad reduction at some prime (WeierstrassCurve.one_lt_absNorm_algorithmicConductor_iff). It is the exponent σ with N ^ σ = |Δ_min|, and it is at least 1 because N divides Δ_min. Szpiro's conjecture asserts |Δ_min| ≪_ε N ^ (6 + ε) for every ε > 0, uniformly in E: with |Δ_min| ≤ C N ^ (6 + ε), the Szpiro ratio is at most 6 + ε + log C / log N. The modified Szpiro conjecture asserts the stronger bound max (|c₄|³, c₆²) ≪_ε N ^ (6 + ε), with c₄ and c₆ the invariants of a minimal equation. Since 1728 Δ = c₄³ - c₆², the modified conjecture implies the original one. Neither conjecture is proved here.

The abc conjecture (TauCeti.AbcConjecture) implies the modified Szpiro conjecture. Take the reduced minimal model and divide c₆² + 1728 Δ = c₄³ by g = gcd (c₄³, c₆²) to obtain a coprime triple. abc bounds max (|c₄|³, c₆²) / g by a power 1 + ε of the radical of 6 c₄ c₆ Δ, and g times that radical divides 432 c₄ c₆ N: minimality bounds the common factor g (WeierstrassCurve.IsGlobalMinimal.dvd_six_of_pow_dvd), and a prime p ≥ 5 dividing g is a prime of additive reduction, so p² divides N (WeierstrassCurve.IsGlobalMinimal.sq_dvd_absNorm_algorithmicConductor_iff). Since |c₄ c₆| ≤ max (|c₄|³, c₆²) ^ (5 / 6), this gives max (|c₄|³, c₆²) ≪_ε N ^ (6 + ε). When c₄ c₆ = 0, that is, when j is 0 or 1728, minimality alone bounds the invariants by N⁶.

By Ogg's formula the algorithmic conductor is the conductor of E. That identification is not formalised, so the ratio and the conjectures are stated against the algorithmic conductor and are named for it. For a semistable curve, such as the Frey curve of a solution of Fermat's equation, every exponent f_p is 0 or 1, and N is the radical of Δ_min.

Main definitions

• WeierstrassCurve.algorithmicSzpiroRatio E h: the Szpiro ratio log |Δ_min| / log N, for h : 1 < N.
• TauCeti.AlgorithmicSzpiroConjecture: Szpiro's conjecture |Δ_min| ≪_ε N ^ (6 + ε).
• TauCeti.AlgorithmicModifiedSzpiroConjecture: the modified Szpiro conjecture max (|c₄|³, c₆²) ≪_ε N ^ (6 + ε).

Main results

• TauCeti.algorithmicSzpiroConjecture_iff, TauCeti.algorithmicModifiedSzpiroConjecture_iff: the defining characterizations of the two conjectures.
• WeierstrassCurve.rpow_algorithmicSzpiroRatio: N ^ σ = |Δ_min| for the Szpiro ratio σ, and WeierstrassCurve.algorithmicSzpiroRatio_le_iff: σ ≤ r exactly when |Δ_min| ≤ N ^ r.
• WeierstrassCurve.one_le_algorithmicSzpiroRatio: the Szpiro ratio is at least 1.
• WeierstrassCurve.algorithmicSzpiroRatio_smul: the Szpiro ratio is invariant under a change of variables.
• TauCeti.AlgorithmicModifiedSzpiroConjecture.algorithmicSzpiroConjecture: the modified Szpiro conjecture implies Szpiro's conjecture.
• TauCeti.AbcConjecture.algorithmicModifiedSzpiroConjecture: the abc conjecture implies the modified Szpiro conjecture.

References

• L. Szpiro, Discriminant et conducteur des courbes elliptiques, Astérisque 183 (1990), 7–18.
• J. Oesterlé, Nouvelles approches du « théorème » de Fermat, Séminaire Bourbaki 694 (1988), Astérisque 161–162 (1988), 165–186.
• J. Silverman, The Arithmetic of Elliptic Curves, III.1 (1728 Δ = c₄³ - c₆²) and VIII.11.

noncomputable def WeierstrassCurve.algorithmicSzpiroRatio (E : WeierstrassCurve ℚ) [E.IsElliptic] (_h : 1 < Ideal.absNorm (algorithmicConductor ℤ E)) : ℝ

The Szpiro ratio log |Δ_min| / log N of an elliptic curve over ℚ, where |Δ_min| is the norm of the minimal discriminant ideal over ℤ and N that of the algorithmic conductor. The hypothesis 1 < N makes the denominator nonzero; without it the quotient would be 0 by division by zero.

theorem WeierstrassCurve.algorithmicSzpiroRatio_def (E : WeierstrassCurve ℚ) [E.IsElliptic] (h : 1 < Ideal.absNorm (algorithmicConductor ℤ E)) : E.algorithmicSzpiroRatio h = Real.log ↑(Ideal.absNorm (minimalDiscriminantIdeal ℤ E)) / Real.log ↑(Ideal.absNorm (algorithmicConductor ℤ E))

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

theorem WeierstrassCurve.rpow_algorithmicSzpiroRatio (E : WeierstrassCurve ℚ) [E.IsElliptic] (h : 1 < Ideal.absNorm (algorithmicConductor ℤ E)) : ↑(Ideal.absNorm (algorithmicConductor ℤ E)) ^ E.algorithmicSzpiroRatio h = ↑(Ideal.absNorm (minimalDiscriminantIdeal ℤ E))

The Szpiro ratio is the exponent of N giving |Δ_min|: N ^ σ = |Δ_min|.

theorem WeierstrassCurve.algorithmicSzpiroRatio_le_iff (E : WeierstrassCurve ℚ) [E.IsElliptic] (h : 1 < Ideal.absNorm (algorithmicConductor ℤ E)) {r : ℝ} : E.algorithmicSzpiroRatio h ≤ r ↔ ↑(Ideal.absNorm (minimalDiscriminantIdeal ℤ E)) ≤ ↑(Ideal.absNorm (algorithmicConductor ℤ E)) ^ r

The Szpiro ratio is at most r exactly when |Δ_min| ≤ N ^ r.

theorem WeierstrassCurve.one_le_algorithmicSzpiroRatio (E : WeierstrassCurve ℚ) [E.IsElliptic] (h : 1 < Ideal.absNorm (algorithmicConductor ℤ E)) : 1 ≤ E.algorithmicSzpiroRatio h

The Szpiro ratio is at least 1, since the algorithmic conductor divides the minimal discriminant ideal.

@[simp]

theorem WeierstrassCurve.algorithmicSzpiroRatio_smul (E : WeierstrassCurve ℚ) [E.IsElliptic] (C : VariableChange ℚ) (h : 1 < Ideal.absNorm (algorithmicConductor ℤ (C • E))) : (C • E).algorithmicSzpiroRatio h = E.algorithmicSzpiroRatio ⋯

The Szpiro ratio is invariant under a change of variables, so it is an invariant of the curve and not of the equation presenting it.

def TauCeti.AlgorithmicSzpiroConjecture : Prop

Szpiro's conjecture, against the algorithmic conductor: for every ε > 0 there is a constant C such that every elliptic curve over ℚ satisfies |Δ_min| ≤ C N ^ (6 + ε), where |Δ_min| is the norm of the minimal discriminant ideal over ℤ and N that of the algorithmic conductor.

theorem TauCeti.algorithmicSzpiroConjecture_iff : AlgorithmicSzpiroConjecture ↔ ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), ∀ (E : WeierstrassCurve ℚ) [inst : E.IsElliptic], ↑(Ideal.absNorm (WeierstrassCurve.minimalDiscriminantIdeal ℤ E)) ≤ C * ↑(Ideal.absNorm (WeierstrassCurve.algorithmicConductor ℤ E)) ^ (6 + ε)

The defining characterization of TauCeti.AlgorithmicSzpiroConjecture. This is the interface to it outside its defining module.

def TauCeti.AlgorithmicModifiedSzpiroConjecture : Prop

The modified Szpiro conjecture, against the algorithmic conductor: for every ε > 0 there is a constant C such that every elliptic curve over ℚ satisfies max (|c₄|³, c₆²) ≤ C N ^ (6 + ε), where c₄ and c₆ are the invariants of the reduced minimal model and N is the norm of the algorithmic conductor. The invariants of any globally minimal equation have the same absolute values, as such equations differ by changes of variables over ℤ with u = ±1.

theorem TauCeti.algorithmicModifiedSzpiroConjecture_iff : AlgorithmicModifiedSzpiroConjecture ↔ ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ), ∀ (E : WeierstrassCurve ℚ) [inst : E.IsElliptic], max (|↑E.reducedMinimalModel.c₄| ^ 3) (↑E.reducedMinimalModel.c₆ ^ 2) ≤ C * ↑(Ideal.absNorm (WeierstrassCurve.algorithmicConductor ℤ E)) ^ (6 + ε)

The defining characterization of TauCeti.AlgorithmicModifiedSzpiroConjecture. This is the interface to it outside its defining module.

theorem TauCeti.AlgorithmicModifiedSzpiroConjecture.algorithmicSzpiroConjecture (h : AlgorithmicModifiedSzpiroConjecture) : AlgorithmicSzpiroConjecture

The modified Szpiro conjecture implies Szpiro's conjecture, with the same constants: the relation 1728 Δ = c₄³ - c₆² on the reduced minimal model gives |Δ_min| ≤ max (|c₄|³, c₆²).

The abc conjecture implies the modified Szpiro conjecture

theorem TauCeti.AbcConjecture.algorithmicModifiedSzpiroConjecture (h : AbcConjecture) : AlgorithmicModifiedSzpiroConjecture

The abc conjecture implies the modified Szpiro conjecture (Oesterlé), against the algorithmic conductor: for every ε > 0 there is a constant C with max (|c₄|³, c₆²) ≤ C N ^ (6 + ε) for every elliptic curve over ℚ, where c₄ and c₆ are the invariants of its reduced minimal model and N is the norm of its algorithmic conductor. With TauCeti.AlgorithmicModifiedSzpiroConjecture.algorithmicSzpiroConjecture, abc therefore implies Szpiro's conjecture as well.