A quadratic twist splits a nonsplit multiplicative reduction

Let R be a discrete valuation ring with fraction field K and let E be an elliptic curve over K, given by a minimal equation with multiplicative reduction. The node of the reduced curve has two tangent directions, the roots of the node polynomial c₄ T² + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄), and the reduction is split when they are rational over the residue field. This file proves that a separable quadratic twist makes the reduction split, in every characteristic of K and of the residue field.

The twist is explicit. Since c₄ is a unit, the node polynomial is c₄ · (T² + a₁ T + n) with n = coeff₀ / c₄ integral (nodePolynomial_eq_C_mul), and the twist to take is the one by (t, n) = (-a₁, n), the trace and norm of a root θ of T² + a₁ T + n. The node polynomial of that twist is D² c₄ · (T - (a₁² - 2n)) · (T - 2n) with D = a₁² - 4n (nodePolynomial_quadraticTwistOf_neg_a₁), so its roots lie in R. As c₄ D = -c₆ and both c₄ and c₆ are units at a multiplicative reduction, D is a unit: the twisted equation is integral with unit c₄, hence minimal, its discriminant D⁶ Δ has the valuation of Δ, and its node polynomial splits over the residue field (hasSplitMultiplicativeReduction_quadraticTwistOf).

When the reduction of E is nonsplit, T² + a₁ T + n has no root in the residue field, hence, R being integrally closed, none in K. So L = K[T] / (T² + a₁ T + n) is a quadratic field extension, separable because D ≠ 0. The twist E.quadraticTwist L agrees with the explicit twist up to a change of variables over K, and split multiplicative reduction transfers between minimal models related by a change of variables (exists_quadraticTwist_hasSplitMultiplicativeReduction).

Away from residue characteristic two, splitting is the condition that -c₆ be a square in the residue field, and the classical choice of twist is by K(√-c₆). Twisting by the node quadratic itself removes the restriction on the characteristic.

Main results

• WeierstrassCurve.hasSplitMultiplicativeReduction_quadraticTwistOf: the explicit twist by (-a₁, coeff₀ / c₄) of a curve with multiplicative reduction has split multiplicative reduction.
• WeierstrassCurve.exists_quadraticTwist_hasSplitMultiplicativeReduction: a curve with nonsplit multiplicative reduction acquires split multiplicative reduction after a separable quadratic twist.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.5 and X.2.

Provenance

The statement of exists_quadraticTwist_hasSplitMultiplicativeReduction is the headline of the FLT project's PR #1088, "Quadratic twist to split multiplicative reduction" (ImperialCollegeLondon/FLT @ bc2fe8ff7396, Apache-2.0, by Kevin Buzzard), from which the minimal-model and node-polynomial results used here were ported (MinimalModel/Basic.lean, NodePolynomial.lean). The proof in this file was written against those ported results, not adapted from the source's proof of the headline.

theorem WeierstrassCurve.hasSplitMultiplicativeReduction_quadraticTwistOf (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u} [Field K] [Algebra R K] [IsFractionRing R K] {E : WeierstrassCurve K} [hE : HasMultiplicativeReduction R E] : HasSplitMultiplicativeReduction R (E.quadraticTwistOf (-E.a₁) (E.nodePolynomial.coeff 0 / E.c₄))

The explicit twist with split multiplicative reduction. If E has multiplicative reduction, the twist of E by the trace -a₁ and norm n = coeff₀ / c₄ of a root of the node quadratic T² + a₁ T + n has split multiplicative reduction: its node polynomial has the roots a₁² - 2n and 2n (nodePolynomial_quadraticTwistOf_neg_a₁). No hypothesis on the characteristic of K or of the residue field is needed, and none on whether the reduction of E is split.

theorem WeierstrassCurve.exists_quadraticTwist_hasSplitMultiplicativeReduction {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u} [Field K] [Algebra R K] [IsFractionRing R K] {E : WeierstrassCurve K} [E.IsElliptic] [HasMultiplicativeReduction R E] (h : ¬HasSplitMultiplicativeReduction R E) : ∃ (L : Type u) (x : Field L) (x_1 : Algebra K L) (x_2 : Algebra.IsQuadraticExtension K L) (x_3 : Algebra.IsSeparable K L), HasSplitMultiplicativeReduction R (minimal R (E.quadraticTwist L))

Quadratic twist to split multiplicative reduction. Over the fraction field K of a discrete valuation ring R, a curve with multiplicative but nonsplit reduction acquires split multiplicative reduction after a separable quadratic twist. As HasMultiplicativeReduction extends IsMinimal, the hypothesis is about a minimal equation; the conclusion is about Mathlib's chosen minimal equation .minimal R of the twist. The field L is found in the universe of K.