Potential good reduction

Let R be a discrete valuation ring with fraction field K. An elliptic curve over K has potential good reduction when it acquires good reduction after a finite extension of K: there are a finite extension L / K and a discrete valuation ring S with fraction field L dominating R, such that a minimal equation of the curve over S has good reduction.

The minimal model is taken after the base change. An equation that is minimal over R need not stay minimal over S, and Mathlib's HasGoodReduction holds only for minimal equations, so asking HasGoodReduction S (W.baseChange L) would make the predicate depend on the chosen model over K.

Over a complete R the valuation of K extends uniquely to L (Neukirch, Algebraic Number Theory, II.4.8), so the integral closure of R in L is the only discrete valuation ring with fraction field L dominating R; then S is forced and the definition is the usual one. For a general R the place of L above R is part of the data being quantified over.

The main result is the j-invariant criterion (Silverman VII.5.5): an elliptic curve has potential good reduction exactly when its j-invariant is integral. The necessary direction holds in every residue characteristic. Its proof reads j = c₄ ³ / Δ on a minimal model with good reduction over S, where Δ is a unit, and descends integrality from S to R because R, a valuation ring, is integrally closed against every ring dominating it. In particular a curve with multiplicative reduction, whose j-invariant has a pole, never has potential good reduction.

The sufficient direction holds in every residue characteristic as well, by two normal forms, since 2 and 3 cannot both lie in the maximal ideal of R. In both cases the curve is first put in the normal form over a finite separable extension of K, whose j-invariant is still integral at a discrete valuation ring of the extension dominating R.

• When 2 is a unit, the curve takes the Legendre form y² = x (x - 1) (x + B), whose j-invariant is 256 (B² + B + 1)³ / (B² (B + 1)²). If it is integral then so are B, 1 / B and -1 / (B + 1), being roots of a monic polynomial with integral coefficients, so the discriminant 16 B² (B + 1)² is a unit.
• When 3 is a unit, the curve takes the Deuring normal form y² + axy + y = x³, whose j-invariant is a³ (a³ - 24)³ / (a³ - 27). If it is integral then so is a, a root of a monic polynomial with integral coefficients, and the discriminant a³ - 27 divides 3⁶, so it is a unit.

Main definitions

• WeierstrassCurve.HasPotentialGoodReduction: good reduction after some finite extension.

Main results

• WeierstrassCurve.HasGoodReduction.hasPotentialGoodReduction: good reduction is potentially good.
• WeierstrassCurve.hasPotentialGoodReduction_smul: potential good reduction is invariant under a change of variables.
• WeierstrassCurve.HasGoodReduction.isInteger_j: a minimal equation with good reduction has integral j-invariant.
• WeierstrassCurve.HasPotentialGoodReduction.isElliptic: a curve with potential good reduction is elliptic.
• WeierstrassCurve.HasPotentialGoodReduction.isInteger_j: a curve with potential good reduction has integral j-invariant.
• WeierstrassCurve.HasMultiplicativeReduction.not_isInteger_j and WeierstrassCurve.HasMultiplicativeReduction.not_hasPotentialGoodReduction: multiplicative reduction gives a nonintegral j-invariant, so it is not potentially good.
• WeierstrassCurve.hasGoodReduction_freyCurve_one: a curve y² = x (x - 1) (x + B) in Legendre form with integral j-invariant has good reduction where 2 is a unit.
• WeierstrassCurve.hasGoodReduction_deuringNormalForm: a curve y² + axy + y = x³ in Deuring normal form with integral j-invariant has good reduction where 3 is a unit.
• WeierstrassCurve.hasPotentialGoodReduction_of_isInteger_j and WeierstrassCurve.hasPotentialGoodReduction_iff_isInteger_j: a curve with integral j-invariant has potential good reduction, so the criterion is an equivalence.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.5.4, VII.5.5 and Appendix A, Proposition 1.3.
• J. Neukirch, Algebraic Number Theory, II.4.8.

def WeierstrassCurve.HasPotentialGoodReduction (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] (W : WeierstrassCurve K) : Prop

Potential good reduction: after some finite extension L of K, at some discrete valuation ring S with fraction field L dominating R, a minimal equation of W has good reduction. The maps R → S → L and R → K → L are required to agree, so that S lies over R. The field L and the ring S are taken in the universe of K.

Over a complete R, the integral closure of R in L is the only such ring S, so this is the usual notion of good reduction over the ring of integers of a finite extension.

theorem WeierstrassCurve.hasPotentialGoodReduction_iff {R : Type v} [CommRing R] {K : Type u} [Field K] [Algebra R K] {W : WeierstrassCurve K} : HasPotentialGoodReduction R W ↔ ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (_ : FiniteDimensional K L) (S : Type u) (x_3 : CommRing S) (x_4 : IsDomain S) (x_5 : IsDiscreteValuationRing S) (x_6 : Algebra S L) (x_7 : IsFractionRing S L) (x_8 : Algebra R S) (_ : IsLocalHom (algebraMap R S)), (algebraMap S L).comp (algebraMap R S) = (algebraMap K L).comp (algebraMap R K) ∧ HasGoodReduction S (minimal S (W.baseChange L))

Potential good reduction unfolded: good reduction of a minimal equation after a finite extension, at a discrete valuation ring dominating R.

