The local minimal discriminant ideal

Let R be a discrete valuation ring with fraction field K. The discriminant of an integral minimal Weierstrass equation over K belongs to R, and the principal ideal it generates is independent of the chosen minimal equation. This file packages that ideal as WeierstrassCurve.localMinimalDiscriminant.

Mathlib's WeierstrassCurve.minimal chooses one minimal equation in the variable-change orbit. The definition uses that choice, while localMinimalDiscriminant_eq_span_Δ is the choice-free interface: any integral minimal equation in the same orbit generates the same ideal. The reason is that two minimal equations have equal discriminant valuation; over a discrete valuation ring their discriminants therefore differ by a unit. In particular the ideal is invariant under every change of variables of the original equation.

This is the local invariant whose products over the height-one primes form the minimal discriminant ideal over a Dedekind domain. For an elliptic curve it is nonzero. The later global comparison with an arbitrary integral equation additionally records the excess valuation in multiples of twelve; no obstruction exponent is defined here.

Main definitions

• WeierstrassCurve.localMinimalDiscriminant: the principal ideal generated by the discriminant of a local minimal equation.

Main results

• WeierstrassCurve.associated_integralModel_Δ_of_isMinimal_smul: minimal equations in the same variable-change orbit have associated integral discriminants.
• WeierstrassCurve.localMinimalDiscriminant_eq_span_Δ: any such minimal equation computes the local minimal discriminant.
• WeierstrassCurve.localMinimalDiscriminant_smul: the ideal is invariant under a change of variables.
• WeierstrassCurve.localMinimalDiscriminant_ne_bot: an elliptic curve has nonzero local minimal discriminant.
• WeierstrassCurve.localMinimalDiscriminant_eq_top_iff: the ideal is trivial exactly at good reduction.

The mathematics is Silverman, The Arithmetic of Elliptic Curves, VII.1.

noncomputable def WeierstrassCurve.localMinimalDiscriminant (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) : Ideal R

The local minimal discriminant ideal. It is the principal ideal of R generated by the discriminant of a minimal integral equation in the variable-change orbit of W.

The definition uses Mathlib's chosen W.minimal R; use localMinimalDiscriminant_eq_span_Δ to compute it from any minimal equation in the same orbit.

Equations

• WeierstrassCurve.localMinimalDiscriminant R W = Ideal.span {(WeierstrassCurve.integralModel R (WeierstrassCurve.minimal R W)).Δ}

theorem WeierstrassCurve.associated_integralModel_Δ_of_isMinimal_smul (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W₁ W₂ : WeierstrassCurve K} [IsMinimal R W₁] [IsMinimal R W₂] (D : VariableChange K) (hD : D • W₁ = W₂) : Associated (integralModel R W₁).Δ (integralModel R W₂).Δ

Minimal equations in one variable-change orbit have associated integral discriminants. Their discriminants have the same valuation in K; equality of valuations in a discrete valuation ring says exactly that their lifts to R differ by a unit.

theorem WeierstrassCurve.localMinimalDiscriminant_eq_span_Δ (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) {W' : WeierstrassCurve K} [IsMinimal R W'] (D : VariableChange K) (hD : D • W = W') : localMinimalDiscriminant R W = Ideal.span {(integralModel R W').Δ}

Every minimal equation in the orbit computes the local minimal discriminant. If W' is minimal and D carries W to W', then the chosen minimal equation and W' have associated integral discriminants, hence generate the same ideal of R.

@[simp]

theorem WeierstrassCurve.localMinimalDiscriminant_smul (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (D : VariableChange K) (W : WeierstrassCurve K) : localMinimalDiscriminant R (D • W) = localMinimalDiscriminant R W

The local minimal discriminant is invariant under a change of variables. It depends on the curve presented by a Weierstrass equation, not on that presentation.

theorem WeierstrassCurve.localMinimalDiscriminant_ne_bot (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) [W.IsElliptic] : localMinimalDiscriminant R W ≠ ⊥

An elliptic curve has nonzero local minimal discriminant. Its chosen minimal equation is again elliptic, so its discriminant, and therefore its lift to R, is nonzero.

theorem WeierstrassCurve.localMinimalDiscriminant_eq_top_iff (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) : localMinimalDiscriminant R W = ⊤ ↔ HasGoodReduction R (minimal R W)

The local minimal discriminant is the unit ideal exactly at good reduction. This reads good reduction from the curve-level ideal rather than from a chosen minimal equation.