Tate normal form

For a b : R, the Weierstrass curve in Tate normal form is

Y² + aXY + bY = X³ + bX²,

that is, a₁ = a, a₂ = a₃ = b and a₄ = a₆ = 0 (WeierstrassCurve.tateNormalForm). The point (0, 0) lies on it. Its discriminant is b³ (a³ - a⁴ - 8a²b + 36ab - 16b² - 27b), so b is a unit whenever the curve is elliptic.

Let W be a Weierstrass curve over a commutative ring R and (x, y) a point of W with coordinates in R. Suppose that the 2-division polynomial ψ₂ = 2Y + a₁X + a₃ is a unit at (x, y) and that the 3-division polynomial Ψ₃ is a unit at x. For an elliptic curve over a field these say that the point (x, y) is killed neither by 2 nor by 3; over a ring they say this at every point of Spec R. Then exactly one change of variables carries W to Tate normal form and (x, y) to (0, 0) (WeierstrassCurve.existsUnique_variableChange_tateNormalForm). It is WeierstrassCurve.toTateNormalForm, given by

u = ψ₂³ / Ψ₃, r = x, s = (a₄ + 2a₂x - a₁y + 3x²) / ψ₂, t = y,

and the resulting curve has b = Ψ₃³ / ψ₂⁸. No hypothesis on R is needed. The translation (r, t) = (x, y) moves the point to the origin, s makes the tangent line there horizontal (a₄ = 0), and u makes a₂ = a₃. The identity behind the last step is (C • W).b₈ = u⁻⁸ Ψ₃(r) (WeierstrassCurve.variableChange_b₈_eq_eval_Ψ₃): once a₄ = a₆ = 0, the invariant b₈ is a₂a₃². For an elliptic W the two unit conditions are also necessary (WeierstrassCurve.exists_variableChange_tateNormalForm_iff). The construction commutes with base change (WeierstrassCurve.toTateNormalForm_map).

Finally, WeierstrassCurve.UniversalTate.curve is the Tate normal form with indeterminate coefficients over ℤ[A, B][Δ⁻¹]. It is elliptic, and every elliptic Tate normal form over a commutative ring is its base change along exactly one ring homomorphism (WeierstrassCurve.UniversalTate.map_lift, WeierstrassCurve.UniversalTate.eq_lift), naturally in the base ring (WeierstrassCurve.UniversalTate.comp_lift).

Main definitions

• WeierstrassCurve.tateNormalForm a b: the curve Y² + aXY + bY = X³ + bX².
• WeierstrassCurve.toTateNormalForm: the change of variables to Tate normal form centred at a point where ψ₂ and Ψ₃ are units.
• WeierstrassCurve.UniversalTate.Ring, WeierstrassCurve.UniversalTate.curve: the ring ℤ[A, B][Δ⁻¹] and the universal elliptic Tate normal form over it.
• WeierstrassCurve.UniversalTate.lift: the classifying homomorphism ℤ[A, B][Δ⁻¹] →+* R of an elliptic Tate normal form over R.
• WeierstrassCurve.UniversalTate.curveULift: the universal elliptic Tate normal form over the copy ULift.{u} ℤ[A, B][Δ⁻¹] of ℤ[A, B][Δ⁻¹] in Type u, over which it is read in schemes of universe u.

Main results

• WeierstrassCurve.tateNormalForm_Δ: the discriminant of the Tate normal form.
• WeierstrassCurve.toTateNormalForm_smul: the change of variables produces a Tate normal form, with explicit coefficients.
• WeierstrassCurve.eq_toTateNormalForm: it is the only change of variables doing so that sends (x, y) to (0, 0).
• WeierstrassCurve.existsUnique_variableChange_tateNormalForm: existence and uniqueness together.
• WeierstrassCurve.exists_variableChange_tateNormalForm_iff: for elliptic W, such a change of variables exists exactly when (x, y) lies on W and ψ₂ and Ψ₃ are units there.
• The instance Algebra.Smooth ℤ WeierstrassCurve.UniversalTate.Ring: the ring ℤ[A, B][Δ⁻¹] is smooth over ℤ.

