Tate's algorithm: the singular point at the origin

Tate's algorithm reads the reduction type of a minimal Weierstrass equation over a discrete valuation ring R, with uniformiser π and perfect residue field k, off a sequence of changes of variables defined over R and divisibility tests on the coefficients. This file contains its first two steps, from whose normal form every later step starts.

Step 1 tests whether π ∣ Δ: the reduction is good exactly when it does not (WeierstrassCurve.reduction_Δ_eq_zero_iff). Otherwise the reduced curve is singular, and its singular point is k-rational because k is perfect (WeierstrassCurve.Affine.exists_isSingular_of_Δ_eq_zero). Step 2 lifts that point to R and translates it to the origin by x ↦ x + r, y ↦ y + t. Afterwards π divides a₃, a₄ and a₆, so the reduced equation reads y² + a₁ x y = x³ + a₂ x² and has c₄ = b₂². On such an equation:

• the reduction is multiplicative exactly when π ∤ b₂, and additive exactly when π ∣ b₂;
• a multiplicative reduction is split exactly when the tangent quadratic T² + a₁ T − a₂ splits over k, its roots being the slopes of the two tangent lines at the node.

Every reduction type is invariant under changes of variables defined over R (WeierstrassCurve.hasMultiplicativeReduction_baseChange_smul_iff and its companions), so these tests decide the reduction type of the equation one started from.

Perfectness of k is used only to find the singular point. Over the imperfect field 𝔽₃(s) the cubic y² = x³ − s is singular only at (s^{1/3}, 0), which is not rational.

Main results

• WeierstrassCurve.map_residue_isSingular_zero_iff: the reduction of an integral equation over a local ring is singular at the origin exactly when a₆, a₄ and a₃ lie in the maximal ideal.

• WeierstrassCurve.exists_map_residue_variableChange_isSingular_zero: over a local ring with perfect residue field, an integral equation whose discriminant lies in the maximal ideal is translated over R to one whose reduction is singular at the origin.

• WeierstrassCurve.exists_reduction_baseChange_smul_isSingular_zero: a minimal equation with bad reduction is translated over R to a minimal equation whose reduction is singular at the origin.

• WeierstrassCurve.hasMultiplicativeReduction_iff_reduction_b₂_ne_zero and WeierstrassCurve.hasAdditiveReduction_iff_reduction_b₂_eq_zero: on a minimal equation whose reduction is singular at the origin, the reduction is multiplicative when π ∤ b₂ and additive when π ∣ b₂.

• WeierstrassCurve.hasSplitMultiplicativeReduction_iff_reduction_b₂_ne_zero_and_splits: on such an equation, the reduction is split multiplicative exactly when π ∤ b₂ and T² + a₁ T − a₂ splits over the residue field.

• WeierstrassCurve.dvd_b₄_and_dvd_b₆_and_sq_dvd_b₈_of_dvd_b₂_of_dvd_a₃_of_dvd_a₄_of_dvd_a₆ and WeierstrassCurve.sq_dvd_Δ_of_dvd_b₂_of_dvd_a₃_of_dvd_a₄_of_dvd_a₆: the invariant and discriminant divisibilities of the additive Step 2 normal form.

References

• J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, GTM 151, IV.9, Steps 1 and 2 of Tate's algorithm.
• J. Tate, Algorithm for determining the type of a singular fibre in an elliptic pencil, in Modular Functions of One Variable IV, LNM 476 (1975), 33–52.

theorem WeierstrassCurve.map_residue_isSingular_zero_iff {R : Type u_1} [CommRing R] [IsLocalRing R] (W : WeierstrassCurve R) : (W.map (IsLocalRing.residue R)).toAffine.IsSingular 0 0 ↔ W.a₆ ∈ IsLocalRing.maximalIdeal R ∧ W.a₄ ∈ IsLocalRing.maximalIdeal R ∧ W.a₃ ∈ IsLocalRing.maximalIdeal R

The reduction of an integral equation is singular at the origin exactly when a₆, a₄ and a₃ lie in the maximal ideal, which is the normal form Step 2 of Tate's algorithm produces.

theorem WeierstrassCurve.exists_map_residue_variableChange_isSingular_zero {R : Type u_1} [CommRing R] [IsLocalRing R] [PerfectField (IsLocalRing.ResidueField R)] (W : WeierstrassCurve R) (hΔ : W.Δ ∈ IsLocalRing.maximalIdeal R) : ∃ (r : R) (t : R), (({ u := 1, r := r, s := 0, t := t } • W).map (IsLocalRing.residue R)).toAffine.IsSingular 0 0

