The universal elliptic curve

This file defines the universal Weierstrass curve (Universal.curve) over the polynomial ring ℤ[A₁,A₂,A₃,A₄,A₆], and the universal pointed elliptic curve (Universal.pointedCurve) over the field of fractions (Universal.Field) of Universal.Ring = Universal.Poly/⟨P⟩ = ℤ[A₁,A₂,A₃,A₄,A₆,X,Y]/⟨P⟩ (where P is the Weierstrass polynomial) with distinguished point (X,Y).

It also defines the universal elliptic Weierstrass curve (Universal.ellipticCurve) over Universal.EllipticRing = ℤ[A₁,A₂,A₃,A₄,A₆][Δ⁻¹], the polynomial ring localised away from the discriminant Δ of the universal curve, and the classifying homomorphism (WeierstrassCurve.specializeElliptic) along which an elliptic Weierstrass curve over any commutative ring is the base change of that curve.

Main definitions

• WeierstrassCurve.Universal.curve: the universal Weierstrass curve, over ℤ[A₁,⋯,A₆].
• WeierstrassCurve.Universal.Poly, .Ring, .Field: the polynomial ring ℤ[A₁,⋯,A₆,X,Y], its quotient by the Weierstrass polynomial, and that quotient's field of fractions; polyToField is the composite Poly →+* Field.
• WeierstrassCurve.Universal.pointedCurve: the universal curve over Universal.Field. It is an elliptic curve, and carries the distinguished point Universal.Affine.point (Universal.Jacobian.point in Jacobian coordinates).
• WeierstrassCurve.specialize: for a Weierstrass curve W over a commutative ring R, the specialization homomorphism ℤ[A₁,⋯,A₆] →+* R substituting W's coefficients.
• WeierstrassCurve.Universal.polyEval, .ringEval: the homomorphism Universal.Poly →+* R induced by a point (x,y) of the affine plane, and its factorisation Universal.Ring →+* R through the Weierstrass polynomial when (x,y) lies on W.
• WeierstrassCurve.Universal.EllipticRing: the ring ℤ[A₁,⋯,A₆][Δ⁻¹], a Noetherian integral domain.
• WeierstrassCurve.Universal.ellipticCurve: the universal curve over Universal.EllipticRing. It is an elliptic curve.
• WeierstrassCurve.specializeElliptic: for an elliptic Weierstrass curve W over a commutative ring R, the classifying homomorphism ℤ[A₁,⋯,A₆][Δ⁻¹] →+* R extending W.specialize.

Main results

• WeierstrassCurve.Universal.polyToField_polynomial: the Weierstrass polynomial vanishes in the universal field — the relation Universal.Ring is the quotient by.
• WeierstrassCurve.Universal.equation_point: (X,Y) satisfies the affine Weierstrass equation of pointedCurve — the universal curve really is pointed.
• WeierstrassCurve.map_specialize: every Weierstrass curve is a specialization of the universal one.
• WeierstrassCurve.specialize_Δ: specialize sends the discriminant of the universal curve to the discriminant of W.
• WeierstrassCurve.Universal.map_ringEval: pushing the universal curve over Universal.Ring along ringEval returns W, so one identity over curveRing is the same identity for every curve and every point on it. Note the restriction: ringEval maps out of Universal.Ring, so it transports identities over curveRing, not over pointedCurve, which lives over Universal.Field. An identity stated there needs its denominators cleared into Universal.Ring first.
• WeierstrassCurve.Universal.map_polyToField: curvePoly pushed along polyToField is pointedCurve. Named rather than left definitional, because the module system does not expose polyToField's body; this is what lands a Jacobian formula transported from Poly on pointedCurve rather than on an unreduced base change.
• WeierstrassCurve.Universal.ringHom_ext: two homomorphisms out of Universal.Ring agreeing on the coefficient ring and on the two distinguished coordinates are equal — the uniqueness half of the universal property, since those generate.
• WeierstrassCurve.Universal.algebraMap_field_injective: ℤ[A₁,⋯,A₆] embeds in Universal.Field, which is what makes pointedCurve an elliptic curve.
• WeierstrassCurve.map_specializeElliptic: every elliptic Weierstrass curve is the base change of Universal.ellipticCurve along its classifying homomorphism.
• WeierstrassCurve.specializeElliptic_map_ellipticCurve: a homomorphism out of Universal.EllipticRing is the classifying homomorphism of the curve it produces, so the classifying homomorphism is unique. WeierstrassCurve.Universal.EllipticRing.ringHom_ext is the extensionality behind it: the images of the five indeterminates determine the homomorphism.
• WeierstrassCurve.specializeElliptic_map: the classifying homomorphism is natural in the base ring.

Implementation notes