theorem WeierstrassCurve.HasPotentialGoodReduction.intro (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] {W : WeierstrassCurve K} (L : Type u) [Field L] [Algebra K L] [FiniteDimensional K L] (S : Type u) [CommRing S] [IsDomain S] [IsDiscreteValuationRing S] [Algebra S L] [IsFractionRing S L] [Algebra R S] [IsLocalHom (algebraMap R S)] (h : (algebraMap S L).comp (algebraMap R S) = (algebraMap K L).comp (algebraMap R K)) (hW : HasGoodReduction S (minimal S (W.baseChange L))) : HasPotentialGoodReduction R W

Introducing potential good reduction from a finite extension L / K and a discrete valuation ring S with fraction field L, dominating R, over which a minimal equation of W has good reduction.

@[simp]

theorem WeierstrassCurve.hasPotentialGoodReduction_smul (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] (D : VariableChange K) (W : WeierstrassCurve K) : HasPotentialGoodReduction R (D • W) ↔ HasPotentialGoodReduction R W

Potential good reduction is invariant under a change of variables, so it is a property of the curve rather than of the equation presenting it.

theorem WeierstrassCurve.HasPotentialGoodReduction.isElliptic (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] {W : WeierstrassCurve K} (h : HasPotentialGoodReduction R W) : W.IsElliptic

A curve with potential good reduction is elliptic: its discriminant becomes a unit after the finite extension at which a minimal equation has good reduction, so it is nonzero.

The j-invariant

theorem WeierstrassCurve.HasGoodReduction.isInteger_j (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] (h : HasGoodReduction R W) : IsLocalization.IsInteger R W.j

A minimal equation with good reduction has integral j-invariant: its c₄ is integral and its discriminant is a unit, so j = c₄ ³ / Δ is integral.

theorem WeierstrassCurve.HasPotentialGoodReduction.isInteger_j (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] (h : HasPotentialGoodReduction R W) : IsLocalization.IsInteger R W.j

A curve with potential good reduction has integral j-invariant (Silverman VII.5.5, the necessary direction): j lies in the image of R.

theorem WeierstrassCurve.HasMultiplicativeReduction.not_isInteger_j (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] (h : HasMultiplicativeReduction R W) : ¬IsLocalization.IsInteger R W.j

Multiplicative reduction gives a nonintegral j-invariant: on a minimal equation with multiplicative reduction, c₄ is a unit while Δ is not, so j = c₄ ³ / Δ has a pole.

theorem WeierstrassCurve.HasMultiplicativeReduction.not_hasPotentialGoodReduction (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] (h : HasMultiplicativeReduction R W) : ¬HasPotentialGoodReduction R W

Multiplicative reduction is not potentially good.

The Legendre form

theorem WeierstrassCurve.hasGoodReduction_freyCurve_one (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] (h2 : IsUnit 2) {B : K} [(TauCeti.freyCurve 1 B).IsElliptic] (hj : IsLocalization.IsInteger R (TauCeti.freyCurve 1 B).j) : HasGoodReduction R (TauCeti.freyCurve 1 B)

A curve in Legendre form with integral j-invariant has good reduction over a discrete valuation ring in which 2 is a unit. The curve is y² = x (x - 1) (x + B), that is TauCeti.freyCurve 1 B.

The j-invariant 256 (B² + B + 1)³ / (B² (B + 1)²) forces B, 1 / B and -1 / (B + 1) to be roots of the monic polynomial (X² + X + 1)³ - (j / 256) X² (X + 1)², so B and B + 1 are units of R. The discriminant 16 B² (B + 1)² of the integral equation is then a unit too (Silverman, AEC, VII.5.5).

The Deuring normal form

theorem WeierstrassCurve.hasGoodReduction_deuringNormalForm (R : Type v) [CommRing R] {K : Type u} [Field K] [Algebra R K] [IsDomain R] [IsDiscreteValuationRing R] [IsFractionRing R K] (h3 : IsUnit 3) {a : K} [(deuringNormalForm a).IsElliptic] (hj : IsLocalization.IsInteger R (deuringNormalForm a).j) : HasGoodReduction R (deuringNormalForm a)

A curve in Deuring normal form with integral j-invariant has good reduction over a discrete valuation ring in which 3 is a unit. The curve is y² + axy + y = x³, that is WeierstrassCurve.deuringNormalForm a (Silverman, AEC, VII.5.5).

theorem WeierstrassCurve.HasGoodReduction.hasPotentialGoodReduction (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} (h : HasGoodReduction R W) : HasPotentialGoodReduction R W

Good reduction is potentially good, taking the trivial extension L = K, S = R. Here R lives in the universe of K, since HasPotentialGoodReduction takes S there.

theorem WeierstrassCurve.hasPotentialGoodReduction_of_isInteger_j (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] (hj : IsLocalization.IsInteger R W.j) : HasPotentialGoodReduction R W

Integral j-invariant gives potential good reduction (Silverman VII.5.5, the sufficient direction), in every residue characteristic: an elliptic curve over K whose j-invariant is integral, that is lies in the discrete valuation ring R, has potential good reduction.

Here R lives in the universe of K, as in WeierstrassCurve.HasGoodReduction.hasPotentialGoodReduction, since the discrete valuation ring witnessing the good reduction is built in the universe of a finite extension of K.

theorem WeierstrassCurve.hasPotentialGoodReduction_iff_isInteger_j (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [W.IsElliptic] : HasPotentialGoodReduction R W ↔ IsLocalization.IsInteger R W.j

The j-invariant criterion for potential good reduction (Silverman VII.5.5): an elliptic curve has potential good reduction exactly when its j-invariant is integral.