Evaluating the coordinate ring of a Weierstrass curve at a point

The coordinate ring R[W] of an affine Weierstrass curve W is AdjoinRoot W.polynomial, so at a point (x, y) satisfying the Weierstrass equation the evaluation map Polynomial.evalEval x y factors through it, by Mathlib's AdjoinRoot.evalEval. The same holds one level up: a point with coordinates in an R-algebra A — that is, a solution of the equation of the base change W⁄A — gives an R-algebra homomorphism R[W] →ₐ[R] A, and conversely every such homomorphism is evaluation at the images of the two coordinate functions, which therefore solve that equation. These statements concern the affine model WeierstrassCurve.Affine R itself, not a global WeierstrassCurve R.

Main definitions

• WeierstrassCurve.Affine.CoordinateRing.evalAlgHom: evaluation of the coordinate ring at a point of W⁄A, an R-algebra homomorphism into A.

Main results

• WeierstrassCurve.evalEval_eq_of_mk_eq: bivariate polynomials that are equal in the coordinate ring evaluate equally at a point of the curve.
• WeierstrassCurve.Affine.CoordinateRing.algHom_mk_eq_evalEval: an algebra homomorphism out of the coordinate ring is evaluation at the images of the coordinate functions, and WeierstrassCurve.Affine.CoordinateRing.equation_of_algHom says that those images satisfy the Weierstrass equation of the base change.
• WeierstrassCurve.Affine.CoordinateRing.algHom_ext: two algebra homomorphisms out of the coordinate ring that agree on the two coordinate functions are equal.
• WeierstrassCurve.Affine.CoordinateRing.algHom_injective: over a field, an algebra homomorphism out of the coordinate ring under which x stays transcendental is injective. This is the nonconstancy criterion the isogeny development already used for pullbacks (TauCeti.Isogeny.pullback_injective, which is now this lemma applied to a pullback), stated once for an arbitrary algebra homomorphism.

Everything but the last result is stated over an arbitrary commutative base ring; the curve need not be elliptic, and R need not be a domain, since the statement is exactly the factorisation and nothing more. Neither algHom_ext nor algHom_injective needs the target algebra to be commutative: the first says R[W] is generated by its two coordinate functions, and the second argues with a norm taken in R[W]; its one condition on the target side is that the image of the coordinate x be transcendental. algHom_mk_eq_evalEval evaluates a bivariate polynomial in the target, so it needs a commutative semiring there, and the results naming the base-changed curve W⁄A need a commutative ring, for W⁄A to be a Weierstrass curve over A. algHom_injective needs the base to be a field, because that norm needs the rank-two basis of R[W] over R[X].

These are what lets the division-polynomial identities, which Mathlib states in the coordinate ring, be consumed at points of the curve. In the converse direction they recover a solution of the Weierstrass equation from a residue degree-one ideal, which is the dictionary between points and places, and evalAlgHom together with algHom_injective is what the translations τ_P are built from: the pullback of τ_P is evaluation at a translate of the generic point.

theorem WeierstrassCurve.evalEval_eq_of_mk_eq {R : Type u_1} [CommRing R] (W : Affine R) {x y : R} (h : W.Equation x y) {p q : Polynomial (Polynomial R)} (hpq : (Affine.CoordinateRing.mk W) p = (Affine.CoordinateRing.mk W) q) : Polynomial.evalEval x y p = Polynomial.evalEval x y q

Bivariate polynomials that are equal in the coordinate ring R[W] evaluate equally at a point (x, y) of W.

theorem WeierstrassCurve.Affine.CoordinateRing.algHom_ext {R : Type u_1} [CommRing R] {A : Type u_2} [Semiring A] [Algebra R A] {W : Affine R} {f g : W.CoordinateRing →ₐ[R] A} (hX : f ((AdjoinRoot.of W.polynomial) Polynomial.X) = g ((AdjoinRoot.of W.polynomial) Polynomial.X)) (hY : f (AdjoinRoot.root W.polynomial) = g (AdjoinRoot.root W.polynomial)) : f = g

Two algebra homomorphisms out of the coordinate ring agreeing on the two coordinate functions are equal: the coordinate ring is generated by them.

This is a statement about the source: R[W] is generated over R by the two coordinate functions, so the target carries no commutativity hypothesis.

