Changes of variables and the coordinate functions of a Weierstrass curve

Let W be a Weierstrass curve over a commutative ring R, and let x and y be the coordinate functions of its affine coordinate ring R[W] = R[X, Y] ⧸ (W(X, Y)). The pair (x, y) satisfies the Weierstrass equation of W, and of no other Weierstrass curve over R. This file is about the pairs of the shape (αx + β, γy + δx + ε), with coefficients in R, that satisfy the Weierstrass equation of a second curve W' over R. For a change of variables C = (u, r, s, t) the pair (u²x + r, u³y + u²sx + t) does so exactly when C • W' = W, by the transformation law WeierstrassCurve.Affine.baseChange_variableChange_equation. Conversely, if (αx + β, γy + δx + ε) satisfies the equation of W' then γ² = α³, and if moreover α is a unit then the pair is (u²x + r, u³y + u²sx + t) for a change of variables C with C • W' = W. No hypothesis on W, on W' or on R is needed.

The coordinate ring is free over R on the monomials xⁱ and xⁱy (WeierstrassCurve.Affine.CoordinateRing.basisMonomials). Once y² is eliminated by the equation of W, the equation of W' at such a pair is an R-linear relation among the six monomials 1, x, x², x³, y and xy, so its six coefficients vanish. For the pair (x, y) the coefficient of x³ is zero and the other five are, up to sign, the differences of the coefficients of the two curves. For the pair (αx + β, γy + δx + ε) the coefficient of x³ is γ² - α³. When α is a unit, u = γ / α is then a unit with u² = α and u³ = γ, which puts the pair in the shape (u²x + r, u³y + u²sx + t), and that case is reduced to the pair (x, y) by the transformation law WeierstrassCurve.Affine.baseChange_variableChange_equation.

