Complements on Weierstrass curves

Facts about the invariants of an elliptic curve, complementing Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean:

• WeierstrassCurve.a₁_ne_zero_or_a₃_ne_zero_of_Δ_ne_zero_of_two_eq_zero: where 2 = 0, a curve with Δ ≠ 0 has a₁ ≠ 0 or a₃ ≠ 0;
• WeierstrassCurve.Δ_eq_of_c₄_eq_of_c₆_eq: two equations with the same c-invariants have the same discriminant, wherever 1728 is a regular element, by WeierstrassCurve.c_relation;
• WeierstrassCurve.j_eq_1728_iff: j = 1728 ↔ c₆ = 0, the analogue for j = 1728 of Mathlib's WeierstrassCurve.j_eq_zero_iff (j = 0 ↔ c₄ = 0), together with its unreduced companion WeierstrassCurve.j_eq_1728_iff' mirroring WeierstrassCurve.j_eq_zero_iff';
• WeierstrassCurve.baseChange_c₄_ne_zero and WeierstrassCurve.baseChange_c₆_ne_zero: the two corollaries of those criteria that say j ≠ 0 and j ≠ 1728 survive base change along an injection, in the c₄/c₆ form the automorphism criterion consumes.
• WeierstrassCurve.cusp: the cusp curve Y² = X³, its coefficient projections, and the point (1, 1) on it (WeierstrassCurve.equation_cusp_one_one). It depends on nothing beyond a Weierstrass equation, and is the specialization target TauCeti/AlgebraicGeometry/EllipticCurve/Universal.lean uses to retract the universal ring onto ℤ.

All are stated over a commutative ring, matching the generality of the Mathlib results they complement. The first two are consumed by the automorphism-group development in TauCeti/AlgebraicGeometry/EllipticCurve/Aut.lean, the Aut (E, O) milestone of TauCetiRoadmap/EllipticCurves/README.md §Layer 1; the base-change pair is consumed by the twist classification in TauCeti/AlgebraicGeometry/EllipticCurve/QuadraticTwist/Basic.lean, which needs Aut(Eᴸ) = {±1} after base change to a splitting field.

Adapted from the FLT project (ImperialCollegeLondon/FLT, FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean at the roadmap's pin bc2fe8ff7396 (FLT PR #1088), Apache 2.0, by Kevin Buzzard and Claude). Every result here except the cusp curve is adapted from that file, and all are generalised from FLT's field-level statements to a commutative ring: the two j-criteria, and the base-change pair baseChange_c₄_ne_zero / baseChange_c₆_ne_zero, which FLT states only for a field extension. The cusp curve is not from FLT: it came with the universal-curve port and is placed here because it needs no universal machinery.

theorem WeierstrassCurve.a₁_ne_zero_or_a₃_ne_zero_of_Δ_ne_zero_of_two_eq_zero {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) (hΔ : E.Δ ≠ 0) (h2 : 2 = 0) : E.a₁ ≠ 0 ∨ E.a₃ ≠ 0

Where 2 = 0, a curve with nonzero discriminant has a₁ ≠ 0 or a₃ ≠ 0: otherwise a₁ = a₃ = 0 makes the partial derivative ∂/∂y = 2y + a₁x + a₃ vanish identically, so Δ = 0.

theorem WeierstrassCurve.Δ_eq_of_c₄_eq_of_c₆_eq {R : Type u_1} [CommRing R] (h1728 : IsRegular 1728) {W W' : WeierstrassCurve R} (h₄ : W.c₄ = W'.c₄) (h₆ : W.c₆ = W'.c₆) : W.Δ = W'.Δ

The discriminant is determined by the c-invariants, wherever 1728 can be cancelled: WeierstrassCurve.c_relation pins 1728 * Δ down to c₄³ - c₆².

theorem WeierstrassCurve.j_eq_1728_iff' {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) [E.IsElliptic] : E.j = 1728 ↔ E.c₆ ^ 2 = 0

j(E) = 1728 if and only if c₆(E)² = 0, by the relation 1728·Δ = c₄³ - c₆². This is the analogue for j = 1728 of WeierstrassCurve.j_eq_zero_iff' (j = 0 ↔ c₄³ = 0).

theorem WeierstrassCurve.j_eq_1728_iff {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) [E.IsElliptic] [IsReduced R] : E.j = 1728 ↔ E.c₆ = 0

j(E) = 1728 if and only if c₆(E) = 0, by the relation 1728·Δ = c₄³ - c₆². This is the analogue for j = 1728 of WeierstrassCurve.j_eq_zero_iff (j = 0 ↔ c₄ = 0).

theorem WeierstrassCurve.baseChange_c₄_ne_zero {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) {A : Type u_2} [CommRing A] [Algebra R A] (hRA : Function.Injective ⇑(algebraMap R A)) (hc₄ : E.c₄ ≠ 0) : (E.baseChange A).c₄ ≠ 0

c₄ ≠ 0 survives base change along an injection, since c₄ of the base change is the image of c₄. Stated on c₄ rather than on j: nothing here needs [IsReduced R] or the j-criterion — nor even that E be elliptic — and a caller with j ≠ 0 gets the hypothesis from j_eq_zero_iff.

theorem WeierstrassCurve.baseChange_c₆_ne_zero {R : Type u_1} [CommRing R] (E : WeierstrassCurve R) {A : Type u_2} [CommRing A] [Algebra R A] (hRA : Function.Injective ⇑(algebraMap R A)) (hc₆ : E.c₆ ≠ 0) : (E.baseChange A).c₆ ≠ 0

c₆ ≠ 0 survives base change along an injection. The companion of baseChange_c₄_ne_zero; a caller with j ≠ 1728 gets the hypothesis from j_eq_1728_iff.

The cusp curve

def WeierstrassCurve.cusp (R : Type u_2) [Zero R] : Affine R

The cusp curve Y² = X³ over a commutative ring R.

Equations

• WeierstrassCurve.cusp R = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 0, a₆ := 0 }

@[simp]

theorem WeierstrassCurve.cusp_a₁ (R : Type u_2) [Zero R] : (cusp R).a₁ = 0

Every coefficient of the cusp curve vanishes, and likewise for cusp_a₂ through cusp_a₆. The definition body is unexposed, so these are how a consumer projects out of cusp — for instance when specialising the universal curve along it.

@[simp]

theorem WeierstrassCurve.cusp_a₂ (R : Type u_2) [Zero R] : (cusp R).a₂ = 0

The a₂ coefficient of the cusp curve vanishes.

@[simp]

theorem WeierstrassCurve.cusp_a₃ (R : Type u_2) [Zero R] : (cusp R).a₃ = 0

The a₃ coefficient of the cusp curve vanishes.

@[simp]

theorem WeierstrassCurve.cusp_a₄ (R : Type u_2) [Zero R] : (cusp R).a₄ = 0

The a₄ coefficient of the cusp curve vanishes.

@[simp]

theorem WeierstrassCurve.cusp_a₆ (R : Type u_2) [Zero R] : (cusp R).a₆ = 0

The a₆ coefficient of the cusp curve vanishes.

theorem WeierstrassCurve.equation_cusp_one_one (R : Type u_2) [CommRing R] : (cusp R).Equation 1 1

(1, 1) lies on the cusp curve Y² = X³, over any commutative ring.

The case R = ℤ is the one the universal curve uses: specializing along that point is the cheap route to nonvanishing statements, since ψₙ(1,1) = n, so a universal quantity that vanished would have to vanish in ℤ. The CharZero Universal.Ring instance in TauCeti/AlgebraicGeometry/EllipticCurve/Universal.lean is obtained that way.