Minimal models: a criterion, their comparison, and what transfers between them

Mathlib defines WeierstrassCurve.IsMinimal by a maximality property — the valuation of the discriminant is maximal among all integral models isomorphic to the given one — and derives minimality only from that property or from a class that already extends it. Establishing it for a given equation therefore means quantifying over every change of variables, which is not something a caller can discharge by hand.

This file supplies the cheapest sufficient condition — an integral Weierstrass equation whose c₄ is a unit at the place is already minimal — and then the comparison any two minimal models admit: they have the same discriminant valuation, so a change of variables between them has a scaling factor of valuation 1.

Main results

• WeierstrassCurve.isMinimal_of_valuation_c₄_eq_one: over the fraction field of a discrete valuation ring, an integral Weierstrass equation with v (c₄) = 1 is minimal.
• WeierstrassCurve.exists_smul_eq_minimal: Mathlib's chosen minimal equation is obtained by a change of variables.
• WeierstrassCurve.exists_smul_minimal_eq_minimal: chosen minimal equations of isomorphic equations are related by a change of variables.
• WeierstrassCurve.valuation_Δ_le_of_isMinimal_smul: no integral model in the orbit of a minimal model has larger v (Δ).
• WeierstrassCurve.valuation_Δ_eq_of_isMinimal_smul: two minimal models related by a change of variables have equal v (Δ).
• WeierstrassCurve.isMinimal_of_valuation_Δ_eq_of_isMinimal_smul: conversely, an integral model attaining that valuation is minimal.
• WeierstrassCurve.isMinimal_baseChange_smul: a change of variables defined over R carries a minimal model to a minimal model.
• WeierstrassCurve.valuation_u_eq_one_of_isMinimal_smul: for an elliptic curve, the scaling factor of such a change of variables satisfies v (u) = 1.
• WeierstrassCurve.VariableChange.exists_unit_algebraMap_eq_u_of_isMinimal_smul: the scaling factor is the image of a unit of the discrete valuation ring.
• WeierstrassCurve.valuation_Δ_minimal_smul and WeierstrassCurve.valuation_c₄_minimal_smul: the chosen minimal equations of isomorphic curves have the same discriminant and c₄ valuations.
• WeierstrassCurve.HasSplitMultiplicativeReduction.of_isMinimal_smul: split multiplicative reduction transfers along such a change of variables.

valuation_u_eq_one_of_isMinimal_smul and VariableChange.exists_unit_algebraMap_eq_u_of_isMinimal_smul supply the unit needed for descent. Turning that into a change of variables actually defined over R is the job of WeierstrassCurve.VariableChange.exists_baseChange_eq_of_smul_eq, which also consumes integrality of both models. A change of variables defined over R is one the reduction can see, and that is what carries split multiplicativity across.

Why this is the useful form

The hypothesis is stated through the adic valuation of W.c₄ : K, matching how Mathlib phrases WeierstrassCurve.HasMultiplicativeReduction, whose multiplicativeReduction field is exactly valuation K (maximalIdeal R) W.c₄ = 1. That class extends IsMinimal, so the implication is not needed to go from multiplicative reduction to minimality — it is needed in the other direction, to construct HasMultiplicativeReduction for an equation one has only computed c₄ and Δ for. That is the shape a quadratic twist arrives in: twisting by a discriminant that is a unit scales c₄ by a unit square, so the twist's c₄ valuation is again 1, and this criterion is what turns that computation into minimality of the twisted model.

Mathematical content

It is the unit-c₄ case of the Kraus–Laska criterion — the special case "v (c₄) < 4 or v (Δ) < 12 implies minimal" of Silverman, The Arithmetic of Elliptic Curves, Remark VII.1.1, restricted to v (c₄) = 0. The proof is direct: a change of variables scales c₄ by u⁻⁴ and Δ by u⁻¹², and integrality of the transformed model bounds v (u⁻⁴) by 1, hence v (u⁻¹²) ≤ 1, so no change of variables can raise the discriminant's valuation.

Provenance

⚠ mathlib-track: this is a statement about Mathlib's own IsMinimal, with no Tau Ceti definitions involved, and belongs upstream once its consumers are in place.

Ported from FLT, https://github.com/ImperialCollegeLondon/FLT @ bc2fe8ff7396469a16c2a6d51d6117f5825d93a0 (Apache-2.0), file FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean, by Kevin Buzzard — the source commit is FLT PR #1088, "Quadratic twist to split multiplicative reduction". Five declarations are taken from it:

• isMinimal_of_valuation_c₄_eq_one;
• valuation_Δ_aux_smul_le, here valuation_Δ_le_of_isMinimal_smul;
• valuation_Δ_eq_of_isMinimal_smul;
• valuation_u_eq_one_of_isMinimal_smul;
• HasSplitMultiplicativeReduction.of_isMinimal_smul.

The source declaration HasSplitMultiplicativeReduction.of_isMinimal_smul no longer exists at FLT's current head (9deae05a), which drops that development entirely; the pinned revision above is the record of it. It is absent from Mathlib too, whose IsMinimal API stops at the pairwise exclusion of the reduction types and never compares two minimal models.

Statements are taken unchanged except for of_isMinimal_smul, which drops the source's [IsMinimal R W₁]: that instance is already implied by its h₁, since HasSplitMultiplicativeReduction extends HasMultiplicativeReduction extends IsMinimal. The proofs diverge in six places:

• the section's variable block is restated here, and the opens are narrowed to those of Mathlib's own Minimal section (IsLocalRing is left closed, since opening it makes maximalIdeal ambiguous — ResidueField is written qualified instead);
• valuation_Δ_aux_smul_le is restated here as valuation_Δ_le_of_isMinimal_smul, through the ordinary valuation of two models related by a change of variables rather than through the internal valuation_Δ_aux and the orbit of one equation; valuation_Δ_eq_of_isMinimal_smul is then two applications of it, and isMinimal_of_valuation_Δ_eq_of_isMinimal_smul — its converse, which the source does not have — is a third;
• the source's exists_algebraMap_unit_eq_of_valuation_eq_one — a separate shim of its own, in FLT/Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean — is not ported. Mathlib has since acquired that file, and with it associated_of_valuation_eq, which the three lines below call directly. The source obtains the unit in the orientation u • x = 1 and then inverts it; taking associated_of_valuation_eq 1 ↑D.u instead lands on algebraMap R K u = D.u with no inversion at all;
• the source's exists_variableChange_baseChange_eq_of_smul_eq is this repository's WeierstrassCurve.VariableChange.exists_baseChange_eq_of_smul_eq, which is stated over IsIntegrallyClosedIn R K rather than a discrete valuation ring; instance search discharges it here;
• the source's nodePoly_map_splits_smul_iff is this repository's existing splits_variableChange_nodePolynomial_map_iff, and the node polynomial reaches Mathlib's class field through nodePolynomial_def, since the definition's body is not exposed across the module boundary;
• the ⁄K notation is written baseChange, and the source's show … from rfl scaffolding for it is replaced by a single congrArg.

theorem WeierstrassCurve.isMinimal_of_valuation_c₄_eq_one (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) [IsIntegral R W] (hc₄ : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ = 1) : IsMinimal R W

An integral Weierstrass equation whose c₄ is a unit at the place is minimal. No change of variables can increase the valuation of the discriminant: it scales Δ by u⁻¹² while scaling c₄ by u⁻⁴, and integrality of the transformed equation forces v (u⁻⁴) ≤ 1.

This is the unit-c₄ case of the Kraus–Laska criterion (Silverman, AEC, Remark VII.1.1). The hypothesis is phrased through the adic valuation of W.c₄ : K to match WeierstrassCurve.HasMultiplicativeReduction, so that a curve for which only c₄ has been computed can be given its IsMinimal field.

theorem WeierstrassCurve.exists_smul_eq_minimal (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) : ∃ (C : VariableChange K), C • W = minimal R W

Mathlib's chosen minimal equation lies in the variable-change orbit. The equation W.minimal R is obtained from W by a change of variables.

theorem WeierstrassCurve.exists_smul_minimal_eq_minimal (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) : ∃ (C : VariableChange K), C • minimal R W = minimal R (D • W)

The chosen minimal equations of two equations related by a change of variables are themselves related by a change of variables.

Comparing two minimal models

IsMinimal says the discriminant valuation is maximal among integral models. Two minimal models of the same curve therefore pin each other: each is at least as good as the other, so their valuations agree, and the change of variables between them can only scale Δ by a unit.

