Changes of variables between integral models

A change of variables D : VariableChange K carrying one integral Weierstrass model to another need not be integral itself: its scaling factor D.u is a unit of K, and D.r, D.s, D.t are elements of K. This file shows that when R is integrally closed in K, as soon as D.u lies in R so do D.r, D.s and D.t, and hence that when D.u comes from a unit of R, D is the base change of a VariableChange R. Three further facts about integral models sit beside it: over a domain with fraction field K every equation has an integral model, obtained by clearing a common denominator of the coefficients; a change of variables whose u⁻¹, r, s and t lie in R preserves integrality; and integrality is inherited by a larger ring of a tower.

Main results

• WeierstrassCurve.VariableChange.isInteger_r_s_t_of_smul_eq: for R integrally closed in K, if D • W₁ = W₂ with W₁ and W₂ integral over R and D.u ∈ R, then D.r, D.s and D.t lie in R (Silverman VII.1.3(d)).
• WeierstrassCurve.VariableChange.exists_baseChange_eq_of_smul_eq: for R integrally closed in K (IsIntegrallyClosedIn R K), if D • W₁ = W₂ with W₁ and W₂ integral over R and D.u the image of a unit of R, then D = C₀.baseChange K for some C₀ : VariableChange R.
• WeierstrassCurve.exists_smul_isIntegral: every equation over K has an integral model over a ring R with fraction field K.
• WeierstrassCurve.isIntegral_smul_of_exists_lift: a change of variables whose u⁻¹, r, s and t lie in R preserves integrality.
• WeierstrassCurve.IsIntegral.of_isScalarTower: integrality passes to a larger ring of the tower.

The integral-closedness hypothesis is what the proof actually consumes. A discrete valuation ring with its fraction field is the intended application and satisfies it through isIntegrallyClosed_iff_isIntegrallyClosedIn, but no valuation is used anywhere below.

How it is proved

Each of r, s, t is exhibited as a root of an explicit monic polynomial over R, built from the change-of-variables formulas for the invariants, and R is integrally closed:

• r from the b₆- and b₈-relations, as a root of a quartic. The two are combined as b₈-relation − r · b₆-relation: that cancels the r³ · b₂ terms and turns 3r⁴ − 4r⁴ into −r⁴, leaving b₈ + 2r · b₆ + r² · b₄ − r⁴. The r⁴ term does not cancel and must not — it is the quartic's leading term;
• s from the a₂-relation, as a root of a quadratic, once r is known to lie in R;
• t from the a₆-relation, likewise a quadratic, once r is known.

The three arguments are separate private lemmas rather than one proof: each is a distinct integrality certificate with its own polynomial, and taken together they are past the repository's hard cap on proof length. s and t take the integral representative of r as a hypothesis, which is why they are stated after it rather than beside it.

Why this is not in EllipticCurve/VariableChange.lean

That file is where this repository keeps its VariableChange API, and the statement below is about VariableChange.baseChange, so it would sit there naturally — except that the proof needs WeierstrassCurve.IsIntegral and integralModel, i.e. Mathlib's EllipticCurve.Reduction with its valuation machinery. VariableChange.lean currently imports only Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange, and three modules import it; putting the descent there would push the reduction cone onto all of them. The topic here is integral models, so the file is named for them.

Provenance

⚠ mathlib-track. Statements about Mathlib's own IsIntegral for Weierstrass models and VariableChange.baseChange, with no Tau Ceti definitions involved.

The descent is ported from FLT, https://github.com/ImperialCollegeLondon/FLT @ bc2fe8ff7396469a16c2a6d51d6117f5825d93a0 (Apache-2.0), file FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean, declaration WeierstrassCurve.exists_variableChange_baseChange_eq_of_smul_eq, by Kevin Buzzard; exists_smul_isIntegral, isIntegral_smul_of_exists_lift and IsIntegral.of_isScalarTower are not from that source. The source commit is FLT PR #1088, "Quadratic twist to split multiplicative reduction". The mathematics is unchanged: the same three polynomials, the same linear_combination certificates. The single 66-line proof is split into the three integrality arguments plus their assembly, so that no declaration exceeds the length cap. Three hypotheses are weakened relative to the source, which states the descent for a discrete valuation ring and a unit scaling factor: the integrality certificates need only Algebra R K and a scaling factor in R, and the assembly needs only IsIntegrallyClosedIn R K.

