The defect ideal of an integral Weierstrass equation

Let O be a Dedekind domain with fraction field K, and let W be an integral elliptic Weierstrass equation over O. Its local obstruction exponents

fᵥ(W) = (v(Δ W) - v(Δ_min,ᵥ)) / 12

are nonnegative integers. This file assembles them into the defect ideal

𝔍_W = ∏ᵥ 𝔭ᵥ ^ fᵥ(W).

The product is finite because each exponent is bounded by the multiplicity of 𝔭ᵥ in the nonzero principal ideal generated by Δ W. Its characteristic identity is

(Δ W) = 𝔇_{E/K} · 𝔍_W ^ 12,

where 𝔇_{E/K} is the minimal discriminant ideal. Thus the defect ideal records exactly the failure of an integral equation to be globally minimal; in particular it is the unit ideal precisely for globally minimal equations.

Main definitions

• WeierstrassCurve.weierstrassDefectIdeal: the ideal ∏ᵥ 𝔭ᵥ ^ fᵥ(W).

Main results

• WeierstrassCurve.hasFiniteMulSupport_pow_obstructionExponentAt_toNat: the defining product has finite support.
• WeierstrassCurve.weierstrassDefectIdeal_ne_bot: the defect ideal is nonzero.
• WeierstrassCurve.count_weierstrassDefectIdeal_eq_obstructionExponentAt: the exponent of 𝔭ᵥ in the defect ideal is fᵥ(W).
• WeierstrassCurve.coe_weierstrassDefectIdeal_smul_mul_toPrincipalIdeal: the transformation formula for defect ideals.
• WeierstrassCurve.span_Δ_eq_minimalDiscriminantIdeal_mul_weierstrassDefectIdeal_pow_twelve: the discriminant ideal factors as 𝔇_{E/K} · 𝔍_W ^ 12.
• WeierstrassCurve.weierstrassDefectIdeal_eq_top_iff_isGlobalMinimal: the defect ideal is the unit ideal exactly when the equation is globally minimal.

References

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

theorem WeierstrassCurve.count_span_Δ_eq_localMinimalDiscriminantValuation_add_twelve_mul_obstructionExponentAt (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) = ↑(localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W) + 12 * obstructionExponentAt O v W

The exponent of 𝔭ᵥ in the discriminant ideal is the local minimal exponent plus twelve times the local obstruction exponent. This integer-valued identity holds for any elliptic equation with a global integral representative d of its discriminant; the equation itself need not be integral.

theorem WeierstrassCurve.count_span_Δ_eq_localMinimalDiscriminantValuation_add_twelve_mul_obstructionExponentAt_toNat (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 (Localization.AtPrime v.asIdeal) W] {d : O} (hd : (algebraMap O K) d = W.Δ) : (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {d})).factors = localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W + 12 * (obstructionExponentAt O v W).toNat

For an equation integral at v, the primewise discriminant-defect identity in natural exponents. Local integrality makes the obstruction exponent nonnegative, so taking toNat loses no information.

theorem WeierstrassCurve.hasFiniteMulSupport_pow_obstructionExponentAt_toNat (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] : Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum O) => v.asIdeal ^ (obstructionExponentAt O v W).toNat

Only finitely many local obstruction exponents of an integral equation are nonzero. Equivalently, the prime-power family defining the defect ideal has finite multiplicative support.

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

The defect ideal 𝔍_W = ∏ᵥ 𝔭ᵥ ^ fᵥ(W) of an integral Weierstrass equation. Integrality makes every local obstruction exponent nonnegative, so its natural-number part loses no information. The product ranges over the finite support certified by hasFiniteMulSupport_pow_obstructionExponentAt_toNat, which is how the construction consumes integrality; weierstrassDefectIdeal_def recovers the finprod over all height-one primes.

Equations

• WeierstrassCurve.weierstrassDefectIdeal O W = ∏ v ∈ Set.Finite.toFinset ⋯, v.asIdeal ^ (WeierstrassCurve.obstructionExponentAt O v W).toNat

theorem WeierstrassCurve.weierstrassDefectIdeal_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] [IsIntegral O W] : weierstrassDefectIdeal O W = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum O), v.asIdeal ^ (obstructionExponentAt O v W).toNat

The defining prime-power factorisation of the defect ideal, as a product over all height-one primes.

theorem WeierstrassCurve.weierstrassDefectIdeal_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] [IsIntegral O W] : weierstrassDefectIdeal O W ≠ 0

The defect ideal is nonzero.

@[simp]

theorem WeierstrassCurve.count_weierstrassDefectIdeal_eq_obstructionExponentAt (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] : ↑((Associates.mk v.asIdeal).count (Associates.mk (weierstrassDefectIdeal O W)).factors) = obstructionExponentAt O v W

The exponent of 𝔭ᵥ in the defect ideal is the local obstruction exponent fᵥ(W). The cast to ℤ reflects that obstructionExponentAt is defined for arbitrary rational equations, while ideal multiplicities are natural numbers.

theorem WeierstrassCurve.coe_weierstrassDefectIdeal_smul_mul_toPrincipalIdeal (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] (C : VariableChange K) [IsIntegral O W] [IsIntegral O (C • W)] : ↑(weierstrassDefectIdeal O (C • W)) * ↑((toPrincipalIdeal O K) C.u) = ↑(weierstrassDefectIdeal O W)

The defect ideals of two integral equations related by C differ by the principal fractional ideal generated by C.u: 𝔍_(C • W) · (C.u) = 𝔍_W.

Primewise, this is the change-of-variables identity f_v(C • W) + ord_v(C.u) = f_v(W). The equation is stated in fractional ideals because C.u need not lie in O.

theorem WeierstrassCurve.span_Δ_eq_minimalDiscriminantIdeal_mul_weierstrassDefectIdeal_pow_twelve {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.Δ) : Ideal.span {d} = minimalDiscriminantIdeal O W * weierstrassDefectIdeal O W ^ 12

The discriminant ideal of an integral equation is its minimal discriminant ideal times the twelfth power of its defect ideal: (Δ W) = 𝔇_{E/K} · 𝔍_W ^ 12.

@[simp]

theorem WeierstrassCurve.weierstrassDefectIdeal_eq_top_iff_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] [IsIntegral O W] : weierstrassDefectIdeal O W = ⊤ ↔ IsGlobalMinimal O W

An integral equation has trivial defect ideal exactly when it is globally minimal.