theorem WeierstrassCurve.valuation_Δ_le_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} [hm : IsMinimal R W₁] [IsIntegral R W₂] (D : VariableChange K) (hD : D • W₁ = W₂) : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W₂.Δ ≤ (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W₁.Δ

A minimal model maximises the discriminant valuation in its orbit: every integral model obtained from it by a change of variables has discriminant of at most that valuation. This is the valuation-level reading of Mathlib's IsMinimal, whose MaximalFor phrasing speaks of valuation_Δ_aux and of the orbit of a fixed equation.

theorem WeierstrassCurve.valuation_Δ_eq_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₂) : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W₂.Δ = (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W₁.Δ

Two minimal models related by a change of variables have the same discriminant valuation. So v (Δ) is an invariant of the curve at this place rather than of the chosen model: any two minimal models of the same curve agree on it, and a consumer may read it off whichever model it holds.

theorem WeierstrassCurve.isMinimal_of_valuation_Δ_eq_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₁] [IsIntegral R W₂] (D : VariableChange K) (hD : D • W₁ = W₂) (h : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W₂.Δ = (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W₁.Δ) : IsMinimal R W₂

An integral model whose discriminant valuation matches that of a minimal model in its orbit is itself minimal. Together with valuation_Δ_le_of_isMinimal_smul this makes the discriminant valuation a complete test for minimality among integral models of one curve.

theorem WeierstrassCurve.isMinimal_baseChange_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) [IsMinimal R W] (C : VariableChange R) : IsMinimal R (C.baseChange K • W)

A change of variables defined over R preserves minimality: if W is minimal over R and C is a change of variables with coefficients in R, then C • W is minimal over R. With valuation_u_eq_one_of_isMinimal_smul and VariableChange.exists_baseChange_eq_of_smul_eq in the other direction, the changes of variables between minimal models of an elliptic curve are exactly those defined over R.

theorem WeierstrassCurve.valuation_u_eq_one_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₂] [W₁.IsElliptic] (D : VariableChange K) (hD : D • W₁ = W₂) : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) ↑D.u = 1

The scaling factor of a change of variables between two minimal models of an elliptic curve has valuation 1. Over a discrete valuation ring that says u is a unit: it and its inverse are both integral, so such a change of variables is as integral as its coordinates allow. This is the hypothesis VariableChange.exists_baseChange_eq_of_smul_eq asks for, and hence the step by which a property of the reduction transfers between two minimal models of one curve.

theorem WeierstrassCurve.VariableChange.exists_unit_algebraMap_eq_u_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₂] [W₁.IsElliptic] (D : VariableChange K) (hD : D • W₁ = W₂) : ∃ (u₀ : Rˣ), (algebraMap R K) ↑u₀ = ↑D.u

The scaling factor between two minimal elliptic equations is the image of a unit of the discrete valuation ring.

@[simp]

theorem WeierstrassCurve.valuation_Δ_minimal_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) : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) (minimal R (D • W)).Δ = (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) (minimal R W).Δ

The discriminants of the chosen minimal equations have the same valuation after a change of variables.

@[simp]

theorem WeierstrassCurve.valuation_c₄_minimal_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] : (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) (minimal R (D • W)).c₄ = (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) (minimal R W).c₄

The c₄ invariants of the chosen minimal equations have the same valuation after a change of variables.

theorem WeierstrassCurve.HasSplitMultiplicativeReduction.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₂] [W₁.IsElliptic] (D : VariableChange K) (hD : D • W₁ = W₂) (h₁ : HasSplitMultiplicativeReduction R W₁) : HasSplitMultiplicativeReduction R W₂

Split multiplicative reduction is an isomorphism invariant of minimal models. If two minimal Weierstrass models of an elliptic curve over K are related by a change of variables (D • W₁ = W₂), and W₁ has split multiplicative reduction, then so does W₂.

This is what makes split multiplicative reduction a property of the curve at the place rather than of the equation presenting it. Mathlib's class is stated through a chosen integral model, so the transfer is not definitional: it needs D to be defined over R. Two results combine to give that — valuation_u_eq_one_of_isMinimal_smul supplies the unit scaling factor, and VariableChange.exists_baseChange_eq_of_smul_eq turns that unit, with integrality of both models, into the descent. A form of Silverman, The Arithmetic of Elliptic Curves, Remark VII.1.3(b), on the uniqueness of minimal models over a discrete valuation ring.