Global and semi-global minimal Weierstrass equations over a Dedekind domain

Mathlib's WeierstrassCurve.IsMinimal R W minimises a Weierstrass equation over one discrete valuation ring R at a time. Over the fraction field K of a Dedekind domain O — a number field and its ring of integers being the case that matters — the local rings are the localisations Oᵥ := Localization.AtPrime v.asIdeal at the height-one primes v of O, and a globally minimal equation is one that is minimal at every v simultaneously (Silverman, The Arithmetic of Elliptic Curves, VIII.8). This file defines that predicate and its semi-global relaxation, proves that a globally minimal equation has coefficients in O, and describes the changes of variables between globally minimal equations: they are exactly those defined over O.

Main definitions

• WeierstrassCurve.IsGlobalMinimal O W: W is minimal over Oᵥ for every height-one prime v of O.
• WeierstrassCurve.IsSemiGlobalMinimal O W: W is globally minimal, or there is one height-one prime v₀ at which W is merely integral while it is minimal at every other height-one prime.

Main results

• WeierstrassCurve.isIntegral_of_forall_isIntegral_localizationAtPrime: an equation integral over every Oᵥ is integral over O. This is O = ⋂ᵥ Oᵥ (IsDedekindDomain.HeightOneSpectrum.isInteger_of_forall_isInteger_localizationAtPrime) applied to each coefficient.
• WeierstrassCurve.IsGlobalMinimal.isIntegral and WeierstrassCurve.IsSemiGlobalMinimal.isIntegral: both predicates imply integrality over O, through Mathlib's [IsMinimal R W] : IsIntegral R W at each prime and the descent.
• WeierstrassCurve.IsGlobalMinimal.baseChange_smul: a change of variables defined over O carries a globally minimal equation to a globally minimal equation.
• WeierstrassCurve.IsGlobalMinimal.exists_baseChange_eq_of_smul_eq: conversely, a change of variables between two globally minimal equations of an elliptic curve is defined over O, its scaling factor being a unit of O (Silverman, AEC, VIII.8).

The predicates are unexposed. Their interface is the simp lemmas isGlobalMinimal_iff and isSemiGlobalMinimal_iff together with the introduction and elimination lemmas IsGlobalMinimal.isMinimal, IsGlobalMinimal.of_forall_isMinimal, IsGlobalMinimal.isSemiGlobalMinimal and IsSemiGlobalMinimal.of_isIntegral_of_isMinimal.

Design

• Integrality over O is a theorem, not a conjunct. Mathlib's instance gives integrality over each Oᵥ only, so inferInstance does not reach IsIntegral O W, and adding it as a hypothesis to the definition would hide the descent.
• The semi-global predicate is a disjunction. A field is a Dedekind domain whose height-one spectrum is empty; there IsGlobalMinimal is vacuously true while the bare existential ∃ v₀, … is false. The disjunct is what makes IsGlobalMinimal.isSemiGlobalMinimal hold at that degenerate base. The integrality clause at v₀ cannot be dropped either: minimality away from v₀ says nothing about the denominators at v₀.
• Both predicates carry [W.IsElliptic]. Minimal models are a notion for elliptic curves: the invariants built on these predicates — the minimal discriminant ideal, the obstruction exponents, semistability — need Δ ≠ 0, and for a singular cubic the products defining them lose their finite support. IsGlobalMinimal does not itself consume the instance, which its binder name records. The localisation instances that make IsMinimal Oᵥ W and IsIntegral Oᵥ W typecheck for an abstract fraction field K are in TauCeti/RingTheory/Localization/AtPrime.lean and TauCeti/RingTheory/DedekindDomain/LocalizationAtPrime.lean.

Provenance

The two definitions are adapted from LeanBridge (github.com/CBirkbeck/LeanBridge, Apache-2.0), file LeanBridge/ForMathlib/4-EC.lean at JaneShi99/LeanBridge@d84dd305 (branch formalize/ec-defs), by Jane Shi, where they formalise the LMFDB knowls ec.global_minimal_model and ec.semi_global_minimal_model. Two departures: the semi-global predicate acquires the IsGlobalMinimal disjunct, and both predicates carry [W.IsElliptic]. The descent theorem is proved afresh here; LeanBridge records only that it had been proved and then removed.

def WeierstrassCurve.IsGlobalMinimal (O : Type u_1) [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] (W : WeierstrassCurve K) [_hE : W.IsElliptic] : Prop

A globally minimal Weierstrass equation (LMFDB ec.global_minimal_model): W is minimal over the discrete valuation ring Localization.AtPrime v.asIdeal at every height-one prime v of O. Integrality over O is not assumed; it is the theorem IsGlobalMinimal.isIntegral. The ellipticity instance keeps the predicate to elliptic curves, the setting in which the invariants derived from it make sense; the definition itself does not consume it, which its binder name records.

Equations

