Pointed isomorphisms of projective Weierstrass models are changes of variables

Let W be a Weierstrass curve over a commutative ring R. A change of variables C = (u, r, s, t) induces the isomorphism projModelVariableChangeIso W C : projModel (C • W) ≅ projModel W, [X : Y : Z] ↦ [u²X + rZ : u²sX + u³Y + tZ : Z], of projective Weierstrass models, over Spec R and carrying the zero section to the zero section. This file shows that these are all such isomorphisms, and that each comes from only one change of variables: every isomorphism projModel W ≅ projModel W' over Spec R that carries the zero section to the zero section is induced by a unique change of variables C with C • W' = W. In particular, among the changes of variables fixing W, only the identity induces the identity of projModel W. No hypothesis on W, on W' or on R is needed; in particular the base may be nonreduced.

Uniqueness. Two changes of variables are compared on the tautological point [x : y : 1] of C • W, whose coordinates lie in the affine coordinate ring R[x, y] ⧸ ((C • W)(x, y)). The isomorphisms induced by C and C' send it to the points [u²x + r : u²sx + u³y + t : 1] and [u'²x + r' : u'²s'x + u'³y + t' : 1], and x, y and 1 are linearly independent over R.

Existence. Let e : projModel W ≅ projModel W' be an isomorphism over Spec R carrying the zero section to the zero section. Since the zero section is the complement of the chart D₊(Z), e sends the tautological point [x : y : 1] of W to a point [X' : Y' : 1] with X' and Y' in the affine coordinate ring R[W]. The pole orders of X' and Y' at infinity are read on the formal neighbourhood of the zero section. Its formal point [-z : 1 : -w(z)], with values in R⟦z⟧ and w(z) = z³ + ⋯ the w-expansion of W, specializes to the zero section, so its image under e lies on the open chart D₊(Y) of W'. By uniqueness of the solution of the w-equation, the image is the formal point of W' at a parameter b(z) with b(0) = 0. The same holds for the inverse of e, and composing the two substitutions gives z, so b = z c(z) with c a unit. Over the Laurent series R⸨z⸩, the tautological point is the formal point, through the Laurent expansion R[W] → R⸨z⸩ at infinity (WeierstrassCurve.laurentExpansion). Comparing the two descriptions of its image shows that X' has a pole of order exactly 2, with unit leading coefficient, and Y' a pole of order at most 3. So X' = αx + β and Y' = γy + δx + ε with α a unit (WeierstrassCurve.exists_eq_of_coeff_laurentExpansion_eq_zero_of_lt_neg_two), and then (X', Y') is (u²x + r, u³y + u²sx + t) for a change of variables C with C • W' = W (WeierstrassCurve.Affine.CoordinateRing.exists_variableChange_of_equation). The isomorphisms e and the one induced by C agree on the tautological point, hence on the scheme-theoretically dense chart D₊(Z), hence everywhere, as the target is separated over Spec R.

The behaviour at the zero section cannot be dropped: an isomorphism of affine coordinate rings need not come from a change of variables. Over R = k[ε] ⧸ (ε²) with k a field of characteristic different from 2, the derivation ∂ = (2y + a₁x + a₃) ∂/∂x + (3x² + 2a₂x + a₄ - a₁y) ∂/∂y of R[W] gives the automorphism g ↦ g + εx ∂g, which sends x to x + εx(2y + a₁x + a₃). Its xy coefficient 2ε is nonzero, so this is not of the shape u²x + r.

Main results

• WeierstrassCurve.existsUnique_eq_eqToHom_comp_projModelVariableChangeIso_hom: an isomorphism of projective Weierstrass models over the base that carries the zero section to the zero section is induced by a unique change of variables.
• WeierstrassCurve.projModelVariableChangeIso_hom_inj: for C • W = C' • W, the isomorphisms induced by C and C' agree exactly when C = C'.
• WeierstrassCurve.eqToHom_comp_projModelVariableChangeIso_hom_inj: for C • W = W' and C' • W = W', the morphisms projModel W' ⟶ projModel W induced by C and C' agree exactly when C = C'.
• WeierstrassCurve.eqToHom_comp_projModelVariableChangeIso_hom_eq_id_iff: for C • W = W, the endomorphism of projModel W induced by C is the identity exactly when C = 1.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, III.1 (the change of variables), III.3.1(b) (the classification over a field) and IV.1 (the expansions at the zero section in the parameter z = -x / y).
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, 2.2.

Provenance

