The minimal discriminant ideal of an elliptic curve over a Dedekind domain

Let O be a Dedekind domain with fraction field K and let W be an elliptic Weierstrass equation over K. At each height-one prime v of O the localisation Oᵥ = Localization.AtPrime v.asIdeal is a discrete valuation ring, and WeierstrassCurve.localMinimalDiscriminantValuation reads off the exponent v (Δ_min,ᵥ) of a Weierstrass equation minimal over Oᵥ. This file assembles those exponents into a single ideal of O,

𝔇_{E/K} = ∏ᵥ 𝔭ᵥ ^ v (Δ_min,ᵥ),

the minimal discriminant ideal (Silverman, The Arithmetic of Elliptic Curves, VIII.8).

Each exponent is invariant under a change of variables, so the ideal depends only on the K-isomorphism class of the curve and not on the equation presenting it. Against an equation that is already integral over O it is comparable with the actual discriminant: the local exponents never exceed those of Δ W, with equality at v exactly when W is minimal there, so 𝔇_{E/K} = (Δ W) characterises global minimality among integral equations. Accordingly, this characterisation is stated only for equations integral over O.

The obstruction exponents (v (Δ W) − v (Δ_min,ᵥ)) / 12 of an integral equation, the integral defect ideal they assemble into, and its class in ClassGroup O are not defined here.

Main definitions

• WeierstrassCurve.minimalDiscriminantIdeal: the ideal ∏ᵥ 𝔭ᵥ ^ v (Δ_min,ᵥ) of O.

Main results

• WeierstrassCurve.count_span_Δ_eq_ord_Δ: the exponent of a prime in the discriminant ideal is the additive valuation of the discriminant.
• WeierstrassCurve.count_span_Δ_eq_localMinimalDiscriminantValuation: at a prime where the equation is minimal, the exponent of 𝔭ᵥ in (Δ W) is v (Δ_min,ᵥ).
• WeierstrassCurve.localMinimalDiscriminantValuation_le_count_span_Δ: for an integral equation the local minimal exponent never exceeds that of Δ W.
• WeierstrassCurve.minimalDiscriminantIdeal_smul: the ideal is invariant under a change of variables, hence an invariant of the curve rather than of the equation.
• WeierstrassCurve.hasFiniteMulSupport_pow_localMinimalDiscriminantValuation and WeierstrassCurve.minimalDiscriminantIdeal_ne_bot: the defining product is finite and nonzero.
• WeierstrassCurve.count_minimalDiscriminantIdeal_eq_localMinimalDiscriminantValuation: the exponent of 𝔭ᵥ in 𝔇_{E/K} is v (Δ_min,ᵥ), which recovers each local exponent from the ideal.
• WeierstrassCurve.minimalDiscriminantIdeal_dvd_span: for an integral equation, the minimal discriminant ideal divides the ideal generated by its discriminant.
• WeierstrassCurve.minimalDiscriminantIdeal_eq_span_of_isGlobalMinimal and WeierstrassCurve.isGlobalMinimal_iff_minimalDiscriminantIdeal_eq_span: a globally minimal equation computes the ideal as (Δ W), and among integral equations that identity holds only for the globally minimal ones.

References

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

theorem WeierstrassCurve.valuation_Δ_eq_exp_neg_localMinimalDiscriminantValuation (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve K) (v : IsDedekindDomain.HeightOneSpectrum O) [W.IsElliptic] {W' : WeierstrassCurve K} [IsMinimal (Localization.AtPrime v.asIdeal) W'] (D : VariableChange K) (hD : D • W = W') : (IsDedekindDomain.HeightOneSpectrum.valuation K v) W'.Δ = WithZero.exp (-↑(localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W))

The discriminant of an equation minimal at v has v-adic valuation exp (-v (Δ_min,ᵥ)). This is valuation_Δ_eq_exp_neg_of_isMinimal_smul read through the v-adic valuation of O rather than through the discrete valuation of Oᵥ.

theorem WeierstrassCurve.count_span_Δ_eq_ord_Δ {O : Type u_1} [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve K) (v : IsDedekindDomain.HeightOneSpectrum O) [W.IsElliptic] {d : O} (hd : (algebraMap O K) d = W.Δ) : ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {d})).factors) = (IsDedekindDomain.HeightOneSpectrum.valuation K v).ord W.Δ

The exponent of 𝔭ᵥ in the discriminant ideal is the additive valuation of the discriminant. This is the bridge between unique factorisation of the principal ideal (d) and the order function used by the local obstruction exponent.