The cusp curve Y² = X³ carries the rational point (1,1), with the nice property that ψₙ(1,1) = n. Specializing along it is therefore the cheap route to nonvanishing of the universal ψₙ for n ≠ 0, which shows that (X,Y) is a point of infinite order on the universal pointed elliptic curve. The CharZero Universal.Ring instance is the first use of that argument.

Roadmap

The [n]-is-division-polynomials bullet of TauCetiRoadmap/EllipticCurves/README.md's opening narrative on isogenies asks for multiplication by n ≠ 0 as an isogeny of degree n² whose pullback is "pinned by the division-polynomial multiplication formula, already proved at the point level in the Lutz–Nagell provenance through J. Xu's work (mathlib #13782 / ZSMul.lean) — the mathlib-track anchor Layer 1 consumes". This file is the Universal.Ring prerequisite of that ZSMul.lean: ringEval is what turns a single identity over curveRing into the same identity for every Weierstrass curve and every point on it, so the point-level [n]-compatibility is proved once, universally, rather than curve by curve. It maps out of Universal.Ring; identities over pointedCurve, which is over Universal.Field, transport only after their denominators are cleared into Universal.Ring. Mathlib PR #13782 is still open, so the whole Universal namespace below is absent from Mathlib.

Provenance

Ported from J. Xu's LutzNagell/Universal.lean in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache 2.0, main at 1c1c7466, projects/NagellLutz/LutzNagell/Universal.lean), the source the roadmap pins for the Nagell–Lutz strand. Most declarations here come from that file: the Coeff index type and the bulk of the Universal namespace (curve, Poly, Ring, Field, polyToField, pointedCurve, Affine.point, Jacobian.point, curvePoly and curveRing with their lemmas), and the specialization API (specialize, polyEval, ringEval with their compatibility lemmas).

Three groups are not simple ports, and are listed among the adaptations below: ringHom_ext is new, and so is map_polyToField — upstream that identity is definitional and is taken as rfl inside the ZSMul.lean proofs that need it, which this repository's unexposed polyToField makes impossible; the CharZero Universal.Ring instance replaces the source's Poly.two_ne_zero and Field.two_ne_zero rather than porting them, and carries the field case with it — Mathlib derives CharZero Universal.Field from it through IsFractionRing.charZero, so no second instance is declared. That derivation is why Mathlib.Algebra.CharP.Algebra is imported: without it (2 : Universal.Field) ≠ 0, which the division-polynomial addition formulas need, does not synthesize. And the equation lemmas for the opaque definitions (polyToField_apply, Affine.point_def, Jacobian.point_def, pointedCurve_Δ) exist because this repository's module system leaves definition bodies unexposed. That file's header reads Authors: Junyan Xu; following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header.

Four adaptations were made. The file was converted to this repository's module system (module, public import, public section). The source's three opening lemmas — CoordinateRing.algebraMap_poly_injective, CoordinateRing.algebraMap_injective' and Affine.Point.some_eq_some_iff — are not ported: the first two are FaithfulSMul.algebraMap_injective applied to Mathlib's own FaithfulSMul instances on the coordinate ring, and the third is the Iff reading of the auto-generated some.injEq, which simp proves alone. This repository declines such wrappers, and had already declined the analogous instances in Affine/FunctionField/Finrank.lean; the one internal use, in algebraMap_field_injective, calls FaithfulSMul.algebraMap_injective directly. Dropping them also removes the source's set_option backward.isDefEq.respectTransparency false in, which existed only for the first of them and which TauCeti/ forbids in any case. No definition in this file is exposed. polyToField_apply, algebraMap_field_eq_comp, the five pointedCurve_aᵢ lemmas and the two point_def lemmas are proved := (rfl): the parentheses satisfy the module system's export check without publishing any body, which is what an @[expose] would do. The section is a plain public section for the reason spelled out in TauCeti/AlgebraicGeometry/EllipticCurve/Affine/Point/VariableChange.lean — exposing the whole file would publish every proof body to make a handful of rfls go through. And equation_point opens with change where the source has show, that step rewriting the goal rather than only naming it (linter.style.show).

polyToField_polynomial is the source's declaration of that name (its :120), and the last of this file's declarations to arrive; equation_point, which the source also routes through it, does so here too. One difference: upstream it is @[simp], and here it must not be. simp can already prove the statement, because this file's polyToField_apply is @[simp] where the source's is not, and the tag therefore fails scripts/lint-env.sh with a fresh simpNF violation ("simp can prove this: by simp only [*, polyToField_apply, AdjoinRoot.mk_self, map_zero]"). Untagged, that run reports no new violations. Being redundant for simp does not make the name redundant: three proofs cite it by name, equation_point here and the two doubling formulas in DivisionPolynomial/ZSMul.lean.

The section on the universal elliptic Weierstrass curve has a second source: the ModularCurves project of AINTLIB (github.com/CBirkbeck/AINTLIB, Apache 2.0, commit c3415f32a313e19ace43e05479aeaa0d56ca287a, under projects/ModularCurves/ModularCurves/). Adapted from it are WeierstrassAtlasRing with its IsDomain and IsNoetherianRing instances and universalWeierstrassLoc with its IsElliptic instance (Moduli/WeierstrassAtlas.lean), classifyRingHom and universalWeierstrassLoc_map_classifyRingHom (EllipticCurve/WeierstrassAtlasBundle.lean), classifyRingHom_map and classifyRingHom_universalWeierstrassLoc (EllipticCurve/AdditionBaseChange.lean), and ringHomOfEllipticW_ellipticWOfRingHom (Moduli/MellWeierstrass.lean). Those headers read Authors: Chris Birkbeck, except that of WeierstrassAtlasBundle.lean, which reads Authors: The AINTLIB Authors.

The source builds these on a second universal curve, universalWeierstrass over MvPolynomial (Fin 5) ℤ, with its own coefficient maps classifyCoeffHom and specializeAt. Here they are built on this file's Universal.curve and specialize, so there is one universal curve and specializeElliptic extends specialize. EllipticRing.ringHom_ext is new: the source repeats IsLocalization.ringHom_ext and MvPolynomial.ringHom_ext inside each proof. specializeElliptic_map and specializeElliptic_ellipticCurve are corollaries of specializeElliptic_map_ellipticCurve rather than separate computations, and specializeElliptic_map takes the ellipticity of W.map f from Mathlib's instance instead of a second hypothesis. The Noetherian instance is not declared: instance search derives it from Mathlib's instances once Coeff is a Fintype. The source's ULift copies in higher universes (WeierstrassAtlasRingU, universalWeierstrassLocU, classifyRingHomU) are not ported.

The universal elliptic curve

inductive WeierstrassCurve.Coeff : Type

A type whose elements represent the five coefficients a₁, a₂, a₃, a₄ and a₆ of the Weierstrass polynomial. It indexes the variables of MvPolynomial Coeff ℤ = ℤ[A₁,⋯,A₆], the ring the universal curve is defined over. There is no A₅ — the subscripts are weights, not positions — and the constructors are uppercase as names of indeterminates: specialize sends A₁ to W.a₁.

• A₁ : Coeff
• A₂ : Coeff
• A₃ : Coeff
• A₄ : Coeff
• A₆ : Coeff

@[instance_reducible]

instance WeierstrassCurve.instFintypeCoeff : Fintype Coeff

The five coefficient indices form a finite type, so ℤ[A₁,⋯,A₆] and its localisations are Noetherian rings.

Equations

• WeierstrassCurve.instFintypeCoeff = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Unit ⊕ Unit ⊕ Unit) WeierstrassCurve.Coeff.proxyTypeEquiv

