feat(EllipticCurve): the universal elliptic curve

[alreadydone]

• Define 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 the universal ring ℤ[A₁,A₂,A₃,A₄,A₆,X,Y]/⟨P⟩ = Universal.Poly/⟨P⟩ (Universal.Ring, where P is the Weierstrass polynomial) with distinguished point (X,Y).

• Given a Weierstrass curve W over a commutative ring R, we define the specialization homomorphism W.specialize : ℤ[A₁,A₂,A₃,A₄,A₆] →+* R. If (x,y) is a point on the affine plane, we define W.polyEval x y : Universal.Poly →+* R, which factors through W.ringEval x y : Universal.Ring →+* R if (x,y) is on W.

• Introduce the cusp curve Y² = X³, on which lies the rational point (1,1), with the nice property that ψₙ(1,1) = n, making it easy to prove nonvanishing of the universal ψₙ when n ≠ 0 by specializing to the cusp curve, which shows that (X,Y) is a point of infinite order on the universal pointed elliptic curve.

---

• depends on: [Merged by Bors] - feat(EllipticCurve): affine formulas and bivariate polynomial lemmas #13845
• depends on: [Merged by Bors] - feat(EllipticCurve): a coordinate ring over a domain is a domain #12883

[github-actions]

PR summary 44f983a8fa

Import changes

No significant changes to the import graph

---

Declarations diff

+ Affine.point
+ Coeff
+ Equation.map
+ Field.two_ne_zero
+ Jacobian.point
+ Poly.two_ne_zero
+ Y_sub_negPolynomial
+ Y_sub_polynomialY
+ addX_eq_subX_sub
+ addY_sub_negY
+ algebraMap_field_eq_comp
+ algebraMap_field_injective
+ algebraMap_injective
+ algebraMap_injective'
+ algebraMap_ring_eq_comp
+ baseChange_polynomialX_eval_eval
+ baseChange_polynomialY_eval_eval
+ baseChange_polynomial_eval_eval
+ coe_algebraMap_eq_CC
+ coe_evalEvalRingHom
+ curve
+ curveField_eq
+ curveRing_map_ringEval
+ cusp
+ cusp_equation_one_one
+ cyclic_sum_Y_mul_X_sub_X
+ equation_point
+ eval_C_X_comp_eval₂_map_C_X
+ eval_C_X_eval₂_map_C_X
+ eval₂RingHom_eval₂RingHom
+ eval₂_eval₂RingHom_apply
+ instance : Algebra R W.CoordinateRing
+ instance : Algebra R[X] W.CoordinateRing
+ instance : CommRing Poly := Polynomial.commRing /- why is this not automatic ... -/
+ instance : IsScalarTower R R[X] W.CoordinateRing
+ instance [IsDomain R] : IsDomain W.CoordinateRing
+ instance [Subsingleton R] : Subsingleton W.CoordinateRing
+ map
+ map_injective
+ map_mk
+ map_polynomialX_eval_eval
+ map_polynomialY_eval_eval
+ map_polynomial_eval
+ map_polynomial_evalEval
+ map_polynomial_eval_eval
+ map_smul
+ map_specialize
+ pointedCurve
+ pointedCurve_a₁
+ pointedCurve_a₂
+ pointedCurve_a₃
+ pointedCurve_a₄
+ pointedCurve_a₆
+ polyEval
+ polyEval_apply
+ polyEval_comp_eq_specialize
+ polyToField
+ polyToField_apply
+ polyToField_polynomial
+ ringEval
+ ringEval_comp_eq_specialize
+ ringEval_comp_mk
+ ringEval_mk
+ some_eq_some_iff
+ some_ne_zero
+ specialize
+ Δ_curve_ne_zero
- baseChange_eval_polynomial
- baseChange_eval_polynomialX
- baseChange_eval_polynomialY
- instAlgebraCoordinateRing
- instAlgebraCoordinateRing'
- instIsDomainCoordinateRing
- instIsDomainCoordinateRing_of_Field
- instIsScalarTowerCoordinateRing
- instSubsingletonCoordinateRing
- map_eval_polynomial
- map_eval_polynomialX
- map_eval_polynomialY

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[Multramate]

Thanks! I think I said somewhere (but I've lost it!) that I intend to combine stuff from this file with all the stuff to do with the coordinate ring, because I would think that these are "universal constructions" for any Weierstrass curve. I haven't had the time to do it so far, but can you give me some time to think about it? I'll make a subbranch (hopefully I don't mess it up again!).

[alreadydone]

Thanks! I think I said somewhere (but I've lost it!) that I intend to combine stuff from this file with all the stuff to do with the coordinate ring, because I would think that these are "universal constructions" for any Weierstrass curve. I haven't had the time to do it so far, but can you give me some time to think about it? I'll make a subbranch (hopefully I don't mess it up again!).

I think you said it here. Yes I agree that for a Weierstrass curve W over comm. ring R you can define a "universal" Weierstrass curve over the coordinate ring R[W] with a distinguished point (X,Y) on it, such that every point (x,y) on W is the specialization of the distinguished point under the ring homomorphism R[W]->R sending X to x and Y to y. As I remarked here, you can almost prove the ZSMul formula using this less universal ring, but it would not be so easy to show ψₙ ≠ 0 when n ≠ 0 if the characteristic divides n, and in char 2 there's an additional issue.

I'll try to refactor my code with generalized definitions, thanks for mentioning this!

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(EllipticCurve): affine formulas and bivariate polynomial lemmas #13845
• [Merged by Bors] - feat(EllipticCurve): a coordinate ring over a domain is a domain #12883
  By Dependent Issues (🤖). Happy coding!