The universal Tate normal form over a scheme

Let E be an elliptic curve over a scheme S and let P be a section of E such that none of P, 2P and 3P meets the zero section over any point of S. Then (E, P) is the pullback of the universal Tate normal form

Y² + AXY + BY = X³ + BX²

over Spec ℤ[A, B][Δ⁻¹], with its point (0, 0), along exactly one morphism S ⟶ Spec ℤ[A, B][Δ⁻¹], and by exactly one cartesian morphism from E carrying the zero section to the zero section and P to (0, 0) (EllipticCurveGeom.existsUnique_tateNormalForm). Conversely, a section which is such a pullback of (0, 0) satisfies the three conditions (EllipticCurveGeom.exists_tateNormalForm_iff). So Spec ℤ[A, B][Δ⁻¹] is a fine moduli scheme for elliptic curves with a section P such that P, 2P and 3P are nowhere the zero section, with universal family the projective model of the universal Tate normal form. No hypothesis on S is needed; in particular S may be nonreduced or non-affine. By the uniqueness of the classifying morphism, an automorphism of E over S fixing the zero section and P is the identity (EllipticCurveGeom.eq_id_of_isPullback_of_comp_eq).

The coefficient ring ℤ[A, B][Δ⁻¹] (WeierstrassCurve.UniversalTate.Ring) lies in Type. For schemes in an arbitrary universe the universal Tate normal form is read over its copy ULift.{u} ℤ[A, B][Δ⁻¹] (WeierstrassCurve.UniversalTate.curveULift).

Main definitions

• WeierstrassCurve.UniversalTate.point: the point (0, 0) of the projective model of the universal Tate normal form over ULift.{u} ℤ[A, B][Δ⁻¹].
• TauCeti.AlgebraicGeometry.UniversalTate.curveGeom: the universal Tate normal form as an elliptic curve over Spec ℤ[A, B][Δ⁻¹].
• TauCeti.AlgebraicGeometry.UniversalTate.pointHom: its point (0, 0), with values in the base.

Main results

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.existsUnique_tateNormalForm: a section P such that P, 2P and 3P miss the zero section everywhere is the pullback of (0, 0) along a unique cartesian pointed morphism to the universal Tate normal form.

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_tateNormalForm_iff: such a morphism exists exactly when P, 2P and 3P miss the zero section everywhere.

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_id_of_isPullback_of_comp_eq: an automorphism of E over S fixing such a section P is the identity.

• TauCeti.AlgebraicGeometry.EllipticCurveGeom.existsUnique_tateNormalForm_curveGeom: the same universal property, with the universal Tate normal form read as the elliptic curve curveGeom.

• WeierstrassCurve.UniversalTate.smooth_terminal_from: the base Spec ℤ[A, B][Δ⁻¹] of the universal Tate normal form is smooth over Spec ℤ.

• WeierstrassCurve.UniversalTate.point_ne_projModelZero, WeierstrassCurve.UniversalTate.point_projModelMulBy_two_ne_projModelZero and WeierstrassCurve.UniversalTate.point_projModelMulBy_three_ne_projModelZero: the universal point satisfies the three conditions.

References

• D. Loeffler, Modular Curves, lecture notes, §3.3, for Tate normal form and Y₁(N).
• 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.
• N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985, Chapter 4, for fine moduli schemes of elliptic curves with level structure.

noncomputable def WeierstrassCurve.UniversalTate.point : AlgebraicGeometry.Spec ↧(ULift.{u, 0} Ring) ⟶ curveULift.projModel

The point (0, 0) of the universal Tate normal form.

@[simp]

theorem WeierstrassCurve.UniversalTate.point_def : point = curveULift.projModelAffinePoint equation_curveULift_zero

The universal point is the point [0 : 0 : 1] of the projective model.

theorem WeierstrassCurve.UniversalTate.point_projModelOver : CategoryTheory.CategoryStruct.comp point curveULift.projModelOver = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec ↧(ULift.{u, 0} Ring))

The universal point is a section of the projective model of the universal Tate normal form.

theorem WeierstrassCurve.UniversalTate.point_projModelOver_assoc {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec ↧(ULift.{u, 0} Ring) ⟶ Z) : CategoryTheory.CategoryStruct.comp point (CategoryTheory.CategoryStruct.comp curveULift.projModelOver h) = h

The universal point is a section of the projective model of the universal Tate normal form.

theorem WeierstrassCurve.UniversalTate.point_ne_projModelZero (s : ↥(AlgebraicGeometry.Spec ↧(ULift.{u, 0} Ring))) : point s ≠ curveULift.projModelZero s

The universal point (0, 0) misses the zero section at every point of the base.