noncomputable def WeierstrassCurve.Universal.curve : Affine (MvPolynomial Coeff ℤ)

The universal Weierstrass curve: the curve over ℤ[A₁,⋯,A₆] = MvPolynomial Coeff ℤ (the universal polynomial ring for Weierstrass curves) whose five coefficients are the five indeterminates. Every Weierstrass curve is one of its specializations (map_specialize); its base changes are curvePoly, curveRing and pointedCurve.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.Universal.curve_a₁ : curve.a₁ = MvPolynomial.X Coeff.A₁

The a₁ coefficient of the universal curve is the indeterminate A₁, and likewise for A₂ through A₆. The definition body is unexposed, so these are how a consumer normalises a coefficient of curve inside a polynomial identity.

@[simp]

theorem WeierstrassCurve.Universal.curve_a₂ : curve.a₂ = MvPolynomial.X Coeff.A₂

The a₂ coefficient of the universal curve is the indeterminate A₂.

@[simp]

theorem WeierstrassCurve.Universal.curve_a₃ : curve.a₃ = MvPolynomial.X Coeff.A₃

The a₃ coefficient of the universal curve is the indeterminate A₃.

@[simp]

theorem WeierstrassCurve.Universal.curve_a₄ : curve.a₄ = MvPolynomial.X Coeff.A₄

The a₄ coefficient of the universal curve is the indeterminate A₄.

@[simp]

theorem WeierstrassCurve.Universal.curve_a₆ : curve.a₆ = MvPolynomial.X Coeff.A₆

The a₆ coefficient of the universal curve is the indeterminate A₆.

theorem WeierstrassCurve.Universal.curve_Δ_ne_zero : Δ curve ≠ 0

The discriminant of the universal Weierstrass curve is a nonzero polynomial in ℤ[A₁,⋯,A₆], i.e. a Weierstrass equation is not singular identically in its coefficients. Transported along algebraMap_field_injective, this is what makes pointedCurve elliptic over Universal.Field.

@[reducible, inline]

abbrev WeierstrassCurve.Universal.Poly : Type