The three integrality certificates

These need nothing of R beyond its algebra structure on K: each exhibits a monic polynomial over R killing the coordinate. Integral closedness enters only in the assembly below, which is where the roots are pulled back into R.

Assembly

Pulling the three roots back into R is exactly IsIntegrallyClosedIn R K, and that is the only hypothesis this section adds. A discrete valuation ring together with its fraction field is the intended way to obtain it — see isIntegrallyClosed_iff_isIntegrallyClosedIn — but nothing here requires a valuation, and K need not be a fraction field.

theorem WeierstrassCurve.VariableChange.isInteger_r_s_t_of_smul_eq (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsIntegrallyClosedIn R K] {W₁ W₂ : WeierstrassCurve K} [IsIntegral R W₁] [IsIntegral R W₂] (D : VariableChange K) (hD : D • W₁ = W₂) (u₀ : R) (hau : (algebraMap R K) u₀ = ↑D.u) : IsLocalization.IsInteger R D.r ∧ IsLocalization.IsInteger R D.s ∧ IsLocalization.IsInteger R D.t

A change of variables between two integral models has integral translation parameters as soon as its scaling factor lies in R (Silverman, AEC, Proposition VII.1.3(d)). R is assumed integrally closed in K, W₁ and W₂ integral over R, and D.u the image of u₀ : R, which need not be a unit: this is the case of a change of variables carrying an integral model to a minimal one, whose scaling factor has the valuation of the obstruction to minimality.

theorem WeierstrassCurve.VariableChange.exists_baseChange_eq_of_smul_eq (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsIntegrallyClosedIn R K] {W₁ W₂ : WeierstrassCurve K} [IsIntegral R W₁] [IsIntegral R W₂] (D : VariableChange K) (hD : D • W₁ = W₂) (u₀ : Rˣ) (hau : (algebraMap R K) ↑u₀ = ↑D.u) : ∃ (C₀ : VariableChange R), C₀.baseChange K = D

A change of variables between two integral models whose scaling factor is a unit of R is the base change of a change of variables over R. R is assumed integrally closed in K; W₁ and W₂ integral over R; and D.u the image of u₀ : Rˣ. The witness has that same u₀ as its scaling factor.

theorem WeierstrassCurve.exists_smul_isIntegral (R : Type u_1) [CommRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : ∃ (C : VariableChange K), IsIntegral R (C • W)

Every Weierstrass equation over the fraction field of a ring R has an integral model over R. This supplies an integral equation for arguments that compare field-valued curve invariants with ideals of the base ring.

theorem WeierstrassCurve.isIntegral_smul_of_exists_lift {R : Type u_1} [CommRing R] {K : Type u_2} [Field K] [Algebra R K] {W : WeierstrassCurve K} [IsIntegral R W] {C : VariableChange K} (hu : ∃ (u : R), (algebraMap R K) u = ↑C.u⁻¹) (hr : ∃ (r : R), (algebraMap R K) r = C.r) (hs : ∃ (s : R), (algebraMap R K) s = C.s) (ht : ∃ (t : R), (algebraMap R K) t = C.t) : IsIntegral R (C • W)

A change of variables whose u⁻¹, r, s and t lie in R preserves integrality. The scaling factor C.u itself need not lie in R, so C need not be the base change of a VariableChange R: scaling by the inverse of a nonunit π of R multiplies aᵢ by πⁱ and the discriminant by π ^ 12, keeping an integral equation integral but not minimal.

theorem WeierstrassCurve.IsIntegral.of_isScalarTower {R : Type u_1} {S : Type u_2} {K : Type u_3} [CommRing R] [CommRing S] [Field K] [Algebra R K] [Algebra R S] [Algebra S K] [IsScalarTower R S K] (W : WeierstrassCurve K) [IsIntegral R W] : IsIntegral S W

An integral model stays integral over a larger ring of the tower. If W has coefficients in R and R maps to S compatibly with their maps to K, then W has coefficients in S. In particular, global integrality over a Dedekind domain gives integrality at each localisation.