The node polynomial of a Weierstrass curve

For a nodal Weierstrass curve, the node polynomial is the quadratic c₄ T² + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄). Its splitting over the residue field distinguishes split from nonsplit multiplicative reduction.

This file defines WeierstrassCurve.nodePolynomial over a commutative ring and proves:

• its discriminant is -c₄ c₆;
• for a model singular at the origin, it is c₄ times the tangent quadratic T² + a₁ T - a₂;
• it commutes with base change;
• a change of variables (u, r, s, t) acts by the substitution T ↦ u T + s and the scalar u⁻⁶, preserving splitting over a field;
• after mapping to a field where c₄ remains nonzero, splitting is equivalent to the discriminant being a square in characteristic different from two, and to an Artin–Schreier condition in characteristic two.

These criteria apply to any ring homomorphism to a field. Their relation to WeierstrassCurve.HasSplitMultiplicativeReduction is developed in MinimalModel/Basic.lean and LocalPolynomial.lean. The constant-coefficient formula also describes the effect of quadratic twisting in QuadraticTwist/Basic.lean.

Adapted from the FLT project (ImperialCollegeLondon/FLT, commit bc2fe8ff7396, FLT PR #1088, Apache 2.0): the node-polynomial block of FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean (authors Kevin Buzzard, William Coram, Claude), and splitPolynomial_discrim from FLT/Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean (authors Kevin Buzzard, Claude).

noncomputable def WeierstrassCurve.nodePolynomial {A : Type u_1} [CommRing A] (W : WeierstrassCurve A) : Polynomial A

The node polynomial c₄ T² + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄), whose roots are the slopes of the two tangent directions at the node of a multiplicative reduction. This is the polynomial Mathlib writes out inline in WeierstrassCurve.HasSplitMultiplicativeReduction, which asks for the splitting over the residue field of this polynomial formed from the integral model W.integralModel R, as its one extra condition on top of HasMultiplicativeReduction.

Equations

• W.nodePolynomial = Polynomial.C W.c₄ * Polynomial.X ^ 2 + Polynomial.C (W.a₁ * W.c₄) * Polynomial.X - Polynomial.C (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)

theorem WeierstrassCurve.nodePolynomial_def {A : Type u_1} [CommRing A] (W : WeierstrassCurve A) : W.nodePolynomial = Polynomial.C W.c₄ * Polynomial.X ^ 2 + Polynomial.C (W.a₁ * W.c₄) * Polynomial.X - Polynomial.C (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)

The defining formula for the node polynomial. The definition's body is not exposed across the module boundary, so this is how downstream modules see it; nodePolynomial_map_eq_quadratic is the corresponding statement for its image under a ring homomorphism.

theorem WeierstrassCurve.nodePolynomial_coeff_zero {A : Type u_1} [CommRing A] (W : WeierstrassCurve A) : W.nodePolynomial.coeff 0 = -(54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)

The constant coefficient of the node polynomial. Note the sign: nodePolynomial subtracts 54 b₆ - 3 b₂ b₄ + a₂ c₄, so coeff 0 is minus that combination, not it.

Deliberately not @[simp]: the normal form wanted downstream rewrites a twisted curve's coefficient back to the base curve's (nodePolynomial_coeff_zero_quadraticTwistOf), and that lemma's left-hand side is exactly this one's, so tagging both would make the twist lemma non-normal-form.

theorem WeierstrassCurve.nodePolynomial_eq_C_mul {A : Type u_1} [CommRing A] (W : WeierstrassCurve A) {n : A} (hn : W.c₄ * n = W.nodePolynomial.coeff 0) : W.nodePolynomial = Polynomial.C W.c₄ * (Polynomial.X ^ 2 + Polynomial.C W.a₁ * Polynomial.X + Polynomial.C n)

The node polynomial as c₄ times a monic quadratic. If c₄ n is the constant coefficient of the node polynomial, the node polynomial is c₄ · (T² + a₁ T + n). When c₄ is a unit such an n exists and is unique. This is a purely algebraic factorization; when the reduction of a minimal model is multiplicative, the roots of the reduced quadratic T² + a₁ T + n are the slopes of the two tangent directions at the node of the reduced curve.

theorem WeierstrassCurve.nodePolynomial_eq_of_isSingular_zero {A : Type u_1} [CommRing A] (W : WeierstrassCurve A) (h : W.toAffine.IsSingular 0 0) : W.nodePolynomial = Polynomial.C W.c₄ * (Polynomial.C 1 * Polynomial.X ^ 2 + Polynomial.C W.a₁ * Polynomial.X + Polynomial.C (-W.a₂))

For a model singular at the origin, the node polynomial is c₄ times the tangent quadratic T² + a₁ T - a₂, written in the coefficient form used by the quadratic polynomial API.

theorem WeierstrassCurve.discrim_nodePolynomial {A : Type u_1} [CommRing A] (W : WeierstrassCurve A) : discrim W.c₄ (W.a₁ * W.c₄) (-(54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)) = -(W.c₄ * W.c₆)