Tate's algorithm, Step 2. Over a local ring with perfect residue field, an integral Weierstrass equation whose discriminant lies in the maximal ideal is carried by a translation x ↦ x + r, y ↦ y + t with r, t ∈ R to an equation whose reduction is singular at the origin, that is, whose a₃, a₄ and a₆ lie in the maximal ideal (map_residue_isSingular_zero_iff). The translation lifts the singular point of the reduction, which is rational over the residue field because that field is perfect.

theorem WeierstrassCurve.exists_reduction_baseChange_smul_isSingular_zero (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [PerfectField (IsLocalRing.ResidueField R)] [IsMinimal R W] (h : ¬HasGoodReduction R W) : ∃ (r : R) (t : R), (reduction R ({ u := 1, r := r, s := 0, t := t }.baseChange K • W)).toAffine.IsSingular 0 0

Tate's algorithm, Step 2, for a minimal equation. Over a discrete valuation ring with perfect residue field, a minimal Weierstrass equation with bad reduction is carried by a translation x ↦ x + r, y ↦ y + t with r, t ∈ R to a minimal equation whose reduction is singular at the origin. The translated equation has the same reduction type (hasMultiplicativeReduction_baseChange_smul_iff and its companions).

theorem WeierstrassCurve.hasMultiplicativeReduction_iff_reduction_b₂_ne_zero (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [IsMinimal R W] (hW : (reduction R W).toAffine.IsSingular 0 0) : HasMultiplicativeReduction R W ↔ (reduction R W).b₂ ≠ 0

Tate's test for multiplicative reduction. On a minimal equation whose reduction is singular at the origin, the reduction is multiplicative exactly when π ∤ b₂: there c₄ ≡ b₂² (mod π), and multiplicative reduction is the case of a singular reduction with π ∤ c₄.

theorem WeierstrassCurve.hasAdditiveReduction_iff_reduction_b₂_eq_zero (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [IsMinimal R W] (hW : (reduction R W).toAffine.IsSingular 0 0) : HasAdditiveReduction R W ↔ (reduction R W).b₂ = 0

Tate's test for additive reduction. On a minimal equation whose reduction is singular at the origin, the reduction is additive exactly when π ∣ b₂.

theorem WeierstrassCurve.hasSplitMultiplicativeReduction_iff_reduction_b₂_ne_zero_and_splits (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve K} [IsMinimal R W] (hW : (reduction R W).toAffine.IsSingular 0 0) : HasSplitMultiplicativeReduction R W ↔ (reduction R W).b₂ ≠ 0 ∧ (Polynomial.X ^ 2 + Polynomial.C (reduction R W).a₁ * Polynomial.X - Polynomial.C (reduction R W).a₂).Splits

Tate's test for split multiplicative reduction. On a minimal equation whose reduction is singular at the origin, the reduction is split multiplicative exactly when π ∤ b₂ and the tangent quadratic T² + a₁ T − a₂ of the reduced equation splits over the residue field. Its roots are the slopes of the two tangent lines at the node, and the node polynomial of HasSplitMultiplicativeReduction is c₄ times it.

theorem WeierstrassCurve.dvd_b₄_and_dvd_b₆_and_sq_dvd_b₈_of_dvd_b₂_of_dvd_a₃_of_dvd_a₄_of_dvd_a₆ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) (hb₂ : ϖ ∣ W.b₂) (h₃ : ϖ ∣ W.a₃) (h₄ : ϖ ∣ W.a₄) (h₆ : ϖ ∣ W.a₆) : ϖ ∣ W.b₄ ∧ ϖ ∣ W.b₆ ∧ ϖ ^ 2 ∣ W.b₈

In the additive Step 2 normal form, ϖ divides b₄ and b₆, and ϖ² divides b₈. The last assertion uses ϖ ∣ b₂ as well as the singularity at the origin.

theorem WeierstrassCurve.sq_dvd_Δ_of_dvd_b₂_of_dvd_a₃_of_dvd_a₄_of_dvd_a₆ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) (hb₂ : ϖ ∣ W.b₂) (h₃ : ϖ ∣ W.a₃) (h₄ : ϖ ∣ W.a₄) (h₆ : ϖ ∣ W.a₆) : ϖ ^ 2 ∣ W.Δ

The additive Step 2 normal form has discriminant divisible by ϖ².