Provenance

The UniversalTate namespace adapts the construction of the universal elliptic Weierstrass curve in TauCeti/AlgebraicGeometry/EllipticCurve/Universal.lean to two coefficients: UniversalTate.Ring is Localization.Away of the discriminant as Universal.EllipticRing is, UniversalTate.curve is the base change of the polynomial curve as Universal.ellipticCurve is, Ring.ringHom_ext follows Universal.EllipticRing.ringHom_ext, and lift, lift_comp_algebraMap, lift_algebraMap, map_lift, comp_lift and eq_lift follow the classifying homomorphism specializeElliptic and its lemmas specializeElliptic_comp_algebraMap, specializeElliptic_algebraMap, map_specializeElliptic, specializeElliptic_map and specializeElliptic_map_ellipticCurve.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, Exercise 8.13, where the normal form is written y² + (1 - c)xy - by = x³ - bx²; it is the present one with a = 1 - c and b replaced by -b.
• D. S. Kubert, Universal bounds on the torsion of elliptic curves, Proc. London Math. Soc. (3) 33 (1976), 193–237.

The Tate normal form

def WeierstrassCurve.tateNormalForm {R : Type u_1} [CommRing R] (a b : R) : WeierstrassCurve R

The Weierstrass curve Y² + aXY + bY = X³ + bX² in Tate normal form: a₁ = a, a₂ = a₃ = b and a₄ = a₆ = 0.

@[simp]

theorem WeierstrassCurve.tateNormalForm_a₁ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).a₁ = a

@[simp]

theorem WeierstrassCurve.tateNormalForm_a₂ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).a₂ = b

@[simp]

theorem WeierstrassCurve.tateNormalForm_a₃ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).a₃ = b

@[simp]

theorem WeierstrassCurve.tateNormalForm_a₄ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).a₄ = 0

@[simp]

theorem WeierstrassCurve.tateNormalForm_a₆ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).a₆ = 0

@[simp]

theorem WeierstrassCurve.tateNormalForm_b₂ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).b₂ = a ^ 2 + 4 * b

@[simp]

theorem WeierstrassCurve.tateNormalForm_b₄ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).b₄ = a * b

@[simp]

theorem WeierstrassCurve.tateNormalForm_b₆ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).b₆ = b ^ 2

@[simp]

theorem WeierstrassCurve.tateNormalForm_b₈ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).b₈ = b ^ 3

theorem WeierstrassCurve.tateNormalForm_Δ {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).Δ = b ^ 3 * (a ^ 3 - a ^ 4 - 8 * a ^ 2 * b + 36 * a * b - 16 * b ^ 2 - 27 * b)

The discriminant of the Tate normal form Y² + aXY + bY = X³ + bX².

theorem WeierstrassCurve.isUnit_of_isUnit_tateNormalForm_Δ {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (tateNormalForm a b).Δ) : IsUnit b

If the Tate normal form Y² + aXY + bY = X³ + bX² is elliptic, then b is a unit.

theorem WeierstrassCurve.equation_tateNormalForm_zero {R : Type u_1} [CommRing R] (a b : R) : (tateNormalForm a b).toAffine.Equation 0 0

The point (0, 0) lies on the Tate normal form.

@[simp]

theorem WeierstrassCurve.map_tateNormalForm {R : Type u_1} [CommRing R] (a b : R) {A : Type u_2} [CommRing A] (φ : R →+* A) : (tateNormalForm a b).map φ = tateNormalForm (φ a) (φ b)

The Tate normal form commutes with base change.

Changes of variables to Tate normal form

@[simp]

theorem WeierstrassCurve.evalEval_ψ₂_tateNormalForm_zero {R : Type u_1} [CommRing R] (a b : R) : Polynomial.evalEval 0 0 (tateNormalForm a b).ψ₂ = b

On the Tate normal form, the 2-division polynomial ψ₂ takes the value b at (0, 0).

@[simp]

theorem WeierstrassCurve.eval_Ψ₃_tateNormalForm_zero {R : Type u_1} [CommRing R] (a b : R) : Polynomial.eval 0 (tateNormalForm a b).Ψ₃ = b ^ 3