theorem WeierstrassCurve.UniversalTate.point_projModelMulBy_two_ne_projModelZero (s : ↥(AlgebraicGeometry.Spec ↧(ULift.{u, 0} Ring))) : (CategoryTheory.CategoryStruct.comp point (curveULift.projModelMulBy 2)) s ≠ curveULift.projModelZero s

Twice the universal point misses the zero section at every point of the base.

theorem WeierstrassCurve.UniversalTate.point_projModelMulBy_three_ne_projModelZero (s : ↥(AlgebraicGeometry.Spec ↧(ULift.{u, 0} Ring))) : (CategoryTheory.CategoryStruct.comp point (curveULift.projModelMulBy 3)) s ≠ curveULift.projModelZero s

Three times the universal point misses the zero section at every point of the base.

Smoothness of the base

instance WeierstrassCurve.UniversalTate.smooth_terminal_from : AlgebraicGeometry.Smooth (CategoryTheory.Limits.terminal.from (AlgebraicGeometry.Spec ↧(ULift.{u, 0} Ring)))

The base Spec ℤ[A, B][Δ⁻¹] of the universal Tate normal form is smooth over Spec ℤ, the terminal scheme.

The universal Tate normal form as an elliptic curve

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.UniversalTate.curveGeom : EllipticCurveGeom (AlgebraicGeometry.Spec ↧(ULift.{u, 0} WeierstrassCurve.UniversalTate.Ring))

The universal Tate normal form Y² + AXY + BY = X³ + BX² as an elliptic curve over Spec ℤ[A, B][Δ⁻¹], whose total space is the projective model of curveULift.

noncomputable def TauCeti.AlgebraicGeometry.UniversalTate.pointHom : CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Over (AlgebraicGeometry.Spec ↧(ULift.{u, 0} WeierstrassCurve.UniversalTate.Ring))) ⟶ CategoryTheory.Over.mk curveGeom.structureMap

The point (0, 0) of the universal Tate normal form, as a point with values in the base of the elliptic curve curveGeom.

@[simp]

theorem TauCeti.AlgebraicGeometry.UniversalTate.pointHom_left : CategoryTheory.Over.Hom.left pointHom = CategoryTheory.CategoryStruct.comp WeierstrassCurve.UniversalTate.point WeierstrassCurve.UniversalTate.curveULift.toEllipticCurveGeomIso.inv

On the projective model, the point (0, 0) of curveGeom is point.

Classifying pairs

Over an affine base

Restriction to the pointed Weierstrass charts

The universal Tate normal form as an elliptic curve

The classifying pair

