Local obstruction exponents of Weierstrass equations #

Let O be a Dedekind domain with fraction field K, let v be a height-one prime of O, and let W be an elliptic Weierstrass equation over K. The local obstruction exponent is

f_v(W) = (v(Delta W) - v(Delta_min,v)) / 12.

The numerator is divisible by twelve because an admissible change of variables scales the discriminant by the inverse twelfth power of its u-parameter. It is useful to define the exponent for every rational equation, with values in ℤ: local integrality is a sufficient hypothesis for nonnegativity, while a nonintegral equation may have negative defect.

These exponents are the local data assembled by the defect ideal of an integral equation. The reconstruction formula in this file is the interface that construction needs; it avoids relying on integer division or unfolding the definition.

Main definitions #

WeierstrassCurve.obstructionExponentAt: the local discriminant defect divided by twelve.
WeierstrassCurve.IsSharpSemiGlobalMinimalAt: an integral equation minimal away from one prime and having obstruction exponent exactly one there.

Main results #

WeierstrassCurve.twelve_dvd_ord_Δ_sub_localMinimalDiscriminantValuation: the discriminant defect of every rational equation is divisible by twelve.
WeierstrassCurve.twelve_mul_obstructionExponentAt: the exact reconstruction formula.
WeierstrassCurve.obstructionExponentAt_smul: the change-of-variables formula.
WeierstrassCurve.obstructionExponentAt_nonneg_of_isIntegral: local integrality makes the obstruction exponent nonnegative.
WeierstrassCurve.obstructionExponentAt_eq_zero_iff_isMinimal: for a locally integral equation, vanishing of the obstruction exponent is equivalent to local minimality.
WeierstrassCurve.isGlobalMinimal_iff_obstructionExponentAt_eq_zero: an integral equation is globally minimal exactly when all its local obstruction exponents vanish.
WeierstrassCurve.IsSharpSemiGlobalMinimalAt.isSemiGlobalMinimal: sharp semi-global minimality implies the weak semi-global predicate.

References #

J. Silverman, The Arithmetic of Elliptic Curves, VIII.8.

source

theorem WeierstrassCurve.twelve_dvd_ord_Δ_sub_localMinimalDiscriminantValuation (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] :

12 ∣ (IsDedekindDomain.HeightOneSpectrum.valuation K v).ord W.Δ - ↑(localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W)

The difference between the discriminant valuation of an equation and the local minimal valuation is divisible by twelve. An admissible change of variables scales the discriminant by the inverse twelfth power of its u-parameter.

source

noncomputable def WeierstrassCurve.obstructionExponentAt (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] :

ℤ

The local obstruction exponent f_v(W) = (v(Delta W) - v(Delta_min,v)) / 12.

It is integer-valued for every rational equation. Local integrality is not part of the definition: it is the hypothesis that makes the exponent nonnegative, as proved by obstructionExponentAt_nonneg_of_isIntegral.

Equations

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

Instances For

source

@[simp]

theorem WeierstrassCurve.twelve_mul_obstructionExponentAt (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] :

12 * obstructionExponentAt O v W = (IsDedekindDomain.HeightOneSpectrum.valuation K v).ord W.Δ - ↑(localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W)

Twelve times the local obstruction exponent is the discriminant defect. This is the characteristic elimination lemma for obstructionExponentAt; consumers need not reason about integer division.

source

@[simp]

theorem WeierstrassCurve.obstructionExponentAt_smul (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (C : VariableChange K) (W : WeierstrassCurve K) [W.IsElliptic] :

obstructionExponentAt O v (C • W) = obstructionExponentAt O v W - (IsDedekindDomain.HeightOneSpectrum.valuation K v).ord ↑C.u

Changing variables subtracts the order of the scaling parameter from the local obstruction exponent.

source

theorem WeierstrassCurve.obstructionExponentAt_nonneg_of_isIntegral (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] [IsIntegral (Localization.AtPrime v.asIdeal) W] :

0 ≤ obstructionExponentAt O v W

Local integrality makes the local obstruction exponent nonnegative. Without integrality the exponent remains defined but may be negative.

source

@[simp]

theorem WeierstrassCurve.obstructionExponentAt_eq_zero_iff_isMinimal (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] [IsIntegral (Localization.AtPrime v.asIdeal) W] :

obstructionExponentAt O v W = 0 ↔ IsMinimal (Localization.AtPrime v.asIdeal) W

For a locally integral equation, the obstruction exponent vanishes exactly when the equation is minimal at that prime.

source

theorem WeierstrassCurve.isGlobalMinimal_iff_obstructionExponentAt_eq_zero (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve K) [W.IsElliptic] [IsIntegral O W] :

IsGlobalMinimal O W ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum O), obstructionExponentAt O v W = 0

An integral equation is globally minimal exactly when all of its local obstruction exponents vanish.

source

def WeierstrassCurve.IsSharpSemiGlobalMinimalAt (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (v₀ : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] :

Prop

A sharply semi-global model at v₀ is integral at v₀, minimal at every other height-one prime, and has discriminant defect exactly twelve at v₀. Unlike weak semi-global minimality, which permits any defect at its exceptional prime, this pins the defect to the smallest positive value, so the model's defect ideal is exactly 𝔭_{v₀}.

Equations