On the Tate normal form, the 3-division polynomial Ψ₃ takes the value b³ at 0.

noncomputable def WeierstrassCurve.toTateNormalForm {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) : VariableChange R

The change of variables to Tate normal form centred at a point (x, y) at which the 2-division polynomial ψ₂ and the 3-division polynomial Ψ₃ are units: u = ψ₂³ / Ψ₃, r = x, s = (a₄ + 2a₂x - a₁y + 3x²) / ψ₂ and t = y. When (x, y) lies on W, it carries W to Tate normal form (toTateNormalForm_smul) and (x, y) to (0, 0), and it is the only change of variables doing both (eq_toTateNormalForm).

@[simp]

theorem WeierstrassCurve.toTateNormalForm_u {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) : (toTateNormalForm hψ₂ hΨ₃).u = (hΨ₃.unit * hψ₂.unit⁻¹ ^ 3)⁻¹

@[simp]

theorem WeierstrassCurve.toTateNormalForm_r {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) : (toTateNormalForm hψ₂ hΨ₃).r = x

@[simp]

theorem WeierstrassCurve.toTateNormalForm_s {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) : (toTateNormalForm hψ₂ hΨ₃).s = (W.a₄ + 2 * x * W.a₂ - y * W.a₁ + 3 * x ^ 2) * ↑hψ₂.unit⁻¹

@[simp]

theorem WeierstrassCurve.toTateNormalForm_t {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) : (toTateNormalForm hψ₂ hΨ₃).t = y

theorem WeierstrassCurve.toTateNormalForm_smul {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) (h : W.toAffine.Equation x y) : toTateNormalForm hψ₂ hΨ₃ • W = tateNormalForm (Polynomial.eval x W.Ψ₃ * ↑hψ₂.unit⁻¹ ^ 3 * (W.a₁ + 2 * (toTateNormalForm hψ₂ hΨ₃).s)) (Polynomial.eval x W.Ψ₃ ^ 3 * ↑hψ₂.unit⁻¹ ^ 8)

Existence of Tate normal form. If (x, y) lies on W, and ψ₂ and Ψ₃ are units there, then toTateNormalForm carries W to the Tate normal form with a = (Ψ₃ / ψ₂³)(a₁ + 2s) and b = Ψ₃³ / ψ₂⁸.

theorem WeierstrassCurve.eq_toTateNormalForm {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) {C : VariableChange R} (hr : C.r = x) (ht : C.t = y) {a b : R} (hC : C • W = tateNormalForm a b) : C = toTateNormalForm hψ₂ hΨ₃

Uniqueness of Tate normal form. A change of variables carrying W to a Tate normal form and (x, y) to (0, 0) (that is, with r = x and t = y) is toTateNormalForm.

theorem WeierstrassCurve.existsUnique_variableChange_tateNormalForm {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) (h : W.toAffine.Equation x y) : ∃! C : VariableChange R, C.r = x ∧ C.t = y ∧ ∃ (a : R) (b : R), C • W = tateNormalForm a b

Tate normal form. If (x, y) lies on W, and the 2- and 3-division polynomials ψ₂ and Ψ₃ are units there, then exactly one change of variables carries W to a Tate normal form Y² + aXY + bY = X³ + bX² and (x, y) to (0, 0).

theorem WeierstrassCurve.exists_variableChange_tateNormalForm_iff {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} [W.IsElliptic] : (∃ (C : VariableChange R), C.r = x ∧ C.t = y ∧ ∃ (a : R) (b : R), C • W = tateNormalForm a b) ↔ W.toAffine.Equation x y ∧ IsUnit (Polynomial.evalEval x y W.ψ₂) ∧ IsUnit (Polynomial.eval x W.Ψ₃)

For an elliptic W, a change of variables carrying W to a Tate normal form and (x, y) to (0, 0) exists exactly when (x, y) lies on W and the 2- and 3-division polynomials ψ₂ and Ψ₃ are units there.

