noncomputable def EllipticCurveSmooth.shortWeierstrass {k : Type u_1} [Field k] (a b : k) : WeierstrassCurve k

The short Weierstrass curve y² = x³ + a x + b packaged as a WeierstrassCurve.

noncomputable def EllipticCurveSmooth.weierstrass {k : Type u_1} [Field k] (a b : k) : Polynomial (Polynomial k)

The bivariate Weierstrass polynomial Y² − (X³ + aX + b), viewed in k[X][Y].

theorem EllipticCurveSmooth.weierstrass_eq_polynomial {k : Type u_1} [Field k] (a b : k) : weierstrass a b = (shortWeierstrass a b).toAffine.polynomial

Our hand-written Weierstrass polynomial agrees with the mathlib affine defining polynomial.

theorem EllipticCurveSmooth.weierstrass_monic {k : Type u_1} [Field k] (a b : k) : (weierstrass a b).Monic

The Weierstrass polynomial is monic of degree two in Y.

theorem EllipticCurveSmooth.weierstrass_natDegree {k : Type u_1} [Field k] (a b : k) : (weierstrass a b).natDegree = 2

The Weierstrass polynomial has Y-degree exactly two.

theorem EllipticCurveSmooth.weierstrass_no_root {k : Type u_1} [Field k] (a b : k) (g : Polynomial k) : ¬(weierstrass a b).IsRoot g

No polynomial in X can be a root of the Weierstrass polynomial, by degree-counting: X³ + aX + b has odd degree and so is not a square.

theorem EllipticCurveSmooth.weierstrass_irreducible {k : Type u_1} [Field k] (a b : k) : Irreducible (weierstrass a b)

The Weierstrass polynomial is irreducible in k[X][Y], hence the cubic defines an integral plane curve.

theorem EllipticCurveSmooth.weierstrass_irreducible_via_mathlib {k : Type u_1} [Field k] (a b : k) : Irreducible (weierstrass a b)

Alternative proof of irreducibility, via the mathlib affine Weierstrass API.

instance EllipticCurveSmooth.weierstrass_coordinate_ring_isDomain {k : Type u_1} [Field k] (a b : k) : IsDomain (AdjoinRoot (weierstrass a b))

The coordinate ring k[X][Y]/(Y² − X³ − aX − b) of the affine Weierstrass curve is an integral domain.

noncomputable def EllipticCurveSmooth.coordinateRingEquiv {k : Type u_1} [Field k] (a b : k) : AdjoinRoot (weierstrass a b) ≃+* AdjoinRoot (shortWeierstrass a b).toAffine.polynomial

Ring equivalence between our coordinate ring and the mathlib affine coordinate ring, transporting via weierstrass_eq_polynomial.

theorem EllipticCurveSmooth.shortWeierstrass_disc {k : Type u_1} [Field k] (a b : k) : (shortWeierstrass a b).Δ = -16 * (4 * a ^ 3 + 27 * b ^ 2)

Discriminant of the short Weierstrass curve: Δ = −16·(4a³ + 27b²).

theorem EllipticCurveSmooth.shortWeierstrass_disc_ne_zero {k : Type u_1} [Field k] (a b : k) (hchar2 : 2 ≠ 0) (hdisc : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0) : (shortWeierstrass a b).Δ ≠ 0

In characteristic ≠ 2, the discriminant is non-zero iff 4a³ + 27b² ≠ 0.

theorem EllipticCurveSmooth.shortWeierstrass_equation_iff {k : Type u_1} [Field k] (a b x₀ y₀ : k) : (shortWeierstrass a b).toAffine.Equation x₀ y₀ ↔ y₀ ^ 2 = x₀ ^ 3 + a * x₀ + b

A point (x₀, y₀) lies on the short Weierstrass curve iff y₀² = x₀³ + a x₀ + b.

theorem EllipticCurveSmooth.weierstrass_jacobian_smooth {k : Type u_1} [Field k] (a b : k) (hchar2 : 2 ≠ 0) (hdisc : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0) (x₀ y₀ : k) (hcurve : y₀ ^ 2 = x₀ ^ 3 + a * x₀ + b) : ¬(2 * y₀ = 0 ∧ 3 * x₀ ^ 2 + a = 0)

Smoothness via the Jacobian criterion: at any point on the curve, the two partial derivatives 2y and 3x² + a cannot vanish simultaneously when the discriminant is non-zero.

theorem EllipticCurveSmooth.weierstrass_smooth_at_point {k : Type u_1} [Field k] (a b : k) (hchar2 : 2 ≠ 0) (hdisc : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0) (x₀ y₀ : k) (hcurve : y₀ ^ 2 = x₀ ^ 3 + a * x₀ + b) : 2 * y₀ ≠ 0 ∨ 3 * x₀ ^ 2 + a ≠ 0

Equivalent formulation of the Jacobian smoothness criterion: at any curve point, at least one of the two partial derivatives is non-zero.

theorem EllipticCurveSmooth.shortWeierstrass_nonsingular {k : Type u_1} [Field k] (a b : k) (hchar2 : 2 ≠ 0) (hdisc : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0) (x₀ y₀ : k) (hcurve : y₀ ^ 2 = x₀ ^ 3 + a * x₀ + b) : (shortWeierstrass a b).toAffine.Nonsingular x₀ y₀

Smoothness of the elliptic curve: every point on the short Weierstrass curve is nonsingular when Δ ≠ 0 (i.e. char k ≠ 2 and 4a³ + 27b² ≠ 0).

theorem EllipticCurveSmooth.shortWeierstrass_nonsingular_iff {k : Type u_1} [Field k] (a b x₀ y₀ : k) : (shortWeierstrass a b).toAffine.Nonsingular x₀ y₀ ↔ (shortWeierstrass a b).toAffine.Equation x₀ y₀ ∧ (-(3 * x₀ ^ 2 + a) ≠ 0 ∨ 2 * y₀ ≠ 0)

Characterization of nonsingularity in terms of the defining equation and the explicit Jacobian non-vanishing condition.