The polynomial ring ℤ[A₁,A₂,A₃,A₄,A₆,X,Y]: two variables adjoined to the universal polynomial ring ℤ[A₁,⋯,A₆], in Mathlib's iterated form R[X][Y], so Y is the outer variable. The Weierstrass polynomial curve.polynomial lives here; Universal.Ring is the quotient by it.

Equations

• WeierstrassCurve.Universal.Poly = Polynomial (Polynomial (MvPolynomial WeierstrassCurve.Coeff ℤ))

@[reducible, inline]

abbrev WeierstrassCurve.Universal.Ring : Type

The universal ring for pointed Weierstrass curves: ℤ[A₁,⋯,A₆,X,Y]/⟨P⟩, for P the Weierstrass polynomial. A Weierstrass curve over R together with an affine point on it determines a ring homomorphism out of it — ringEval — and determines it uniquely, since the coefficients and the two coordinates generate (ringHom_ext). Being an abbrev for curve.CoordinateRing, it inherits Mathlib's Affine.CoordinateRing API.

Equations

• WeierstrassCurve.Universal.Ring = WeierstrassCurve.Universal.curve.CoordinateRing

@[reducible, inline]

abbrev WeierstrassCurve.Universal.Field : Type

The universal field for pointed Weierstrass curves is the field of fractions of the universal ring.

Equations

• WeierstrassCurve.Universal.Field = FractionRing WeierstrassCurve.Universal.Ring

noncomputable def WeierstrassCurve.Universal.polyToField : Poly →+* Universal.Field

The ring homomorphism ℤ[A₁,⋯,A₆,X,Y] → Universal.Field: reduce modulo the Weierstrass polynomial, then include the universal ring into its fraction field. Every statement about the universal pointed curve is ultimately about the images of X and Y under this map.

Equations

• WeierstrassCurve.Universal.polyToField = (algebraMap WeierstrassCurve.Universal.Ring WeierstrassCurve.Universal.Field).comp (AdjoinRoot.mk WeierstrassCurve.Universal.curve.polynomial)

@[simp]

theorem WeierstrassCurve.Universal.polyToField_apply (p : Poly) : polyToField p = (algebraMap Universal.Ring Universal.Field) ((AdjoinRoot.mk curve.polynomial) p)

polyToField is reduction modulo the Weierstrass polynomial followed by the inclusion into the fraction field.

theorem WeierstrassCurve.Universal.polyToField_polynomial : polyToField curve.polynomial = 0

The Weierstrass polynomial vanishes in the universal field. It is exactly the element Universal.Ring quotients out, so polyToField kills it — which is how an identity over pointedCurve discards the multiples of curve.polynomial that clearing denominators throws up.

theorem WeierstrassCurve.Universal.algebraMap_field_eq_comp : algebraMap (MvPolynomial Coeff ℤ) Universal.Field = polyToField.comp (algebraMap (MvPolynomial Coeff ℤ) Poly)

The structure map of Universal.Field over the coefficient ring factors through Poly: the coefficients A₁,⋯,A₆ reach the universal field by the same route as X and Y do. Rewriting with this turns a statement about algebraMap into one about polyToField.

theorem WeierstrassCurve.Universal.algebraMap_ring_eq_comp : algebraMap (MvPolynomial Coeff ℤ) Universal.Ring = (AdjoinRoot.mk curve.polynomial).comp (algebraMap (MvPolynomial Coeff ℤ) (Polynomial (Polynomial (MvPolynomial Coeff ℤ))))

The Universal.Ring counterpart of algebraMap_field_eq_comp: the structure map from the coefficient ring is the inclusion ℤ[A₁,⋯,A₆] → Poly followed by the quotient map.

theorem WeierstrassCurve.Universal.algebraMap_field_injective : Function.Injective ⇑(algebraMap (MvPolynomial Coeff ℤ) Universal.Field)

The coefficient ring ℤ[A₁,⋯,A₆] embeds in the universal field: the five indeterminates stay algebraically independent after adjoining a point and passing to fractions. This is what carries curve_Δ_ne_zero over to pointedCurve, giving the IsElliptic instance below.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Universal.pointedCurve : WeierstrassCurve Universal.Field

The universal pointed Weierstrass curve: the universal curve base-changed to the universal field, over which it is an elliptic curve (instance below) carrying the distinguished point (X, Y) (equation_point, packaged as Affine.point). It is the base change to Universal.Field, and so is the third of curvePoly, curveRing, pointedCurve.

Equations

• WeierstrassCurve.Universal.pointedCurve = WeierstrassCurve.baseChange WeierstrassCurve.Universal.curve WeierstrassCurve.Universal.Field

theorem WeierstrassCurve.Universal.pointedCurve_Δ : pointedCurve.Δ = (algebraMap (MvPolynomial Coeff ℤ) Universal.Field) (Δ curve)

The discriminant of pointedCurve is the image of curve.Δ. pointedCurve is by definition curve.baseChange Universal.Field, so this is map_Δ at that base change — named here rather than reached through a definitional show, so the ellipticity proof rewrites with an ordinary equation and the reliance on that definitional unfolding sits in one place.