theorem WeierstrassCurve.toTateNormalForm_map {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (hψ₂ : IsUnit (Polynomial.evalEval x y W.ψ₂)) (hΨ₃ : IsUnit (Polynomial.eval x W.Ψ₃)) {A : Type u_2} [CommRing A] (φ : R →+* A) : (toTateNormalForm hψ₂ hΨ₃).map φ = toTateNormalForm ⋯ ⋯

Tate normal form commutes with base change. The image of toTateNormalForm under a ring homomorphism φ is the change of variables to Tate normal form of W.map φ at (φ x, φ y), where ψ₂ and Ψ₃ are again units since they are the images under φ of their values on W.

The universal Tate normal form over ℤ[A, B][Δ⁻¹]

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.UniversalTate.polyCurve : WeierstrassCurve (MvPolynomial (Fin 2) ℤ)

The Tate normal form Y² + AXY + BY = X³ + BX² over the polynomial ring ℤ[A, B], with the indeterminates A = X 0 and B = X 1 as coefficients.

@[reducible, inline]

abbrev WeierstrassCurve.UniversalTate.Ring : Type

The ring ℤ[A, B][Δ⁻¹]: the polynomial ring ℤ[A, B] localised away from the discriminant of the Tate normal form with coefficients A and B.

instance WeierstrassCurve.UniversalTate.instSmoothIntRing : Algebra.Smooth ℤ Ring

The ring ℤ[A, B][Δ⁻¹] is smooth over ℤ: it is a localisation of a polynomial ring in two variables.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.UniversalTate.curve : WeierstrassCurve Ring

The universal elliptic Tate normal form, over ℤ[A, B][Δ⁻¹]. Every elliptic Tate normal form over a commutative ring is its base change along exactly one ring homomorphism (map_lift, eq_lift).

instance WeierstrassCurve.UniversalTate.instIsEllipticRingCurve : curve.IsElliptic

The universal Tate normal form is an elliptic curve.

theorem WeierstrassCurve.UniversalTate.Ring.ringHom_ext {S : Type u_2} [Semiring S] {f g : Ring →+* S} (h₀ : f ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 0)) = g ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 0))) (h₁ : f ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 1)) = g ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 1))) : f = g

Two ring homomorphisms out of ℤ[A, B][Δ⁻¹] are equal as soon as they agree on the images of the indeterminates A and B.

theorem WeierstrassCurve.UniversalTate.Ring.ringHom_ext_iff {S : Type u_2} [Semiring S] {f g : Ring →+* S} : f = g ↔ f ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 0)) = g ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 0)) ∧ f ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 1)) = g ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 1))

theorem WeierstrassCurve.UniversalTate.map_polyCurve {R : Type u_1} [CommRing R] (a b : R) : polyCurve.map (MvPolynomial.eval₂Hom (Int.castRingHom R) ![a, b]) = tateNormalForm a b

Substituting a and b for the indeterminates turns polyCurve into the Tate normal form Y² + aXY + bY = X³ + bX².

noncomputable def WeierstrassCurve.UniversalTate.lift {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (tateNormalForm a b).Δ) : Ring →+* R

The classifying homomorphism ℤ[A, B][Δ⁻¹] →+* R of an elliptic Tate normal form Y² + aXY + bY = X³ + bX² over R, sending A to a and B to b.

theorem WeierstrassCurve.UniversalTate.lift_comp_algebraMap {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (tateNormalForm a b).Δ) : (lift h).comp (algebraMap (MvPolynomial (Fin 2) ℤ) Ring) = MvPolynomial.eval₂Hom (Int.castRingHom R) ![a, b]

Restricted to the polynomial ring ℤ[A, B], the classifying homomorphism substitutes a and b for the indeterminates. Use this shape when composing ring maps and lift_algebraMap when rewriting underneath an application.

theorem WeierstrassCurve.UniversalTate.lift_algebraMap {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (tateNormalForm a b).Δ) (p : MvPolynomial (Fin 2) ℤ) : (lift h) ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) p) = (MvPolynomial.eval₂Hom (Int.castRingHom R) ![a, b]) p

The pointwise form of lift_comp_algebraMap.

@[simp]

theorem WeierstrassCurve.UniversalTate.lift_algebraMap_X_zero {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (tateNormalForm a b).Δ) : (lift h) ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 0)) = a

