Semistable elliptic curves over a Dedekind domain

Let O be a Dedekind domain with fraction field K. An elliptic curve over K is semistable over O when its reduction at every height-one prime is either good or multiplicative, equivalently never additive. Reduction is a property of a minimal equation, so the definition applies Mathlib's reduction predicates to a chosen local minimal equation.

This file proves both local characterizations of semistability. At a discrete valuation ring, a minimal equation is not additive exactly when either its discriminant or its c₄ has valuation one. Globally, this criterion is imposed at every height-one prime. It also proves that the predicate is independent of the equation presenting the curve: changing variables changes the chosen local minimal equation, but the two minimal equations have the same discriminant and c₄ valuations.

Main definitions

• WeierstrassCurve.IsSemistable: an elliptic equation whose local minimal equation has no additive reduction at any height-one prime.

Main results

• WeierstrassCurve.isSemistable_iff_forall_hasGoodReduction_or_hasMultiplicativeReduction: semistability is good or multiplicative reduction everywhere.
• WeierstrassCurve.not_hasAdditiveReduction_iff_valuation_Δ_eq_one_or_valuation_c₄_eq_one: the local valuation criterion on a minimal equation.
• WeierstrassCurve.isSemistable_iff_forall_valuation_Δ_eq_one_or_valuation_c₄_eq_one: the corresponding global criterion.
• WeierstrassCurve.isSemistable_smul: semistability is invariant under a change of variables.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.5 and VIII.8.

The local criterion

theorem WeierstrassCurve.not_hasAdditiveReduction_iff_valuation_Δ_eq_one_or_valuation_c₄_eq_one (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) [IsMinimal R W] : ¬HasAdditiveReduction R W ↔ (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ = 1 ∨ (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ = 1

A minimal equation is not additively reduced exactly when its discriminant or its c₄ is a unit at the place. A unit discriminant gives good reduction; a unit c₄ gives multiplicative reduction when the discriminant is not a unit.

This is valuation arithmetic on the equation itself, so no ellipticity is needed; IsSemistable adds that hypothesis where the trichotomy is read as a reduction type.

Semistability over a Dedekind domain

def WeierstrassCurve.IsSemistable (O : Type u_3) [CommRing O] [IsDedekindDomain O] {F : Type u_4} [Field F] [Algebra O F] [IsFractionRing O F] (W : WeierstrassCurve F) [_hE : W.IsElliptic] : Prop

Semistability over a Dedekind domain: at every height-one prime, a local minimal equation has no additive reduction. Equivalently, the reduction is good or multiplicative everywhere.

The predicate is stated on an elliptic equation but depends only on its F-isomorphism class, as proved by isSemistable_smul. The ellipticity instance excludes singular cubics, which have no reduction type in the good/multiplicative/additive trichotomy of elliptic curves.

Equations

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

theorem WeierstrassCurve.isSemistable_iff {O : Type u_3} [CommRing O] [IsDedekindDomain O] {F : Type u_4} [Field F] [Algebra O F] [IsFractionRing O F] {W : WeierstrassCurve F} [W.IsElliptic] : IsSemistable O W ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum O), ¬HasAdditiveReduction (Localization.AtPrime v.asIdeal) (minimal (Localization.AtPrime v.asIdeal) W)

Semistability means that every local minimal equation has no additive reduction.

theorem WeierstrassCurve.IsSemistable.not_hasAdditiveReduction {O : Type u_3} [CommRing O] [IsDedekindDomain O] {F : Type u_4} [Field F] [Algebra O F] [IsFractionRing O F] {W : WeierstrassCurve F} [W.IsElliptic] (h : IsSemistable O W) (v : IsDedekindDomain.HeightOneSpectrum O) : ¬HasAdditiveReduction (Localization.AtPrime v.asIdeal) (minimal (Localization.AtPrime v.asIdeal) W)

A semistable curve has no additive reduction at any height-one prime.

theorem WeierstrassCurve.IsSemistable.of_forall_not_hasAdditiveReduction {O : Type u_3} [CommRing O] [IsDedekindDomain O] {F : Type u_4} [Field F] [Algebra O F] [IsFractionRing O F] {W : WeierstrassCurve F} [W.IsElliptic] (h : ∀ (v : IsDedekindDomain.HeightOneSpectrum O), ¬HasAdditiveReduction (Localization.AtPrime v.asIdeal) (minimal (Localization.AtPrime v.asIdeal) W)) : IsSemistable O W

A curve with no additive reduction at every height-one prime is semistable.

theorem WeierstrassCurve.isSemistable_iff_forall_hasGoodReduction_or_hasMultiplicativeReduction {O : Type u_3} [CommRing O] [IsDedekindDomain O] {F : Type u_4} [Field F] [Algebra O F] [IsFractionRing O F] (W : WeierstrassCurve F) [W.IsElliptic] : IsSemistable O W ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum O), HasGoodReduction (Localization.AtPrime v.asIdeal) (minimal (Localization.AtPrime v.asIdeal) W) ∨ HasMultiplicativeReduction (Localization.AtPrime v.asIdeal) (minimal (Localization.AtPrime v.asIdeal) W)

A curve is semistable exactly when it has good or multiplicative reduction at every height-one prime.

theorem WeierstrassCurve.isSemistable_iff_forall_valuation_Δ_eq_one_or_valuation_c₄_eq_one {O : Type u_3} [CommRing O] [IsDedekindDomain O] {F : Type u_4} [Field F] [Algebra O F] [IsFractionRing O F] (W : WeierstrassCurve F) [W.IsElliptic] : IsSemistable O W ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum O), (IsDedekindDomain.HeightOneSpectrum.valuation F (IsDiscreteValuationRing.maximalIdeal (Localization.AtPrime v.asIdeal))) (minimal (Localization.AtPrime v.asIdeal) W).Δ = 1 ∨ (IsDedekindDomain.HeightOneSpectrum.valuation F (IsDiscreteValuationRing.maximalIdeal (Localization.AtPrime v.asIdeal))) (minimal (Localization.AtPrime v.asIdeal) W).c₄ = 1

The valuation criterion for semistability: at every height-one prime, a local minimal equation has a unit discriminant or a unit c₄; the latter gives multiplicative reduction when the discriminant is not a unit.

@[simp]

theorem WeierstrassCurve.isSemistable_smul {O : Type u_3} [CommRing O] [IsDedekindDomain O] {F : Type u_4} [Field F] [Algebra O F] [IsFractionRing O F] (D : VariableChange F) (W : WeierstrassCurve F) [W.IsElliptic] : IsSemistable O (D • W) ↔ IsSemistable O W

Semistability is invariant under a change of variables.