The universal property

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.existsUnique_tateNormalForm {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {P : S ⟶ E.carrier} (hP : CategoryTheory.CategoryStruct.comp P E.structureMap = CategoryTheory.CategoryStruct.id S) (h₁ : ∀ (s : ↥S), P s ≠ E.zero s) (h₂ : ∀ (s : ↥S), (CategoryTheory.CategoryStruct.comp P (CategoryTheory.Over.Hom.left (E.mulBy 2))) s ≠ E.zero s) (h₃ : ∀ (s : ↥S), (CategoryTheory.CategoryStruct.comp P (CategoryTheory.Over.Hom.left (E.mulBy 3))) s ≠ E.zero s) : ∃! fg : (S ⟶ AlgebraicGeometry.Spec ↧(ULift.{u, 0} WeierstrassCurve.UniversalTate.Ring)) × (E.carrier ⟶ WeierstrassCurve.UniversalTate.curveULift.projModel), CategoryTheory.IsPullback fg.2 E.structureMap WeierstrassCurve.UniversalTate.curveULift.projModelOver fg.1 ∧ CategoryTheory.CategoryStruct.comp E.zero fg.2 = CategoryTheory.CategoryStruct.comp fg.1 WeierstrassCurve.UniversalTate.curveULift.projModelZero ∧ CategoryTheory.CategoryStruct.comp P fg.2 = CategoryTheory.CategoryStruct.comp fg.1 WeierstrassCurve.UniversalTate.point

The universal Tate normal form. Let E be an elliptic curve over a scheme S and P a section of E such that none of P, 2P and 3P meets the zero section over any point of S. Then there is a unique pair of a morphism f : S ⟶ Spec ℤ[A, B][Δ⁻¹] and a morphism g from E to the projective model of the universal Tate normal form Y² + AXY + BY = X³ + BX² such that g exhibits E as the base change of the universal Tate normal form along f, carrying the zero section of E to the zero section and P to the point (0, 0). Conversely, such a pair exists only if P, 2P and 3P miss the zero section everywhere (exists_tateNormalForm_iff).

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.existsUnique_tateNormalForm_curveGeom {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {P : S ⟶ E.carrier} (hP : CategoryTheory.CategoryStruct.comp P E.structureMap = CategoryTheory.CategoryStruct.id S) (h₁ : ∀ (s : ↥S), P s ≠ E.zero s) (h₂ : ∀ (s : ↥S), (CategoryTheory.CategoryStruct.comp P (CategoryTheory.Over.Hom.left (E.mulBy 2))) s ≠ E.zero s) (h₃ : ∀ (s : ↥S), (CategoryTheory.CategoryStruct.comp P (CategoryTheory.Over.Hom.left (E.mulBy 3))) s ≠ E.zero s) : ∃! fg : (S ⟶ AlgebraicGeometry.Spec ↧(ULift.{u, 0} WeierstrassCurve.UniversalTate.Ring)) × (E.carrier ⟶ UniversalTate.curveGeom.carrier), CategoryTheory.IsPullback fg.2 E.structureMap UniversalTate.curveGeom.structureMap fg.1 ∧ CategoryTheory.CategoryStruct.comp E.zero fg.2 = CategoryTheory.CategoryStruct.comp fg.1 UniversalTate.curveGeom.zero ∧ CategoryTheory.CategoryStruct.comp P fg.2 = CategoryTheory.CategoryStruct.comp fg.1 (CategoryTheory.Over.Hom.left UniversalTate.pointHom)

The universal Tate normal form as an elliptic curve. The universal property existsUnique_tateNormalForm, with the universal Tate normal form read as the elliptic curve curveGeom and its point (0, 0) as pointHom: there is a unique pair of a morphism f : S ⟶ Spec ℤ[A, B][Δ⁻¹] and a morphism g from E to curveGeom exhibiting E as the pullback of curveGeom along f, carrying the zero section to the zero section and P to (0, 0).

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.eq_id_of_isPullback_of_comp_eq {S : AlgebraicGeometry.Scheme} {E : EllipticCurveGeom S} {P : S ⟶ E.carrier} (hP : CategoryTheory.CategoryStruct.comp P E.structureMap = CategoryTheory.CategoryStruct.id S) (h₁ : ∀ (s : ↥S), P s ≠ E.zero s) (h₂ : ∀ (s : ↥S), (CategoryTheory.CategoryStruct.comp P (CategoryTheory.Over.Hom.left (E.mulBy 2))) s ≠ E.zero s) (h₃ : ∀ (s : ↥S), (CategoryTheory.CategoryStruct.comp P (CategoryTheory.Over.Hom.left (E.mulBy 3))) s ≠ E.zero s) {τ : E.carrier ⟶ E.carrier} (hτ : CategoryTheory.IsPullback τ E.structureMap E.structureMap (CategoryTheory.CategoryStruct.id S)) (h0 : CategoryTheory.CategoryStruct.comp E.zero τ = E.zero) (hPτ : CategoryTheory.CategoryStruct.comp P τ = P) : τ = CategoryTheory.CategoryStruct.id E.carrier

Automorphisms fixing a point of order at least four are trivial. Let P be a section of E such that none of P, 2P and 3P meets the zero section over any point of S. An automorphism τ of E over S, given as a cartesian square over the identity of S, which fixes the zero section and P is the identity. The cartesian hypothesis cannot be dropped: if P is killed by N, multiplication by N + 1 fixes the zero section and P.

theorem TauCeti.AlgebraicGeometry.EllipticCurveGeom.exists_tateNormalForm_iff {S : AlgebraicGeometry.Scheme} (E : EllipticCurveGeom S) {P : S ⟶ E.carrier} (hP : CategoryTheory.CategoryStruct.comp P E.structureMap = CategoryTheory.CategoryStruct.id S) : (∃ (f : S ⟶ AlgebraicGeometry.Spec ↧(ULift.{u, 0} WeierstrassCurve.UniversalTate.Ring)) (g : E.carrier ⟶ WeierstrassCurve.UniversalTate.curveULift.projModel), CategoryTheory.IsPullback g E.structureMap WeierstrassCurve.UniversalTate.curveULift.projModelOver f ∧ CategoryTheory.CategoryStruct.comp E.zero g = CategoryTheory.CategoryStruct.comp f WeierstrassCurve.UniversalTate.curveULift.projModelZero ∧ CategoryTheory.CategoryStruct.comp P g = CategoryTheory.CategoryStruct.comp f WeierstrassCurve.UniversalTate.point) ↔ (∀ (s : ↥S), P s ≠ E.zero s) ∧ (∀ (s : ↥S), (CategoryTheory.CategoryStruct.comp P (CategoryTheory.Over.Hom.left (E.mulBy 2))) s ≠ E.zero s) ∧ ∀ (s : ↥S), (CategoryTheory.CategoryStruct.comp P (CategoryTheory.Over.Hom.left (E.mulBy 3))) s ≠ E.zero s

The conditions of the Tate normal form are necessary. A section P of an elliptic curve E over S is the pullback of the point (0, 0) of the universal Tate normal form along a cartesian morphism from E carrying the zero section to the zero section exactly when none of P, 2P and 3P meets the zero section over any point of S.