The statement of projModelVariableChangeIso_hom_inj is that of AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/ComparisonInjective.lean, declaration projModelVCIso_injective', stated here as an equivalence. The proof is not the source's. The source transports each isomorphism to an isomorphism of affine coordinate rings (pointedIsoCoordEquiv, computed for a change of variables by bridge_coordX and bridge_coordY), and treats the zero ring separately. Here both isomorphisms are evaluated on one point of the projective model, by projModelPoint_projModelVariableChangeIso_hom, with no case distinction. What is kept from the source is the last step: the coefficients are read off the linear independence of x, y and 1 over R (the source's coordXY_ext), and u and s are recovered by cancelling the unit u², here in WeierstrassCurve.VariableChange.toMatrix_injective. The other two statements are not stated in the source, which derives them where it uses them (transVC_unique and transVC_self in InvariantDifferential.lean).

The existence statement and its proof through the formal point and the Laurent expansion at infinity are not taken from the source, which derives the classification from an isomorphism of affine coordinate rings preserving their filtration by pole order (see the provenance note of TauCeti/AlgebraicGeometry/EllipticCurve/Affine/CoordinateRing/VariableChange.lean).

@[simp]

theorem WeierstrassCurve.projModelVariableChangeIso_hom_inj {R : Type u} [CommRing R] {W : WeierstrassCurve R} {C C' : VariableChange R} (h : C • W = C' • W) : (W.projModelVariableChangeIso C).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (W.projModelVariableChangeIso C').hom ↔ C = C'

A change of variables is determined by the isomorphism of projective Weierstrass models it induces. For changes of variables C and C' with C • W = C' • W, the isomorphisms projModel (C • W) ≅ projModel W and projModel (C' • W) ≅ projModel W induced by C and C' agree, through the identification of projModel (C • W) with projModel (C' • W), exactly when C = C'.

@[simp]

theorem WeierstrassCurve.eqToHom_comp_projModelVariableChangeIso_hom_inj {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} {C C' : VariableChange R} (hC : C • W = W') (hC' : C' • W = W') : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (W.projModelVariableChangeIso C).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (W.projModelVariableChangeIso C').hom ↔ C = C'

A change of variables carrying W to W' is determined by the isomorphism projModel W' ≅ projModel W it induces. For changes of variables C and C' with C • W = W' and C' • W = W', the isomorphisms induced by C and C', read as morphisms projModel W' ⟶ projModel W through the identifications of projModel W' with projModel (C • W) and with projModel (C' • W), agree exactly when C = C'.

@[simp]

theorem WeierstrassCurve.eqToHom_comp_projModelVariableChangeIso_hom_eq_id_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} {C : VariableChange R} (h : C • W = W) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (W.projModelVariableChangeIso C).hom = CategoryTheory.CategoryStruct.id W.projModel ↔ C = 1

Among the changes of variables fixing W, only the identity induces the identity of the projective Weierstrass model. For a change of variables C with C • W = W, the isomorphism induced by C, read as an endomorphism of projModel W through the identification of projModel W with projModel (C • W), is the identity exactly when C = 1. The implication from C = 1 follows from projModelVariableChangeIso_one.

Existence: a pointed isomorphism is a change of variables

theorem WeierstrassCurve.existsUnique_eq_eqToHom_comp_projModelVariableChangeIso_hom {R : Type u} [CommRing R] {W W' : WeierstrassCurve R} (e : W.projModel ≅ W'.projModel) (he : CategoryTheory.CategoryStruct.comp e.hom W'.projModelOver = W.projModelOver) (h0 : CategoryTheory.CategoryStruct.comp W.projModelZero e.hom = W'.projModelZero) : ∃! C : VariableChange R, ∃ (h : C • W' = W), e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (W'.projModelVariableChangeIso C).hom

Every pointed isomorphism of projective Weierstrass models is a change of variables. Let W and W' be Weierstrass curves over a commutative ring R, and let e : projModel W ≅ projModel W' be an isomorphism over Spec R that carries the zero section to the zero section. Then there is a unique change of variables C with C • W' = W such that e is the isomorphism projModel W ≅ projModel (C • W') ≅ projModel W' induced by C. No hypothesis on W, on W' or on R is needed.

theorem WeierstrassCurve.VariableChange.eq_of_forall_affineOpens_map_eq {S : AlgebraicGeometry.Scheme} (C₁ C₂ : VariableChange ↑(S.presheaf.obj (Opposite.op ⊤))) (h : ∀ (U : ↑S.affineOpens), C₁.map (CommRingCat.Hom.hom (S.presheaf.map (CategoryTheory.homOfLE ⋯).op)) = C₂.map (CommRingCat.Hom.hom (S.presheaf.map (CategoryTheory.homOfLE ⋯).op))) : C₁ = C₂

Changes of variables over Γ(S, ⊤) are determined by their images under restriction to the affine opens of S.

theorem WeierstrassCurve.VariableChange.exists_forall_affineOpens_map_eq {S : AlgebraicGeometry.Scheme} (C : (U : ↑S.affineOpens) → VariableChange ↑(S.presheaf.obj (Opposite.op ↑U))) (compat : ∀ (U V : ↑S.affineOpens) (hVU : ↑V ≤ ↑U), (C U).map (CommRingCat.Hom.hom (S.presheaf.map (CategoryTheory.homOfLE hVU).op)) = C V) : ∃ (C₀ : VariableChange ↑(S.presheaf.obj (Opposite.op ⊤))), ∀ (U : ↑S.affineOpens), C₀.map (CommRingCat.Hom.hom (S.presheaf.map (CategoryTheory.homOfLE ⋯).op)) = C U

Changes of variables glue along the affine opens. Changes of variables C U over Γ(S, U), one for each affine open U, compatible with restriction from an affine open to a smaller one, are the images of a change of variables over Γ(S, ⊤).