The first statement makes the substitution (x', y') ↦ (u²x + r, u³y + u²sx + t) a homomorphism R[W'] → R[W] whenever C • W' = W, and the substitution of C⁻¹ inverts it: a change of variables identifies the coordinate rings, and changes of variables compose as these isomorphisms do. The second statement is the converse: a homomorphism R[W'] → R[W] of this shape, with α a unit, comes from a change of variables.

Main definitions

• WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv: the isomorphism R[W'] ≃ₐ[R] R[W] of a change of variables C with C • W' = W.

Main results

• WeierstrassCurve.Affine.CoordinateRing.equation_X_root_iff: the pair (x, y) satisfies the equation of V over R[W] exactly when V = W.
• WeierstrassCurve.Affine.CoordinateRing.sq_eq_pow_three_of_equation: if the pair (αx + β, γy + δx + ε) satisfies the equation of W' over R[W], then γ² = α³.
• WeierstrassCurve.Affine.CoordinateRing.exists_variableChange_of_equation: if moreover α is a unit, there is a change of variables C with C • W' = W, u² = α, u³ = γ, r = β, u²s = δ and t = ε.
• WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_trans and WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_one: the isomorphisms compose as the changes of variables multiply.
• WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_inj: a change of variables is determined by its isomorphism of coordinate rings.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.1 (the change of variables) and the proof of III.3.1(b).
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.2.

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, directory projects/ModularCurves/ModularCurves/EllipticCurve. The results come from exists_variableChange_of_filtration in ComparisonCoefficients.lean and its private helpers six_ext and exists_unit_sq_cube. That theorem takes an isomorphism R[W'] ≃ₐ[R] R[W] preserving a filtration of the coordinate rings by spans of monomials, extracts α, β, γ, δ, ε from it with α and γ units, and treats the zero ring separately. Here no isomorphism and no filtration appear: the hypothesis is the equation satisfied by the pair (αx + β, γy + δx + ε), only α is assumed to be a unit, and there is no case distinction on R. What is kept is the comparison of the coefficients of 1, x, x², x³, y and xy after eliminating y² (the source's six_ext, which is proved there for a nontrivial ring from Mathlib's basis {1, y} over R[X] and is deduced here from the monomial basis), and the unit u = γ / α (exists_unit_sq_cube). The source then solves the five other coefficient equations for the coefficients of C • W'; here only the coefficient of x³ of that relation is used, and C • W' = W follows from the transformation law WeierstrassCurve.Affine.baseChange_variableChange_equation and from equation_X_root_iff, in which the other five coefficients are compared for the pair (x, y) only. The equation satisfied by the pair (x, y), equation_X_root, is used in the source as coordY_mul_coordY (PoleFiltration.lean), a formula for y². equation_X_root_iff is not in the source, and neither is variableChangeEquiv with its lemmas.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.equation_X_root_iff {R : Type u_1} [CommRing R] {W V : WeierstrassCurve R} : (toAffine (baseChange V W.toAffine.CoordinateRing)).Equation ((AdjoinRoot.of W.toAffine.polynomial) Polynomial.X) (AdjoinRoot.root W.toAffine.polynomial) ↔ V = W

A Weierstrass curve is determined by the coordinate functions of its coordinate ring. For Weierstrass curves W and V over R, the pair (x, y) of coordinate functions of R[W] satisfies the Weierstrass equation of the base change of V to R[W] if and only if V = W.

theorem WeierstrassCurve.Affine.CoordinateRing.sq_eq_pow_three_of_equation {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} {α β γ δ ε : R} (h : (toAffine (baseChange W' W.toAffine.CoordinateRing)).Equation ((algebraMap R W.toAffine.CoordinateRing) α * (AdjoinRoot.of W.toAffine.polynomial) Polynomial.X + (algebraMap R W.toAffine.CoordinateRing) β) ((algebraMap R W.toAffine.CoordinateRing) γ * AdjoinRoot.root W.toAffine.polynomial + (algebraMap R W.toAffine.CoordinateRing) δ * (AdjoinRoot.of W.toAffine.polynomial) Polynomial.X + (algebraMap R W.toAffine.CoordinateRing) ε)) : γ ^ 2 = α ^ 3

If a pair (αx + β, γy + δx + ε) of elements of the coordinate ring R[W], with α, β, γ, δ and ε in R, satisfies the Weierstrass equation of the base change of W' to R[W], then γ² = α³.

theorem WeierstrassCurve.Affine.CoordinateRing.exists_variableChange_of_equation {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} {α β γ δ ε : R} (hα : IsUnit α) (h : (toAffine (baseChange W' W.toAffine.CoordinateRing)).Equation ((algebraMap R W.toAffine.CoordinateRing) α * (AdjoinRoot.of W.toAffine.polynomial) Polynomial.X + (algebraMap R W.toAffine.CoordinateRing) β) ((algebraMap R W.toAffine.CoordinateRing) γ * AdjoinRoot.root W.toAffine.polynomial + (algebraMap R W.toAffine.CoordinateRing) δ * (AdjoinRoot.of W.toAffine.polynomial) Polynomial.X + (algebraMap R W.toAffine.CoordinateRing) ε)) : ∃ (C : VariableChange R), C • W' = W ∧ ↑C.u ^ 2 = α ∧ ↑C.u ^ 3 = γ ∧ C.r = β ∧ ↑C.u ^ 2 * C.s = δ ∧ C.t = ε

A solution of Weierstrass shape over the coordinate ring comes from a change of variables. If a pair (αx + β, γy + δx + ε) of elements of the coordinate ring R[W], with α, β, γ, δ and ε in R and α a unit, satisfies the Weierstrass equation of the base change of W' to R[W], then there is a change of variables C = (u, r, s, t) over R with C • W' = W, u² = α, u³ = γ, r = β, u²s = δ and t = ε; that is, the pair is (u²x + r, u³y + u²sx + t).

The isomorphism of coordinate rings induced by a change of variables

noncomputable def WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} (C : VariableChange R) (h : C • W' = W) : W'.toAffine.CoordinateRing ≃ₐ[R] W.toAffine.CoordinateRing

The isomorphism of coordinate rings induced by a change of variables. If C • W' = W, the coordinate functions x' and y' of W' are sent to u²x + r and u³y + u²sx + t, where x and y are those of W; on points, this is the substitution (x, y) ↦ (u²x + r, u³y + u²sx + t) carrying the points of W to those of W'. The inverse is the isomorphism of C⁻¹.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_of_X {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} (C : VariableChange R) (h : C • W' = W) : (variableChangeEquiv C h) ((AdjoinRoot.of W'.toAffine.polynomial) Polynomial.X) = (algebraMap R W.toAffine.CoordinateRing) ↑C.u ^ 2 * (AdjoinRoot.of W.toAffine.polynomial) Polynomial.X + (algebraMap R W.toAffine.CoordinateRing) C.r

The isomorphism of a change of variables sends x' to u²x + r.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_root {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} (C : VariableChange R) (h : C • W' = W) : (variableChangeEquiv C h) (AdjoinRoot.root W'.toAffine.polynomial) = (algebraMap R W.toAffine.CoordinateRing) ↑C.u ^ 3 * AdjoinRoot.root W.toAffine.polynomial + (algebraMap R W.toAffine.CoordinateRing) ↑C.u ^ 2 * (algebraMap R W.toAffine.CoordinateRing) C.s * (AdjoinRoot.of W.toAffine.polynomial) Polynomial.X + (algebraMap R W.toAffine.CoordinateRing) C.t

The isomorphism of a change of variables sends y' to u³y + u²sx + t.

theorem WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_symm {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} (C : VariableChange R) (h : C • W' = W) (h' : C⁻¹ • W = W') : (variableChangeEquiv C h).symm = variableChangeEquiv C⁻¹ h'

The inverse of the isomorphism of C is the isomorphism of C⁻¹.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_symm_of_X {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} (C : VariableChange R) (h : C • W' = W) : (variableChangeEquiv C h).symm ((AdjoinRoot.of W.toAffine.polynomial) Polynomial.X) = (algebraMap R W'.toAffine.CoordinateRing) ↑C⁻¹.u ^ 2 * (AdjoinRoot.of W'.toAffine.polynomial) Polynomial.X + (algebraMap R W'.toAffine.CoordinateRing) C⁻¹.r

The inverse of the isomorphism of a change of variables sends x to u⁻²(x' - r), written through the components of C⁻¹.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_symm_root {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} (C : VariableChange R) (h : C • W' = W) : (variableChangeEquiv C h).symm (AdjoinRoot.root W.toAffine.polynomial) = (algebraMap R W'.toAffine.CoordinateRing) ↑C⁻¹.u ^ 3 * AdjoinRoot.root W'.toAffine.polynomial + (algebraMap R W'.toAffine.CoordinateRing) ↑C⁻¹.u ^ 2 * (algebraMap R W'.toAffine.CoordinateRing) C⁻¹.s * (AdjoinRoot.of W'.toAffine.polynomial) Polynomial.X + (algebraMap R W'.toAffine.CoordinateRing) C⁻¹.t

The inverse of the isomorphism of a change of variables sends y to u⁻³(y' - s(x' - r) - t), written through the components of C⁻¹.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_trans {R : Type u_1} [CommRing R] {W W' W'' : WeierstrassCurve R} (C C' : VariableChange R) (h : C • W' = W) (h' : C' • W'' = W') : (variableChangeEquiv C' h').trans (variableChangeEquiv C h) = variableChangeEquiv (C * C') ⋯

The isomorphisms of changes of variables compose as the changes of variables multiply.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_one {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} (h : 1 • W = W) : variableChangeEquiv 1 h = AlgEquiv.refl

The isomorphism of the identity change of variables is the identity.

theorem WeierstrassCurve.Affine.CoordinateRing.variableChangeEquiv_inj {R : Type u_1} [CommRing R] {W W' : WeierstrassCurve R} (C C' : VariableChange R) (h : C • W' = W) (h' : C' • W' = W) : variableChangeEquiv C h = variableChangeEquiv C' h' ↔ C = C'

A change of variables is determined by its isomorphism of coordinate rings: the images of x' and y' determine u², u³, r, u²s and t, because x, y and 1 are linearly independent over R in R[W].