The discriminant of the node polynomial is -c₄ c₆. Hence — away from residue characteristic two, and provided c₄ survives the reduction — the tangent directions at the node are rational over the residue field exactly when the image of -c₄ c₆ is a square there (splits_nodePolynomial_map_iff_isSquare); twisting by (t, n) multiplies -c₄ c₆ by (t² - 4n)⁵ = (t² - 4n)⁴ · (t² - 4n), i.e. by the twisting parameter up to a square.

@[simp]

theorem WeierstrassCurve.map_nodePolynomial {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] (φ : A →+* B) (W : WeierstrassCurve A) : (W.map φ).nodePolynomial = Polynomial.map φ W.nodePolynomial

The node polynomial is natural in the coefficient ring: it commutes with base change of the Weierstrass equation along any ring homomorphism.

theorem WeierstrassCurve.nodePolynomial_map_eq_quadratic {A : Type u_1} [CommRing A] {B : Type u_4} [Ring B] (φ : A →+* B) (W : WeierstrassCurve A) : Polynomial.map φ W.nodePolynomial = Polynomial.C (φ W.c₄) * Polynomial.X ^ 2 + Polynomial.C (φ (W.a₁ * W.c₄)) * Polynomial.X + Polynomial.C (-φ (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄))

The reduced node polynomial, presented as a quadratic with an additive constant term — the shape C a * X ^ 2 + C b * X + C c that the criteria of TauCeti/Algebra/Polynomial/QuadraticDiscriminant.lean consume.

theorem WeierstrassCurve.discrim_map_nodePolynomial {A : Type u_1} [CommRing A] {B : Type u_4} [Ring B] (φ : A →+* B) (W : WeierstrassCurve A) : discrim (φ W.c₄) (φ (W.a₁ * W.c₄)) (-φ (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)) = φ (-(W.c₄ * W.c₆))

The image of discrim_nodePolynomial under a ring homomorphism, in the shape produced by the quadratic criteria applied to nodePolynomial_map_eq_quadratic.

theorem WeierstrassCurve.variableChange_nodePolynomial {A : Type u_1} [CommRing A] (W : WeierstrassCurve A) (C : VariableChange A) : (C • W).nodePolynomial = Polynomial.C (↑C.u⁻¹ ^ 6) * W.nodePolynomial.comp (Polynomial.C ↑C.u * Polynomial.X + Polynomial.C C.s)

Under a change of variables C = (u, r, s, t), the node polynomial transforms by the affine substitution T ↦ u T + s and the unit scalar u⁻⁶ — reflecting that the tangent slopes λ transform as λ ↦ (λ - s)/u. Over a field this makes splitting invariant; see splits_variableChange_nodePolynomial_map_iff.

theorem WeierstrassCurve.splits_variableChange_nodePolynomial_map_iff {A : Type u_1} [CommRing A] {k : Type u_3} [Field k] (φ : A →+* k) (W : WeierstrassCurve A) (C : VariableChange A) : (Polynomial.map φ (C • W).nodePolynomial).Splits ↔ (Polynomial.map φ W.nodePolynomial).Splits

Invariance of the node polynomial's splitting under change of variables. Since a change of variables transforms the node polynomial by an affine substitution and a unit scalar (variableChange_nodePolynomial), whether it splits over a field k is unchanged. This is what makes split multiplicative reduction an isomorphism invariant rather than a property of the equation.

theorem WeierstrassCurve.splits_nodePolynomial_map_iff_isSquare {A : Type u_1} [CommRing A] {k : Type u_3} [Field k] [NeZero 2] (φ : A →+* k) (W : WeierstrassCurve A) (hc₄ : φ W.c₄ ≠ 0) : (Polynomial.map φ W.nodePolynomial).Splits ↔ IsSquare (φ (-(W.c₄ * W.c₆)))

Split criterion away from residue characteristic two. Over a field k with 2 ≠ 0, and provided c₄ does not die under φ — the condition that makes the reduced polynomial genuinely quadratic, and which multiplicative reduction supplies — the node polynomial splits, i.e. the two tangent directions at the node are k-rational, exactly when φ (-(c₄ * c₆)), the image of its discriminant (discrim_nodePolynomial), is a square in k. Applied to a quadratic twist via -c₄' c₆' = (t² - 4n)⁵ · (-c₄ c₆), this criterion identifies the square class of twists that turns nonsplit reduction into split reduction.

theorem WeierstrassCurve.splits_nodePolynomial_map_iff_exists_artinSchreier_of_two_eq_zero {A : Type u_1} [CommRing A] {k : Type u_3} [Field k] (h2 : 2 = 0) (φ : A →+* k) (W : WeierstrassCurve A) (hc₄ : φ W.c₄ ≠ 0) : (Polynomial.map φ W.nodePolynomial).Splits ↔ ∃ (z : k), φ (W.a₁ * W.c₄) ^ 2 * (z ^ 2 + z) = φ W.c₄ * -φ (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)

Split criterion in residue characteristic two. Over a field k of characteristic 2, where the square-class criterion splits_nodePolynomial_map_iff_isSquare says nothing, the node polynomial splits exactly when its Artin-Schreier invariant lies in the image of z ↦ z² + z. Only c₄ need be assumed nonzero: in characteristic two c₄ = a₁⁴, so the linear coefficient a₁ c₄ is also nonzero.