• WeierstrassCurve.IsGlobalMinimal O W = ∀ (v : IsDedekindDomain.HeightOneSpectrum O), WeierstrassCurve.IsMinimal (Localization.AtPrime v.asIdeal) W

@[simp]

theorem WeierstrassCurve.isGlobalMinimal_iff {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] : IsGlobalMinimal O W ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum O), IsMinimal (Localization.AtPrime v.asIdeal) W

Global minimality is minimality at every height-one prime. This is the interface to WeierstrassCurve.IsGlobalMinimal outside its defining module.

theorem WeierstrassCurve.IsGlobalMinimal.isMinimal {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) (v : IsDedekindDomain.HeightOneSpectrum O) : IsMinimal (Localization.AtPrime v.asIdeal) W

A globally minimal equation is minimal at each height-one prime.

theorem WeierstrassCurve.IsGlobalMinimal.of_forall_isMinimal {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 : ∀ (v : IsDedekindDomain.HeightOneSpectrum O), IsMinimal (Localization.AtPrime v.asIdeal) W) : IsGlobalMinimal O W

An equation minimal at every height-one prime is globally minimal.

def WeierstrassCurve.IsSemiGlobalMinimal (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] : Prop

A semi-globally minimal Weierstrass equation (LMFDB ec.semi_global_minimal_model): either W is globally minimal, or there is a height-one prime v₀ of O at which W is integral and away from which it is minimal. Over a number field of class number greater than one a curve need not admit a globally minimal equation, but it always admits a semi-globally minimal one; that existence theorem is not proved here. The disjunct is load-bearing: over a field, whose height-one spectrum is empty, the existential alone is false while global minimality holds.

Equations

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

@[simp]

theorem WeierstrassCurve.isSemiGlobalMinimal_iff {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] : IsSemiGlobalMinimal O W ↔ IsGlobalMinimal O W ∨ ∃ (v₀ : IsDedekindDomain.HeightOneSpectrum O), IsIntegral (Localization.AtPrime v₀.asIdeal) W ∧ ∀ (v : IsDedekindDomain.HeightOneSpectrum O), v ≠ v₀ → IsMinimal (Localization.AtPrime v.asIdeal) W

Semi-global minimality, unfolded. This is the interface to WeierstrassCurve.IsSemiGlobalMinimal outside its defining module.

theorem WeierstrassCurve.IsGlobalMinimal.isSemiGlobalMinimal {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) : IsSemiGlobalMinimal O W

A globally minimal equation is semi-globally minimal, at every base including a field.

theorem WeierstrassCurve.IsSemiGlobalMinimal.of_isIntegral_of_isMinimal {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] {v₀ : IsDedekindDomain.HeightOneSpectrum O} (h₀ : IsIntegral (Localization.AtPrime v₀.asIdeal) W) (h : ∀ (v : IsDedekindDomain.HeightOneSpectrum O), v ≠ v₀ → IsMinimal (Localization.AtPrime v.asIdeal) W) : IsSemiGlobalMinimal O W

An equation integral at a height-one prime v₀ and minimal at every other height-one prime is semi-globally minimal.

Descent of integrality from the localisations to O

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

A Weierstrass equation integral over every localisation of O at a height-one prime is integral over O: O = ⋂ᵥ Oᵥ, applied to the coefficients. This is how integrality over O is obtained from local data, as in IsGlobalMinimal.isIntegral.

theorem WeierstrassCurve.IsGlobalMinimal.isIntegral {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) : IsIntegral O W

A globally minimal equation is integral over O. Integrality is thus a consequence of IsGlobalMinimal, not a hypothesis of it, and integralModel O W is available for such W.

theorem WeierstrassCurve.IsSemiGlobalMinimal.isIntegral {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 : IsSemiGlobalMinimal O W) : IsIntegral O W

A semi-globally minimal equation is integral over O, so integralModel O W is available for such W just as for a globally minimal one.

Changes of variables between globally minimal equations

theorem WeierstrassCurve.IsGlobalMinimal.baseChange_smul {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) (C : VariableChange O) : IsGlobalMinimal O (C.baseChange K • W)

A change of variables defined over O preserves global minimality.

theorem WeierstrassCurve.IsGlobalMinimal.exists_baseChange_eq_of_smul_eq {O : Type u_1} [CommRing O] [IsDedekindDomain O] {K : Type u_2} [Field K] [Algebra O K] [IsFractionRing O K] {W₁ W₂ : WeierstrassCurve K} [W₁.IsElliptic] [W₂.IsElliptic] (h₁ : IsGlobalMinimal O W₁) (h₂ : IsGlobalMinimal O W₂) (D : VariableChange K) (hD : D • W₁ = W₂) : ∃ (C₀ : VariableChange O), C₀.baseChange K = D

A change of variables between two globally minimal equations of an elliptic curve is defined over O (Silverman, AEC, VIII.8). Together with IsGlobalMinimal.baseChange_smul, this characterises the changes of variables between globally minimal equations.