Tate normal form of a pointed projective Weierstrass model

Let W be an elliptic Weierstrass curve over a commutative ring R and let P be a section of its projective model projModel W ⟶ Spec R. Suppose that none of P, 2P and 3P meets the zero section over any point of Spec R. Then there are unique a b : R and a unique isomorphism

projModel (tateNormalForm a b) ≅ projModel W

over Spec R carrying the zero section to the zero section and the point (0, 0) of the Tate normal form Y² + aXY + bY = X³ + bX² to P (WeierstrassCurve.existsUnique_tateNormalForm and WeierstrassCurve.tateNormalForm_iso_ext). Conversely, a section which is the image of (0, 0) under such an isomorphism satisfies the three conditions (WeierstrassCurve.exists_iso_tateNormalForm_iff). No hypothesis on R is needed; in particular R may be nonreduced.

This is the scheme-theoretic form of the equation-level Tate normal form WeierstrassCurve.existsUnique_variableChange_tateNormalForm. A section missing the zero section everywhere is the point [x : y : 1] of a solution (x, y) of the affine equation (WeierstrassCurve.exists_eq_projModelAffinePoint). Its multiple nP misses the zero section everywhere exactly when the value ψₙ(x, y) of the n-th division polynomial is a unit (WeierstrassCurve.isUnit_evalEval_ψ_iff), so the conditions on 2P and 3P say that ψ₂(x, y) and Ψ₃(x) are units. An isomorphism of projective models over Spec R preserving the zero sections is a change of variables (WeierstrassCurve.existsUnique_eq_eqToHom_comp_projModelVariableChangeIso_hom), and one carrying (0, 0) to (x, y) has r = x and t = y.

Main results

• WeierstrassCurve.existsUnique_tateNormalForm: a section P such that P, 2P and 3P miss the zero section everywhere is the image of (0, 0) under a pointed isomorphism from the projective model of a Tate normal form, for unique coefficients a and b.
• WeierstrassCurve.tateNormalForm_iso_ext: such an isomorphism is unique.
• WeierstrassCurve.exists_iso_tateNormalForm_iff: such an isomorphism exists exactly when P, 2P and 3P miss the zero section everywhere.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, Exercise 8.13.
• D. S. Kubert, Universal bounds on the torsion of elliptic curves, Proc. London Math. Soc. (3) 33 (1976), 193–237.

theorem WeierstrassCurve.existsUnique_tateNormalForm {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {P : AlgebraicGeometry.Spec ↧R ⟶ W.projModel} (hP : CategoryTheory.CategoryStruct.comp P W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) (h₁ : ∀ (s : ↥(AlgebraicGeometry.Spec ↧R)), P s ≠ W.projModelZero s) (h₂ : ∀ (s : ↥(AlgebraicGeometry.Spec ↧R)), (CategoryTheory.CategoryStruct.comp P (W.projModelMulBy 2)) s ≠ W.projModelZero s) (h₃ : ∀ (s : ↥(AlgebraicGeometry.Spec ↧R)), (CategoryTheory.CategoryStruct.comp P (W.projModelMulBy 3)) s ≠ W.projModelZero s) : ∃! ab : R × R, ∃ (e : (tateNormalForm ab.1 ab.2).projModel ≅ W.projModel), CategoryTheory.CategoryStruct.comp e.hom W.projModelOver = (tateNormalForm ab.1 ab.2).projModelOver ∧ CategoryTheory.CategoryStruct.comp (tateNormalForm ab.1 ab.2).projModelZero e.hom = W.projModelZero ∧ CategoryTheory.CategoryStruct.comp ((tateNormalForm ab.1 ab.2).projModelAffinePoint ⋯) e.hom = P

Tate normal form of a pointed projective Weierstrass model. Let W be an elliptic Weierstrass curve over a commutative ring R and P a section of its projective model over Spec R such that none of P, 2P and 3P meets the zero section over any point of Spec R. Then there are unique a b : R for which some isomorphism projModel (tateNormalForm a b) ≅ projModel W over Spec R carries the zero section to the zero section and the point (0, 0) to P; such an isomorphism is itself unique (tateNormalForm_iso_ext).

theorem WeierstrassCurve.exists_iso_tateNormalForm_iff {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {P : AlgebraicGeometry.Spec ↧R ⟶ W.projModel} (hP : CategoryTheory.CategoryStruct.comp P W.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧R)) : (∃ (a : R) (b : R) (e : (tateNormalForm a b).projModel ≅ W.projModel), CategoryTheory.CategoryStruct.comp e.hom W.projModelOver = (tateNormalForm a b).projModelOver ∧ CategoryTheory.CategoryStruct.comp (tateNormalForm a b).projModelZero e.hom = W.projModelZero ∧ CategoryTheory.CategoryStruct.comp ((tateNormalForm a b).projModelAffinePoint ⋯) e.hom = P) ↔ (∀ (s : ↥(AlgebraicGeometry.Spec ↧R)), P s ≠ W.projModelZero s) ∧ (∀ (s : ↥(AlgebraicGeometry.Spec ↧R)), (CategoryTheory.CategoryStruct.comp P (W.projModelMulBy 2)) s ≠ W.projModelZero s) ∧ ∀ (s : ↥(AlgebraicGeometry.Spec ↧R)), (CategoryTheory.CategoryStruct.comp P (W.projModelMulBy 3)) s ≠ W.projModelZero s

The hypotheses of the Tate normal form are necessary. A section P of the projective model of an elliptic Weierstrass curve W over Spec R is the image of the point (0, 0) under some isomorphism projModel (tateNormalForm a b) ≅ projModel W over Spec R carrying the zero section to the zero section exactly when none of P, 2P and 3P meets the zero section over any point of Spec R.

theorem WeierstrassCurve.tateNormalForm_iso_ext {R : Type u} [CommRing R] {W : WeierstrassCurve R} [W.IsElliptic] {a b : R} {e e' : (tateNormalForm a b).projModel ≅ W.projModel} (he : CategoryTheory.CategoryStruct.comp e.hom W.projModelOver = (tateNormalForm a b).projModelOver) (he₀ : CategoryTheory.CategoryStruct.comp (tateNormalForm a b).projModelZero e.hom = W.projModelZero) (he' : CategoryTheory.CategoryStruct.comp e'.hom W.projModelOver = (tateNormalForm a b).projModelOver) (he'₀ : CategoryTheory.CategoryStruct.comp (tateNormalForm a b).projModelZero e'.hom = W.projModelZero) (hee' : CategoryTheory.CategoryStruct.comp ((tateNormalForm a b).projModelAffinePoint ⋯) e.hom = CategoryTheory.CategoryStruct.comp ((tateNormalForm a b).projModelAffinePoint ⋯) e'.hom) : e = e'

Uniqueness of the isomorphism with a Tate normal form. Two isomorphisms projModel (tateNormalForm a b) ≅ projModel W over Spec R which carry the zero section to the zero section and the point (0, 0) to the same section of projModel W are equal.