Base change of affine elliptic curves

Mathlib carries ellipticity through WeierstrassCurve.map. This module exposes the same instance for the canonical affine base-change spelling W⁄A, so consumers of the point and function-field base-change APIs do not have to unfold that abbreviation. It also records that base change along the identity algebra map returns the original curve, together with the resulting identification WeierstrassCurve.Affine.Point.equivBaseChangeSelf of the point groups of W and W⁄F, and a coordinate descent lemma for points whose abscissa is already rational.

This is infrastructure for the base-change lane of TauCetiRoadmap/EllipticCurves/README.md, Layer 0.5.

@[simp]

theorem WeierstrassCurve.Affine.baseChange_self {R : Type u_1} [CommRing R] (W : Affine R) : toAffine (W.baseChange R) = W

Base changing along the identity algebra map returns the curve itself. Stated over a commutative ring: it is a formal map identity and uses nothing about R beyond its ring structure.

noncomputable def WeierstrassCurve.Affine.Point.equivBaseChangeSelf {F : Type u_1} [Field F] [DecidableEq F] (W : Affine F) : W.Point ≃+ (toAffine (W.baseChange F)).Point

The points of W are the points of its base change along the identity: the transport of the point group along baseChange_self. Point-group facts stated for W⁄F, the form base-change statements produce, are read on W itself through it.

Equations

• WeierstrassCurve.Affine.Point.equivBaseChangeSelf W = AddEquiv.cast ⋯

@[simp]

theorem WeierstrassCurve.Affine.Point.equivBaseChangeSelf_some {F : Type u_1} [Field F] [DecidableEq F] (W : Affine F) {x y : F} (h : W.Nonsingular x y) : (equivBaseChangeSelf W) (some x y h) = some x y ⋯

equivBaseChangeSelf keeps the coordinates of an affine point.

theorem WeierstrassCurve.mem_range_y_of_equation_of_mem_range_x_of_exists_point {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [NoZeroDivisors A] [Algebra R A] (W : WeierstrassCurve R) {x y : A} (heq : (W.baseChange A).toAffine.Equation x y) {x₀ : R} (hx : (algebraMap R A) x₀ = x) (hex : ∃ (y₀ : R), W.toAffine.Equation x₀ y₀) : y ∈ Set.range ⇑(algebraMap R A)

The y-coordinate of a point with rational x is rational whenever the Weierstrass equation at that x has one rational solution: the two roots of the resulting monic quadratic sum to minus its linear coefficient, so the other one is rational as well.

instance WeierstrassCurve.Affine.instIsEllipticBaseChange {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {W : Affine R} [WeierstrassCurve.IsElliptic W] : WeierstrassCurve.IsElliptic (WeierstrassCurve.baseChange W A).toAffine

Base change preserves ellipticity, in the (W⁄A).toAffine spelling used by the affine point API.