instance WeierstrassCurve.Universal.instIsEllipticFieldPointedCurve : pointedCurve.IsElliptic

The universal pointed Weierstrass curve is an elliptic curve: its discriminant is a unit, because Δ of the universal curve is a nonzero polynomial and the coefficient ring embeds in the universal field.

theorem WeierstrassCurve.Universal.equation_point : pointedCurve.toAffine.Equation (polyToField (Polynomial.C Polynomial.X)) (polyToField Polynomial.X)

The pair (X, Y) — the images of the two adjoined variables in the universal field — satisfies the affine Weierstrass equation of pointedCurve. This is what makes the universal curve pointed; Affine.point packages it as an element of the point group.

noncomputable def WeierstrassCurve.Universal.Affine.point : (toAffine (curve.baseChange Universal.Field)).Point

The distinguished point on the universal pointed Weierstrass curve.

Equations

• WeierstrassCurve.Universal.Affine.point = WeierstrassCurve.Affine.Point.mk WeierstrassCurve.Universal.equation_point

@[simp]

theorem WeierstrassCurve.Universal.Affine.point_def : point = Affine.Point.mk equation_point

The affine distinguished point is equation_point packaged as a point of the group. The definition body is not exposed, so this equation lemma is how a consumer recovers it.

noncomputable def WeierstrassCurve.Universal.Jacobian.point : Jacobian.Point (curve.baseChange Universal.Field)

The distinguished point on the universal curve in Jacobian coordinates.

Equations

• WeierstrassCurve.Universal.Jacobian.point = WeierstrassCurve.Jacobian.Point.fromAffine WeierstrassCurve.Universal.Affine.point

@[simp]

theorem WeierstrassCurve.Universal.Jacobian.point_def : point = Jacobian.Point.fromAffine Affine.point

The Jacobian distinguished point is the affine one, moved along fromAffine.

theorem WeierstrassCurve.Universal.pointedCurve_a₁ : pointedCurve.a₁ = polyToField (Polynomial.CC curve.a₁)

The a₁ coefficient of pointedCurve is the image of the indeterminate A₁ in the universal field, and likewise for pointedCurve_a₂ through pointedCurve_a₆.

None of the five is @[simp]: pointedCurve is curve.baseChange Universal.Field, which unfolds to curve.map (algebraMap _ _), so simp already rewrites pointedCurve.a₁ with Mathlib's WeierstrassCurve.map_a₁, to algebraMap _ _ curve.a₁; tagging these would put a non-normal-form left-hand side in the simp set. They are the polyToField reading of the same coefficients, for use by name.

theorem WeierstrassCurve.Universal.pointedCurve_a₂ : pointedCurve.a₂ = polyToField (Polynomial.CC curve.a₂)

The a₂ coefficient of pointedCurve is the image of the indeterminate A₂.

theorem WeierstrassCurve.Universal.pointedCurve_a₃ : pointedCurve.a₃ = polyToField (Polynomial.CC curve.a₃)

The a₃ coefficient of pointedCurve is the image of the indeterminate A₃.

theorem WeierstrassCurve.Universal.pointedCurve_a₄ : pointedCurve.a₄ = polyToField (Polynomial.CC curve.a₄)

The a₄ coefficient of pointedCurve is the image of the indeterminate A₄.

theorem WeierstrassCurve.Universal.pointedCurve_a₆ : pointedCurve.a₆ = polyToField (Polynomial.CC curve.a₆)

The a₆ coefficient of pointedCurve is the image of the indeterminate A₆.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Universal.curvePoly : WeierstrassCurve Poly

The base change of the universal curve from ℤ[A₁,⋯,A₆] to ℤ[A₁,⋯,A₆,X,Y].

Equations

• WeierstrassCurve.Universal.curvePoly = WeierstrassCurve.Universal.curve.baseChange WeierstrassCurve.Universal.Poly

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Universal.curveRing : WeierstrassCurve Universal.Ring

The base change of the universal curve from ℤ[A₁,⋯,A₆] to ℤ[A₁,⋯,A₆,X,Y]/⟨P⟩ (the universal ring), where P is the Weierstrass polynomial.

Equations

• WeierstrassCurve.Universal.curveRing = WeierstrassCurve.Universal.curve.baseChange WeierstrassCurve.Universal.Ring

@[simp]

theorem WeierstrassCurve.Universal.map_polyToField : curvePoly.map polyToField = pointedCurve

Pushing curvePoly along polyToField gives pointedCurve: the base change of the universal curve to ℤ[A₁,⋯,A₆,X,Y] and its base change to the universal field agree along polyToField.

The curve-dependent Jacobian transports state their left-hand side over W.map f, so pushing one from Poly to Universal.Field produces curvePoly.map polyToField and needs this lemma to land on pointedCurve: map_dblZ, map_dblXYZ, map_addX, map_addY, map_addXYZ. map_addZ is not among them — addZ takes no curve argument, so its transport is curve-free.