@[simp]

theorem WeierstrassCurve.UniversalTate.lift_algebraMap_X_one {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (tateNormalForm a b).Δ) : (lift h) ((algebraMap (MvPolynomial (Fin 2) ℤ) Ring) (MvPolynomial.X 1)) = b

@[simp]

theorem WeierstrassCurve.UniversalTate.map_lift {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (tateNormalForm a b).Δ) : curve.map (lift h) = tateNormalForm a b

Every elliptic Tate normal form is the base change of the universal one along its classifying homomorphism.

theorem WeierstrassCurve.UniversalTate.comp_lift {R : Type u_1} [CommRing R] {a b : R} {S : Type u_2} [CommRing S] (φ : R →+* S) (h : IsUnit (tateNormalForm a b).Δ) : φ.comp (lift h) = lift ⋯

The classifying homomorphism is natural in the base ring: followed by a ring homomorphism φ : R →+* S, the classifying homomorphism of Y² + aXY + bY = X³ + bX² is that of its base change Y² + φ(a)XY + φ(b)Y = X³ + φ(b)X², whose discriminant is the unit φ(Δ).

theorem WeierstrassCurve.UniversalTate.eq_lift {R : Type u_1} [CommRing R] {a b : R} (h : IsUnit (tateNormalForm a b).Δ) {f : Ring →+* R} (hf : curve.map f = tateNormalForm a b) : f = lift h

The classifying homomorphism is unique: a ring homomorphism out of ℤ[A, B][Δ⁻¹] along which the universal Tate normal form becomes Y² + aXY + bY = X³ + bX² is lift.

noncomputable def WeierstrassCurve.UniversalTate.curveULift : WeierstrassCurve (ULift.{u, 0} Ring)

The universal elliptic Tate normal form Y² + AXY + BY = X³ + BX², over the copy ULift.{u} ℤ[A, B][Δ⁻¹] of its coefficient ring in Type u.

theorem WeierstrassCurve.UniversalTate.curveULift_eq : curveULift = curve.map ULift.ringEquiv.symm.toRingHom

The universal Tate normal form over ULift.{u} ℤ[A, B][Δ⁻¹] is the base change of the one over ℤ[A, B][Δ⁻¹] along the identification of the two rings.

theorem WeierstrassCurve.UniversalTate.curveULift_eq_tateNormalForm : curveULift = tateNormalForm curveULift.a₁ curveULift.a₃

The universal Tate normal form over ULift.{u} ℤ[A, B][Δ⁻¹] is a Tate normal form.

@[simp]

theorem WeierstrassCurve.UniversalTate.curveULift_a₁ : curveULift.a₁ = { down := curve.a₁ }

The coefficient a₁ of the universal Tate normal form over ULift.{u} ℤ[A, B][Δ⁻¹] is that of the one over ℤ[A, B][Δ⁻¹].

@[simp]

theorem WeierstrassCurve.UniversalTate.curveULift_a₃ : curveULift.a₃ = { down := curve.a₃ }

The coefficient a₃ of the universal Tate normal form over ULift.{u} ℤ[A, B][Δ⁻¹] is that of the one over ℤ[A, B][Δ⁻¹].

theorem WeierstrassCurve.UniversalTate.equation_curveULift_zero : curveULift.toAffine.Equation 0 0

The point (0, 0) lies on the universal Tate normal form over ULift.{u} ℤ[A, B][Δ⁻¹].

@[simp]

theorem WeierstrassCurve.UniversalTate.map_curveULift {S : Type u_2} [CommRing S] (φ : ULift.{u, 0} Ring →+* S) : curveULift.map φ = tateNormalForm (φ curveULift.a₁) (φ curveULift.a₃)

The base change of the universal Tate normal form over ULift.{u} ℤ[A, B][Δ⁻¹] along a ring homomorphism φ is the Tate normal form with the images of A and B as coefficients.

instance WeierstrassCurve.UniversalTate.instIsEllipticULiftRingCurveULift : curveULift.IsElliptic

The universal Tate normal form over ULift.{u} ℤ[A, B][Δ⁻¹] is elliptic.