theorem WeierstrassCurve.count_span_Δ_eq_localMinimalDiscriminantValuation {O : Type u_1} [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve K) (v : IsDedekindDomain.HeightOneSpectrum O) [W.IsElliptic] {d : O} (hd : (algebraMap O K) d = W.Δ) (hv : IsMinimal (Localization.AtPrime v.asIdeal) W) : (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {d})).factors = localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W

At a prime where the equation is minimal, the exponent of 𝔭ᵥ in the discriminant is v (Δ_min,ᵥ). Here d is a global integral representative of Δ W, supplied separately by the hypothesis hd; minimality at v supplies only integrality over the localisation.

theorem WeierstrassCurve.localMinimalDiscriminantValuation_le_count_span_Δ {O : Type u_1} [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve K) (v : IsDedekindDomain.HeightOneSpectrum O) [W.IsElliptic] [IsIntegral O W] {d : O} (hd : (algebraMap O K) d = W.Δ) : localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W ≤ (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {d})).factors

An integral equation has discriminant exponent at least the local minimal one at every prime. Minimality maximises the multiplicative valuation of the discriminant, which is to minimise its exponent.

noncomputable def WeierstrassCurve.minimalDiscriminantIdeal (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] : Ideal O

The minimal discriminant ideal 𝔇_{E/K} = ∏ᵥ 𝔭ᵥ ^ v (Δ_min,ᵥ): the product over the height-one primes of O of the local minimal discriminants of W. The product is finite (hasFiniteMulSupport_pow_localMinimalDiscriminantValuation): after choosing an integral model, only finitely many primes divide its nonzero discriminant ideal, and every local minimal exponent is bounded by that ideal's multiplicity.

Equations

• WeierstrassCurve.minimalDiscriminantIdeal O W = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum O), v.asIdeal ^ WeierstrassCurve.localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W

@[simp]

theorem WeierstrassCurve.minimalDiscriminantIdeal_smul (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (D : VariableChange K) (W : WeierstrassCurve K) [W.IsElliptic] : minimalDiscriminantIdeal O (D • W) = minimalDiscriminantIdeal O W

The minimal discriminant ideal is invariant under a change of variables, so it is an invariant of the curve and not of the equation presenting it.

theorem WeierstrassCurve.hasFiniteMulSupport_pow_localMinimalDiscriminantValuation (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] : Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum O) => v.asIdeal ^ localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W

The product defining the minimal discriminant ideal is finite. Thus the defining finprod agrees with a finite product of the nontrivial local factors.

theorem WeierstrassCurve.minimalDiscriminantIdeal_ne_bot (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] : minimalDiscriminantIdeal O W ≠ 0

The minimal discriminant ideal is nonzero.

@[simp]

theorem WeierstrassCurve.count_minimalDiscriminantIdeal_eq_localMinimalDiscriminantValuation (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve K) (v : IsDedekindDomain.HeightOneSpectrum O) [W.IsElliptic] : (Associates.mk v.asIdeal).count (Associates.mk (minimalDiscriminantIdeal O W)).factors = localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W

The exponent of 𝔭ᵥ in the minimal discriminant ideal is v (Δ_min,ᵥ). This reads the local minimal exponents back off the ideal, so results about 𝔇_{E/K} can be proved without unfolding the defining product.

theorem WeierstrassCurve.minimalDiscriminantIdeal_def (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] : minimalDiscriminantIdeal O W = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum O), v.asIdeal ^ localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W

The defining prime-power factorisation of the minimal discriminant ideal. Outside this module the body of minimalDiscriminantIdeal is not exposed, so this is the interface for unfolding it.

theorem WeierstrassCurve.minimalDiscriminantIdeal_dvd_span {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] {d : O} (hd : (algebraMap O K) d = W.Δ) : minimalDiscriminantIdeal O W ∣ Ideal.span {d}

The minimal discriminant ideal divides the discriminant ideal of every integral equation. This is the global form of the primewise inequality between their exponents.

theorem WeierstrassCurve.minimalDiscriminantIdeal_eq_span_of_isGlobalMinimal {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] (h : IsGlobalMinimal O W) {d : O} (hd : (algebraMap O K) d = W.Δ) : minimalDiscriminantIdeal O W = Ideal.span {d}

A globally minimal equation computes the minimal discriminant ideal as (Δ W).

theorem WeierstrassCurve.isGlobalMinimal_iff_minimalDiscriminantIdeal_eq_span {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] {d : O} (hd : (algebraMap O K) d = W.Δ) : IsGlobalMinimal O W ↔ minimalDiscriminantIdeal O W = Ideal.span {d}

Among integral equations, 𝔇_{E/K} = (Δ W) holds exactly for the globally minimal ones. Integrality is not optional: a non-integral change of variables can fix Δ while destroying minimality.