noncomputable def WeierstrassCurve.specialize {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPolynomial Coeff ℤ →+* R

The specialization homomorphism from ℤ[A₁, ⋯, A₆] to the ring of definition of the Weierstrass curve.

Equations

• W.specialize = (MvPolynomial.aeval fun (t : WeierstrassCurve.Coeff) => WeierstrassCurve.Coeff.rec W.a₁ W.a₂ W.a₃ W.a₄ W.a₆ t).toRingHom

@[simp]

theorem WeierstrassCurve.specialize_X {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (i : Coeff) : W.specialize (MvPolynomial.X i) = Coeff.rec W.a₁ W.a₂ W.a₃ W.a₄ W.a₆ i

specialize sends each indeterminate to the corresponding coefficient of W. With curve_a₁‥curve_a₆ this normalises coefficient evaluation inside a polynomial identity, without unfolding either definition.

@[simp]

theorem WeierstrassCurve.map_specialize {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Universal.curve.map W.specialize = W

Every Weierstrass curve is a specialization of the universal Weierstrass curve.

@[simp]

theorem WeierstrassCurve.specialize_Δ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.specialize (Δ Universal.curve) = W.Δ

specialize sends the discriminant of the universal curve to the discriminant of W.

noncomputable def WeierstrassCurve.Universal.polyEval {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (x y : R) : Poly →+* R

A point in the affine plane over R induces an evaluation homomorphism from ℤ[A₁, ⋯, A₆, X, Y] to R.

Equations

• WeierstrassCurve.Universal.polyEval W x y = Polynomial.eval₂RingHom (Polynomial.eval₂RingHom W.specialize x) y

@[simp]

theorem WeierstrassCurve.Universal.polyEval_apply {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (x y : R) (p : Poly) : (polyEval W x y) p = Polynomial.evalEval x y (Polynomial.map (Polynomial.mapRingHom W.specialize) p)

polyEval computes in the expected order: substitute W's coefficients for the indeterminates A₁,⋯,A₆, then evaluate the resulting bivariate polynomial at (x, y).

noncomputable def WeierstrassCurve.Universal.ringEval {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : Universal.Ring →+* R

A point on a Weierstrass curve over R induces a specialization homomorphism from the universal ring to R.

Equations

• WeierstrassCurve.Universal.ringEval eqn = AdjoinRoot.lift (Polynomial.eval₂RingHom W.specialize x) y ⋯

@[simp]

theorem WeierstrassCurve.Universal.ringEval_mk {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) (p : Poly) : (ringEval eqn) ((AdjoinRoot.mk curve.polynomial) p) = (polyEval W x y) p

ringEval is polyEval read on the quotient: evaluating a representative p gives the same answer as evaluating p in Poly. The pointwise form of ringEval_comp_mk.

@[simp]

theorem WeierstrassCurve.Universal.ringEval_comp_mk {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : (ringEval eqn).comp (AdjoinRoot.mk curve.polynomial) = polyEval W x y

The homomorphism-level form of ringEval_mk: ringEval eqn is the factorisation of polyEval W x y through the quotient by the Weierstrass polynomial. Use this shape when composing ring maps and ringEval_mk when rewriting underneath an application.

@[simp]

theorem WeierstrassCurve.Universal.ringEval_of_X {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : (ringEval eqn) ((AdjoinRoot.of curve.polynomial) Polynomial.X) = x

ringEval sends the distinguished X to the abscissa of the point. Together with ringEval_root this is the coordinate-level content of the universal property: the pair (X, Y) of Universal.Ring goes to the chosen point (x, y) of W.

@[simp]

theorem WeierstrassCurve.Universal.ringEval_root {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : (ringEval eqn) (AdjoinRoot.root curve.polynomial) = y

ringEval sends the distinguished Y to the ordinate of the point.

@[simp]

theorem WeierstrassCurve.Universal.polyEval_comp_eq_specialize {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} : (polyEval W x y).comp (algebraMap (MvPolynomial Coeff ℤ) Poly) = W.specialize

Restricted to the coefficient ring, polyEval W x y is just W.specialize: evaluating at a point does not disturb the substitution of W's coefficients.

theorem WeierstrassCurve.Universal.ringHom_ext {R : Type u_1} [Semiring R] {f g : Universal.Ring →+* R} (hcoeff : f.comp (algebraMap (MvPolynomial Coeff ℤ) Universal.Ring) = g.comp (algebraMap (MvPolynomial Coeff ℤ) Universal.Ring)) (hX : f ((AdjoinRoot.of curve.polynomial) Polynomial.X) = g ((AdjoinRoot.of curve.polynomial) Polynomial.X)) (hY : f (AdjoinRoot.root curve.polynomial) = g (AdjoinRoot.root curve.polynomial)) : f = g

Extensionality for homomorphisms out of the universal ring. Two ring homomorphisms out of Universal.Ring are equal as soon as they agree on the coefficient ring ℤ[A₁,⋯,A₆] and on the two distinguished coordinates X and Y — that is, on generators.

Together with ringEval_comp_eq_specialize, ringEval_of_X and ringEval_root this is the uniqueness half of the universal property: ringEval is not merely a homomorphism carrying the universal curve and its point to W and (x, y), it is the only one. That is what licenses proving an identity once over curveRing and reading it off for every curve and every point.

Agreement after composing with AdjoinRoot.mk would not do: mk is surjective, so that hypothesis is merely a restatement of the conclusion and proves nothing about generators.

theorem WeierstrassCurve.Universal.ringHom_ext_iff {R : Type u_1} [Semiring R] {f g : Universal.Ring →+* R} : f = g ↔ f.comp (algebraMap (MvPolynomial Coeff ℤ) Universal.Ring) = g.comp (algebraMap (MvPolynomial Coeff ℤ) Universal.Ring) ∧ f ((AdjoinRoot.of curve.polynomial) Polynomial.X) = g ((AdjoinRoot.of curve.polynomial) Polynomial.X) ∧ f (AdjoinRoot.root curve.polynomial) = g (AdjoinRoot.root curve.polynomial)

@[simp]

theorem WeierstrassCurve.Universal.ringEval_comp_eq_specialize {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : (ringEval eqn).comp (algebraMap (MvPolynomial Coeff ℤ) Universal.Ring) = W.specialize

The Universal.Ring counterpart of polyEval_comp_eq_specialize: ringEval eqn also restricts to W.specialize on the coefficient ring. This is the compatibility that makes map_ringEval, and with it every specialization argument, go through.

instance WeierstrassCurve.Universal.instCharZeroRing : CharZero Universal.Ring

The universal ring has characteristic zero: specializing to the cusp curve at (1, 1) retracts it onto ℤ. This is the first use of that specialization argument, and it is what gives (2 : Universal.Ring) ≠ 0 — needed by the halving steps of the group law and of the division-polynomial recursion.

@[simp]

theorem WeierstrassCurve.Universal.map_ringEval {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : curveRing.map (ringEval eqn) = W

Specialization is compatible with base change: pushing the universal curve over Universal.Ring along ringEval eqn returns W itself. This is the mechanism the whole file exists for — an identity proved once for curveRing and its distinguished point becomes the same identity for every Weierstrass curve W and every point (x, y) on it.

The universal elliptic Weierstrass curve over ℤ[A₁,⋯,A₆][Δ⁻¹]

@[reducible, inline]

abbrev WeierstrassCurve.Universal.EllipticRing : Type

The universal ring for elliptic Weierstrass curves: ℤ[A₁,⋯,A₆][Δ⁻¹], the universal polynomial ring ℤ[A₁,⋯,A₆] localised away from the discriminant of the universal curve. Being an abbrev for Localization.Away curve.Δ, it inherits Mathlib's localisation API, and with it the Noetherian instance.

Equations

• WeierstrassCurve.Universal.EllipticRing = Localization.Away (WeierstrassCurve.Δ WeierstrassCurve.Universal.curve)

instance WeierstrassCurve.Universal.instIsDomainEllipticRing : IsDomain EllipticRing

ℤ[A₁,⋯,A₆][Δ⁻¹] is an integral domain, since the universal discriminant is nonzero (curve_Δ_ne_zero).

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Universal.ellipticCurve : WeierstrassCurve EllipticRing

The universal elliptic Weierstrass curve: the universal curve base-changed to ℤ[A₁,⋯,A₆][Δ⁻¹], over which its discriminant (ellipticCurve_Δ) is a unit. Every elliptic Weierstrass curve is its base change along exactly one ring homomorphism (map_specializeElliptic, specializeElliptic_map_ellipticCurve).

Equations

• WeierstrassCurve.Universal.ellipticCurve = WeierstrassCurve.Universal.curve.baseChange WeierstrassCurve.Universal.EllipticRing

@[simp]

theorem WeierstrassCurve.Universal.ellipticCurve_Δ : ellipticCurve.Δ = (algebraMap (MvPolynomial Coeff ℤ) EllipticRing) (Δ curve)

The discriminant of ellipticCurve is the image of curve.Δ in ℤ[A₁,⋯,A₆][Δ⁻¹]. Rewrite with this in place of Mathlib's map_Δ, which simp and rw do not apply to ellipticCurve.Δ on their own, since neither unfolds baseChange.

instance WeierstrassCurve.Universal.instIsEllipticEllipticRingEllipticCurve : ellipticCurve.IsElliptic

The universal elliptic Weierstrass curve is an elliptic curve: its discriminant is the image of curve.Δ in the localisation away from curve.Δ, hence a unit.

theorem WeierstrassCurve.Universal.EllipticRing.ringHom_ext {S : Type u_1} [Semiring S] {f g : EllipticRing →+* S} (h : ∀ (i : Coeff), f ((algebraMap (MvPolynomial Coeff ℤ) EllipticRing) (MvPolynomial.X i)) = g ((algebraMap (MvPolynomial Coeff ℤ) EllipticRing) (MvPolynomial.X i))) : f = g

Extensionality for homomorphisms out of ℤ[A₁,⋯,A₆][Δ⁻¹]. Two ring homomorphisms out of Universal.EllipticRing are equal as soon as they agree on the images of the five indeterminates A₁,⋯,A₆ — the coefficients of ellipticCurve. So a homomorphism out of Universal.EllipticRing is determined by the Weierstrass curve it produces from ellipticCurve.

theorem WeierstrassCurve.Universal.EllipticRing.ringHom_ext_iff {S : Type u_1} [Semiring S] {f g : EllipticRing →+* S} : f = g ↔ ∀ (i : Coeff), f ((algebraMap (MvPolynomial Coeff ℤ) EllipticRing) (MvPolynomial.X i)) = g ((algebraMap (MvPolynomial Coeff ℤ) EllipticRing) (MvPolynomial.X i))

noncomputable def WeierstrassCurve.specializeElliptic {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : Universal.EllipticRing →+* R

The classifying homomorphism of an elliptic Weierstrass curve W over R: the ring homomorphism ℤ[A₁,⋯,A₆][Δ⁻¹] →+* R extending W.specialize, which substitutes the coefficients of W for the indeterminates (specializeElliptic_comp_algebraMap). The universal elliptic Weierstrass curve maps to W along it (map_specializeElliptic), and it is the only homomorphism with that property (specializeElliptic_map_ellipticCurve).

Equations

• W.specializeElliptic = IsLocalization.Away.lift (WeierstrassCurve.Δ WeierstrassCurve.Universal.curve) ⋯

@[simp]

theorem WeierstrassCurve.specializeElliptic_comp_algebraMap {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : W.specializeElliptic.comp (algebraMap (MvPolynomial Coeff ℤ) Universal.EllipticRing) = W.specialize

Restricted to the coefficient ring ℤ[A₁,⋯,A₆], the classifying homomorphism of W is W.specialize. Use this shape when composing ring maps and specializeElliptic_algebraMap when rewriting underneath an application.

@[simp]

theorem WeierstrassCurve.specializeElliptic_algebraMap {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] (p : MvPolynomial Coeff ℤ) : W.specializeElliptic ((algebraMap (MvPolynomial Coeff ℤ) Universal.EllipticRing) p) = W.specialize p

The classifying homomorphism of W sends the image of a polynomial p in the coefficients to W.specialize p; with specialize_X, it sends the image of each indeterminate to the corresponding coefficient of W. The pointwise form of specializeElliptic_comp_algebraMap.

@[simp]

theorem WeierstrassCurve.map_specializeElliptic {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] : Universal.ellipticCurve.map W.specializeElliptic = W

Every elliptic Weierstrass curve is the base change of the universal elliptic Weierstrass curve along its classifying homomorphism. An identity that is compatible with base change, proved once for Universal.ellipticCurve over the integral domain Universal.EllipticRing, thereby holds for every elliptic Weierstrass curve over every commutative ring. See map_specialize for Weierstrass curves that need not be elliptic.

@[simp]

theorem WeierstrassCurve.specializeElliptic_map_ellipticCurve {R : Type u_1} [CommRing R] (f : Universal.EllipticRing →+* R) : (Universal.ellipticCurve.map f).specializeElliptic = f

A ring homomorphism f out of ℤ[A₁,⋯,A₆][Δ⁻¹] is the classifying homomorphism of the Weierstrass curve ellipticCurve.map f it produces. With map_specializeElliptic, this makes f ↦ ellipticCurve.map f and W ↦ W.specializeElliptic mutually inverse: ring homomorphisms ℤ[A₁,⋯,A₆][Δ⁻¹] →+* R correspond exactly to elliptic Weierstrass curves over R.

theorem WeierstrassCurve.specializeElliptic_map {R : Type u_2} [CommRing R] (W : WeierstrassCurve R) [W.IsElliptic] {S : Type u_1} [CommRing S] (f : R →+* S) : (W.map f).specializeElliptic = f.comp W.specializeElliptic

The classifying homomorphism is natural in the base ring: the classifying homomorphism of the base change W.map f is that of W followed by f.

@[simp]

theorem WeierstrassCurve.specializeElliptic_ellipticCurve : Universal.ellipticCurve.specializeElliptic = RingHom.id Universal.EllipticRing

The universal elliptic Weierstrass curve is classified by the identity homomorphism of ℤ[A₁,⋯,A₆][Δ⁻¹].