Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.MinimalModel.Valuation

The valuation of the local minimal discriminant #

Let R be a discrete valuation ring with fraction field K, and let W be an elliptic Weierstrass curve over K. The local minimal discriminant ideal is a nonzero power of the maximal ideal of R. This file defines its exponent as WeierstrassCurve.localMinimalDiscriminantValuation and identifies it with the additive valuation of the discriminant of any minimal equation in the variable-change orbit of W.

The exponent is the local quantity usually written v(Delta_min). It is the input used when local minimal discriminants are assembled into the minimal discriminant ideal over a Dedekind domain, and it is the baseline from which the obstruction exponent of an arbitrary integral equation is measured.

Main definitions #

Main results #

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

source
noncomputable def WeierstrassCurve.localMinimalDiscriminantValuation (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] :
ℕ

The valuation of the local minimal discriminant. This is the exponent of the maximal ideal of R in W.localMinimalDiscriminant R, equivalently the additive valuation of the discriminant of a minimal integral equation in the variable-change orbit of W.

The ellipticity hypothesis ensures that this discriminant is nonzero, so the extended-natural additive valuation is finite and has an honest natural-number value.

Equations
Instances For
    source
    theorem WeierstrassCurve.localMinimalDiscriminantValuation_eq_addVal (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] :
    ↑(localMinimalDiscriminantValuation R W) = (IsDiscreteValuationRing.addVal R) (integralModel R (minimal R W)).Δ

    The chosen minimal equation computes the local minimal discriminant valuation. The cast to ℕ∞ records explicitly that the additive valuation is finite.

    source
    theorem WeierstrassCurve.localMinimalDiscriminantValuation_eq_addVal_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 : WeierstrassCurve K) [W.IsElliptic] {W' : WeierstrassCurve K} [IsMinimal R W'] (D : VariableChange K) (hD : D • W = W') :
    ↑(localMinimalDiscriminantValuation R W) = (IsDiscreteValuationRing.addVal R) (integralModel R W').Δ

    Any minimal equation in the variable-change orbit computes the local minimal discriminant valuation. Thus the number does not depend on Mathlib's chosen minimal equation.

    source
    theorem WeierstrassCurve.valuation_Δ_eq_exp_neg_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 : WeierstrassCurve K) [W.IsElliptic] {W' : WeierstrassCurve K} [IsMinimal R W'] (D : VariableChange K) (hD : D • W = W') :
    (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W'.Δ = WithZero.exp (-↑(localMinimalDiscriminantValuation R W))

    A minimal model has discriminant of valuation exp (-v (Δ_min)). This reads the local minimal discriminant valuation off the multiplicative valuation that Mathlib's minimality API is phrased in, and is the form in which the exponent is compared with the v-adic factorisation of a discriminant over a Dedekind domain.

    source
    theorem WeierstrassCurve.localMinimalDiscriminant_eq_maximalIdeal_pow (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 = IsLocalRing.maximalIdeal R ^ localMinimalDiscriminantValuation R W

    The local minimal discriminant is the indicated power of the maximal ideal. This characterizes localMinimalDiscriminantValuation intrinsically at the ideal level and is the form used to assemble local factors over a Dedekind domain.

    source
    @[simp]
    theorem WeierstrassCurve.localMinimalDiscriminantValuation_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) [W.IsElliptic] :
    localMinimalDiscriminantValuation R (D • W) = localMinimalDiscriminantValuation R W

    The local minimal discriminant valuation is invariant under a change of variables.

    source
    @[simp]
    theorem WeierstrassCurve.localMinimalDiscriminantValuation_eq_zero_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) [W.IsElliptic] :
    localMinimalDiscriminantValuation R W = 0 ↔ HasGoodReduction R (minimal R W)

    The local minimal discriminant valuation vanishes exactly at good reduction.

    source
    @[simp]
    theorem WeierstrassCurve.localMinimalDiscriminantValuation_pos_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) [W.IsElliptic] :
    0 < localMinimalDiscriminantValuation R W ↔ ¬HasGoodReduction R (minimal R W)

    The local minimal discriminant valuation is positive exactly at bad reduction.

    source
    theorem WeierstrassCurve.ord_Δ_eq_localMinimalDiscriminantValuation (O : Type u_3) [CommRing O] [IsDedekindDomain O] {K : Type u_4} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] {W' : WeierstrassCurve K} [IsMinimal (Localization.AtPrime v.asIdeal) W'] (D : VariableChange K) (hD : D • W = W') :
    (IsDedekindDomain.HeightOneSpectrum.valuation K v).ord W'.Δ = ↑(localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W)

    A minimal equation computes the local minimal discriminant valuation in additive notation.

    source
    theorem WeierstrassCurve.localMinimalDiscriminantValuation_le_ord_Δ (O : Type u_3) [CommRing O] [IsDedekindDomain O] {K : Type u_4} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] [IsIntegral (Localization.AtPrime v.asIdeal) W] :
    ↑(localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W) ≤ (IsDedekindDomain.HeightOneSpectrum.valuation K v).ord W.Δ

    The local minimal discriminant valuation bounds the order of the discriminant of every integral equation.

    source
    theorem WeierstrassCurve.ord_Δ_eq_localMinimalDiscriminantValuation_iff_isMinimal (O : Type u_3) [CommRing O] [IsDedekindDomain O] {K : Type u_4} [Field K] [Algebra O K] [IsFractionRing O K] (v : IsDedekindDomain.HeightOneSpectrum O) (W : WeierstrassCurve K) [W.IsElliptic] [IsIntegral (Localization.AtPrime v.asIdeal) W] :
    (IsDedekindDomain.HeightOneSpectrum.valuation K v).ord W.Δ = ↑(localMinimalDiscriminantValuation (Localization.AtPrime v.asIdeal) W) ↔ IsMinimal (Localization.AtPrime v.asIdeal) W

    An integral equation attains the local minimal discriminant valuation exactly when it is minimal.