theorem WeierstrassCurve.Affine.CoordinateRing.algHom_ext_iff {R : Type u_1} [CommRing R] {A : Type u_2} [Semiring A] [Algebra R A] {W : Affine R} {f g : W.CoordinateRing →ₐ[R] A} : f = g ↔ f ((AdjoinRoot.of W.polynomial) Polynomial.X) = g ((AdjoinRoot.of W.polynomial) Polynomial.X) ∧ f (AdjoinRoot.root W.polynomial) = g (AdjoinRoot.root W.polynomial)

theorem WeierstrassCurve.Affine.CoordinateRing.algHom_mk_eq_evalEval {R : Type u_1} [CommRing R] {A : Type u_2} [CommSemiring A] [Algebra R A] {W : Affine R} (f : W.CoordinateRing →ₐ[R] A) (p : Polynomial (Polynomial R)) : f ((mk W) p) = Polynomial.evalEval (f ((AdjoinRoot.of W.polynomial) Polynomial.X)) (f (AdjoinRoot.root W.polynomial)) (Polynomial.map (Polynomial.mapRingHom (algebraMap R A)) p)

An algebra homomorphism out of the coordinate ring is evaluation at the images of the two coordinate functions, the coefficients of the polynomial being carried into the target algebra first.

theorem WeierstrassCurve.Affine.CoordinateRing.equation_of_algHom {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {W : Affine R} (f : W.CoordinateRing →ₐ[R] A) : (toAffine (W.baseChange A)).Equation (f ((AdjoinRoot.of W.polynomial) Polynomial.X)) (f (AdjoinRoot.root W.polynomial))

The images of the coordinate functions under an algebra homomorphism out of the coordinate ring satisfy the Weierstrass equation of the base-changed curve.

noncomputable def WeierstrassCurve.Affine.CoordinateRing.evalAlgHom {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {W : Affine R} {x y : A} (h : (toAffine (W.baseChange A)).Equation x y) : W.CoordinateRing →ₐ[R] A

Evaluation of the coordinate ring at a point of the base-changed curve. A solution (x, y) of the Weierstrass equation of W⁄A is a point of W with coordinates in A, and substituting it into a polynomial function factors through the coordinate ring.

Equations

• WeierstrassCurve.Affine.CoordinateRing.evalAlgHom h = AdjoinRoot.liftAlgHom W.polynomial (Polynomial.aeval x) y ⋯

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.evalAlgHom_mk {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {W : Affine R} {x y : A} (h : (toAffine (W.baseChange A)).Equation x y) (p : Polynomial (Polynomial R)) : (evalAlgHom h) ((mk W) p) = Polynomial.evalEval x y (Polynomial.map (Polynomial.mapRingHom (algebraMap R A)) p)

Evaluating the class of a polynomial in the coordinate ring is mapped polynomial evaluation at the given solution of the Weierstrass equation.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.evalAlgHom_of_X {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {W : Affine R} {x y : A} (h : (toAffine (W.baseChange A)).Equation x y) : (evalAlgHom h) ((AdjoinRoot.of W.polynomial) Polynomial.X) = x

Evaluation sends the coordinate-ring class of X to the first coordinate x.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.evalAlgHom_root {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {W : Affine R} {x y : A} (h : (toAffine (W.baseChange A)).Equation x y) : (evalAlgHom h) (AdjoinRoot.root W.polynomial) = y

Evaluation sends the coordinate-ring class of Y to the second coordinate y.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.evalAlgHom_equation_ofAlgHom {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {W : Affine R} (f : W.CoordinateRing →ₐ[R] A) : evalAlgHom ⋯ = f

Constructing a homomorphism from the equation satisfied by its coordinates recovers the original homomorphism.

theorem WeierstrassCurve.Affine.CoordinateRing.algHom_injective {F : Type u_3} [Field F] {W : Affine F} {A : Type u_4} [Ring A] [Algebra F A] (f : W.CoordinateRing →ₐ[F] A) (hx : Transcendental F (f ((mk W) (Polynomial.C Polynomial.X)))) : Function.Injective ⇑f

An algebra homomorphism out of the coordinate ring under which the coordinate x stays transcendental is injective. A nonzero element of the kernel has nonzero norm over F[x], and that norm is a polynomial relation killing the image of x.

Over a field the coordinate ring is free of rank two over F[X], which is what makes the norm available; neither ellipticity nor commutativity of A is needed.