Tate's algorithm: the double-root branch

Let R be a discrete valuation ring with uniformiser ϖ and perfect residue field k. Step 6 of Tate's algorithm (WeierstrassCurve.exists_variableChange_dvd_a₁_a₂_a₃_a₄_a₆) brings an equation with additive reduction to the normal form ϖ ∣ a₁, a₂, ϖ² ∣ a₃, a₄, ϖ³ ∣ a₆, and reads off it the residue cubic

P(T) = T³ + (a₂/ϖ) T² + (a₄/ϖ²) T + a₆/ϖ³ over k.

This file treats the branch of the algorithm in which P has a double root that is not a triple root (Step 7). In Tate's algorithm this branch has reduction symbol Iₙ* for some n ≥ 1; this file formalizes the reduction steps and the termination of the subprocedure, not the identification of the reduction symbol.

Translating x ↦ x + r moves the double root to T = 0 (WeierstrassCurve.exists_variableChange_not_sq_dvd_a₂_and_pow_dvd_a₄_a₆). Then ϖ divides a₂ exactly once, written ϖ ∥ a₂ below, because the simple root -a₂/ϖ of P is nonzero, and the equation is in the normal form of stage n = 1 of the following subprocedure. At stage n the equation satisfies ϖ ∣ a₁, ϖ ∥ a₂ and

• for n = 2k + 1 odd: ϖ^(k+2) ∣ a₃, ϖ^(k+3) ∣ a₄, ϖ^(2k+4) ∣ a₆. If the quadratic Y² + (a₃/ϖ^(k+2)) Y − a₆/ϖ^(2k+4) has distinct roots, that is if ϖ^(2k+5) ∤ b₆, the subprocedure stops (Tate's algorithm then assigns Iₙ*). Otherwise a translation y ↦ y + t moves its double root to 0 (WeierstrassCurve.exists_pow_dvd_and_variableChange_pow_dvd_a₃_a₆) and gives stage n + 1;
• for n = 2k + 2 even: ϖ^(k+3) ∣ a₃, ϖ^(k+3) ∣ a₄, ϖ^(2k+5) ∣ a₆. If the quadratic (a₂/ϖ) X² + (a₄/ϖ^(k+3)) X + a₆/ϖ^(2k+5) has distinct roots, that is if ϖ^(2k+7) ∤ discrim a₂ a₄ a₆ = a₄² − 4 a₂ a₆, the subprocedure stops (Tate's algorithm then assigns Iₙ*). Otherwise a translation x ↦ x + r moves its double root to 0 (WeierstrassCurve.exists_pow_dvd_and_variableChange_pow_dvd_a₄_a₆) and gives stage n + 1.

Each stage forces ϖ^(n+6) ∣ Δ, and translations do not change Δ, so the subprocedure stops at some stage n with n + 6 ≤ v(Δ) whenever Δ ≠ 0 (WeierstrassCurve.exists_variableChange_not_pow_dvd_b₆_or_discrim). No minimality hypothesis is needed for this. Perfectness of k is used to find the double roots of the quadratics, which in characteristic 2 are square roots.

Main results

• WeierstrassCurve.IsTateOddStage and WeierstrassCurve.IsTateEvenStage: the normal forms at the stages of the subprocedure, with the discriminant bounds IsTateOddStage.pow_dvd_Δ and IsTateEvenStage.pow_dvd_Δ.
• WeierstrassCurve.exists_variableChange_not_sq_dvd_a₂_and_pow_dvd_a₄_a₆: Step 7 of Tate's algorithm, the translation. If the residue cubic of an equation in the normal form of Step 6 has a double root that is not a triple root, a translation x ↦ x + r over R produces ϖ ∣ a₁, ϖ ∥ a₂, ϖ² ∣ a₃, ϖ³ ∣ a₄ and ϖ⁴ ∣ a₆.
• WeierstrassCurve.exists_pow_dvd_and_variableChange_pow_dvd_a₃_a₆: completing the square in y. If ϖ^m ∣ a₃, ϖ^(2m) ∣ a₆ and ϖ^(2m+1) ∣ b₆, a translation y ↦ y + t with ϖ^m ∣ t produces ϖ^(m+1) ∣ a₃ and ϖ^(2m+1) ∣ a₆.
• WeierstrassCurve.exists_pow_dvd_and_variableChange_pow_dvd_a₄_a₆: completing the square in x. If m ≥ 2, ϖ ∥ a₂, ϖ^(m+1) ∣ a₄, ϖ^(2m+1) ∣ a₆ and ϖ^(2m+3) ∣ discrim a₂ a₄ a₆, a translation x ↦ x + r with ϖ^m ∣ r produces ϖ^(m+2) ∣ a₄ and ϖ^(2m+2) ∣ a₆.
• WeierstrassCurve.exists_variableChange_not_pow_dvd_b₆_or_discrim: the Iₙ* subprocedure of Tate's algorithm terminates. From the normal form of Step 7 and Δ ≠ 0, a translation over R reaches stage n = 2k + 1 with ϖ^(2k+5) ∤ b₆, or stage n = 2k + 2 with ϖ^(2k+7) ∤ discrim a₂ a₄ a₆, and in either case ϖ^(n+6) ∣ Δ.

References

• J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, GTM 151, IV.9, Step 7 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.

def WeierstrassCurve.IsTateOddStage {R : Type u_1} [CommRing R] (ϖ : R) (k : ℕ) (W : WeierstrassCurve R) : Prop

The equation is at an odd stage n = 2k + 1 of the Iₙ* subprocedure of Tate's algorithm: ϖ ∣ a₁, ϖ ∥ a₂, ϖ^(k+2) ∣ a₃, ϖ^(k+3) ∣ a₄ and ϖ^(2k+4) ∣ a₆.

def WeierstrassCurve.IsTateEvenStage {R : Type u_1} [CommRing R] (ϖ : R) (k : ℕ) (W : WeierstrassCurve R) : Prop

The equation is at an even stage n = 2k + 2 of the Iₙ* subprocedure of Tate's algorithm: ϖ ∣ a₁, ϖ ∥ a₂, ϖ^(k+3) ∣ a₃, ϖ^(k+3) ∣ a₄ and ϖ^(2k+5) ∣ a₆.

@[simp]

theorem WeierstrassCurve.isTateOddStage_iff {R : Type u_1} [CommRing R] {ϖ : R} {k : ℕ} {W : WeierstrassCurve R} : IsTateOddStage ϖ k W ↔ ϖ ∣ W.a₁ ∧ ϖ ∣ W.a₂ ∧ ¬ϖ ^ 2 ∣ W.a₂ ∧ ϖ ^ (k + 2) ∣ W.a₃ ∧ ϖ ^ (k + 3) ∣ W.a₄ ∧ ϖ ^ (2 * k + 4) ∣ W.a₆

Unfolding IsTateOddStage.

@[simp]

theorem WeierstrassCurve.isTateEvenStage_iff {R : Type u_1} [CommRing R] {ϖ : R} {k : ℕ} {W : WeierstrassCurve R} : IsTateEvenStage ϖ k W ↔ ϖ ∣ W.a₁ ∧ ϖ ∣ W.a₂ ∧ ¬ϖ ^ 2 ∣ W.a₂ ∧ ϖ ^ (k + 3) ∣ W.a₃ ∧ ϖ ^ (k + 3) ∣ W.a₄ ∧ ϖ ^ (2 * k + 5) ∣ W.a₆

Unfolding IsTateEvenStage.

theorem WeierstrassCurve.IsTateOddStage.pow_dvd_Δ {R : Type u_1} [CommRing R] {ϖ : R} {k : ℕ} {W : WeierstrassCurve R} (hW : IsTateOddStage ϖ k W) : ϖ ^ (2 * k + 7) ∣ W.Δ

At stage n = 2k + 1, ϖ^(n+6) ∣ Δ.

theorem WeierstrassCurve.IsTateEvenStage.pow_dvd_Δ {R : Type u_1} [CommRing R] {ϖ : R} {k : ℕ} {W : WeierstrassCurve R} (hW : IsTateEvenStage ϖ k W) : ϖ ^ (2 * k + 8) ∣ W.Δ

At stage n = 2k + 2, ϖ^(n+6) ∣ Δ.

theorem WeierstrassCurve.exists_variableChange_not_sq_dvd_a₂_and_pow_dvd_a₄_a₆ {R : Type u_1} [CommRing R] {ϖ : R} [IsDomain R] [IsDiscreteValuationRing R] (hϖ : Irreducible ϖ) (W : WeierstrassCurve R) (h₁ : ϖ ∣ W.a₁) (h₃ : ϖ ^ 2 ∣ W.a₃) {A₂ A₄ A₆ : R} (hA₂ : W.a₂ = ϖ * A₂) (hA₄ : W.a₄ = ϖ ^ 2 * A₄) (hA₆ : W.a₆ = ϖ ^ 3 * A₆) (ρ : IsLocalRing.ResidueField R) (hρ : ρ ^ 3 + (IsLocalRing.residue R) A₂ * ρ ^ 2 + (IsLocalRing.residue R) A₄ * ρ + (IsLocalRing.residue R) A₆ = 0) (hρ' : 3 * ρ ^ 2 + 2 * (IsLocalRing.residue R) A₂ * ρ + (IsLocalRing.residue R) A₄ = 0) (hρ'' : 3 * ρ + (IsLocalRing.residue R) A₂ ≠ 0) : ∃ (r : R), ϖ ∣ ({ u := 1, r := r, s := 0, t := 0 } • W).a₁ ∧ ϖ ∣ ({ u := 1, r := r, s := 0, t := 0 } • W).a₂ ∧ ¬ϖ ^ 2 ∣ ({ u := 1, r := r, s := 0, t := 0 } • W).a₂ ∧ ϖ ^ 2 ∣ ({ u := 1, r := r, s := 0, t := 0 } • W).a₃ ∧ ϖ ^ 3 ∣ ({ u := 1, r := r, s := 0, t := 0 } • W).a₄ ∧ ϖ ^ 4 ∣ ({ u := 1, r := r, s := 0, t := 0 } • W).a₆

Tate's algorithm, Step 7: moving the double root to 0. Over a discrete valuation ring with uniformiser ϖ, let W be an equation in the normal form of Step 6, with ϖ ∣ a₁, ϖ² ∣ a₃, a₂ = ϖ A₂, a₄ = ϖ² A₄ and a₆ = ϖ³ A₆, and let ρ be a double root of the residue cubic P(T) = T³ + A₂ T² + A₄ T + A₆ which is not a triple root: P(ρ) = 0, P'(ρ) = 0 and 3 ρ + A₂ ≠ 0, the last saying that the third root -A₂ - 2 ρ of P differs from ρ. Then a translation x ↦ x + r with r ∈ R produces an equation with ϖ ∣ a₁, ϖ ∣ a₂ but ϖ² ∤ a₂, ϖ² ∣ a₃, ϖ³ ∣ a₄ and ϖ⁴ ∣ a₆.

theorem WeierstrassCurve.exists_pow_dvd_and_variableChange_pow_dvd_a₃_a₆ {R : Type u_1} [CommRing R] {ϖ : R} [IsDomain R] [IsDiscreteValuationRing R] [PerfectField (IsLocalRing.ResidueField R)] (hϖ : Irreducible ϖ) (W : WeierstrassCurve R) {m : ℕ} (h₃ : ϖ ^ m ∣ W.a₃) (h₆ : ϖ ^ (2 * m) ∣ W.a₆) (hb₆ : ϖ ^ (2 * m + 1) ∣ W.b₆) : ∃ (t : R), ϖ ^ m ∣ t ∧ ϖ ^ (m + 1) ∣ ({ u := 1, r := 0, s := 0, t := t } • W).a₃ ∧ ϖ ^ (2 * m + 1) ∣ ({ u := 1, r := 0, s := 0, t := t } • W).a₆

Completing the square in y. Over a discrete valuation ring with uniformiser ϖ and perfect residue field, let W be an equation with ϖ^m ∣ a₃ and ϖ^(2m) ∣ a₆ whose quadratic Y² + (a₃/ϖ^m) Y − a₆/ϖ^(2m) has a double root modulo ϖ, that is ϖ^(2m+1) ∣ b₆. Then a translation y ↦ y + t with ϖ^m ∣ t moves the double root to 0: the new equation has ϖ^(m+1) ∣ a₃ and ϖ^(2m+1) ∣ a₆. The translation fixes a₁ and a₂ and changes a₄ to a₄ − t a₁.

theorem WeierstrassCurve.exists_pow_dvd_and_variableChange_pow_dvd_a₄_a₆ {R : Type u_1} [CommRing R] {ϖ : R} [IsDomain R] [IsDiscreteValuationRing R] [PerfectField (IsLocalRing.ResidueField R)] (hϖ : Irreducible ϖ) (W : WeierstrassCurve R) {m : ℕ} (hm : 2 ≤ m) (h₂ : ϖ ∣ W.a₂) (h₂' : ¬ϖ ^ 2 ∣ W.a₂) (h₄ : ϖ ^ (m + 1) ∣ W.a₄) (h₆ : ϖ ^ (2 * m + 1) ∣ W.a₆) (hd : ϖ ^ (2 * m + 3) ∣ discrim W.a₂ W.a₄ W.a₆) : ∃ (r : R), ϖ ^ m ∣ r ∧ ϖ ^ (m + 2) ∣ ({ u := 1, r := r, s := 0, t := 0 } • W).a₄ ∧ ϖ ^ (2 * m + 2) ∣ ({ u := 1, r := r, s := 0, t := 0 } • W).a₆

Completing the square in x. Over a discrete valuation ring with uniformiser ϖ and perfect residue field, let m ≥ 2 and let W be an equation with ϖ ∣ a₂ but ϖ² ∤ a₂, ϖ^(m+1) ∣ a₄ and ϖ^(2m+1) ∣ a₆, whose quadratic (a₂/ϖ) X² + (a₄/ϖ^(m+1)) X + a₆/ϖ^(2m+1) has a double root modulo ϖ, that is ϖ^(2m+3) ∣ discrim a₂ a₄ a₆ = a₄² − 4 a₂ a₆. Then a translation x ↦ x + r with ϖ^m ∣ r moves the double root to 0: the new equation has ϖ^(m+2) ∣ a₄ and ϖ^(2m+2) ∣ a₆. The translation fixes a₁, changes a₂ to a₂ + 3 r and a₃ to a₃ + r a₁.

theorem WeierstrassCurve.exists_variableChange_not_pow_dvd_b₆_or_discrim {R : Type u_1} [CommRing R] {ϖ : R} [IsDomain R] [IsDiscreteValuationRing R] [PerfectField (IsLocalRing.ResidueField R)] (hϖ : Irreducible ϖ) (W : WeierstrassCurve R) (hΔ : W.Δ ≠ 0) (h₁ : ϖ ∣ W.a₁) (h₂ : ϖ ∣ W.a₂) (h₂' : ¬ϖ ^ 2 ∣ W.a₂) (h₃ : ϖ ^ 2 ∣ W.a₃) (h₄ : ϖ ^ 3 ∣ W.a₄) (h₆ : ϖ ^ 4 ∣ W.a₆) : ∃ (r : R) (t : R) (k : ℕ), ϖ ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₁ ∧ ϖ ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₂ ∧ ¬ϖ ^ 2 ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₂ ∧ (ϖ ^ (k + 2) ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₃ ∧ ϖ ^ (k + 3) ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₄ ∧ ϖ ^ (2 * k + 4) ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₆ ∧ ¬ϖ ^ (2 * k + 5) ∣ ({ u := 1, r := r, s := 0, t := t } • W).b₆ ∧ ϖ ^ (2 * k + 7) ∣ W.Δ ∨ ϖ ^ (k + 3) ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₃ ∧ ϖ ^ (k + 3) ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₄ ∧ ϖ ^ (2 * k + 5) ∣ ({ u := 1, r := r, s := 0, t := t } • W).a₆ ∧ ¬ϖ ^ (2 * k + 7) ∣ discrim ({ u := 1, r := r, s := 0, t := t } • W).a₂ ({ u := 1, r := r, s := 0, t := t } • W).a₄ ({ u := 1, r := r, s := 0, t := t } • W).a₆ ∧ ϖ ^ (2 * k + 8) ∣ W.Δ)

The Iₙ* subprocedure of Tate's algorithm terminates. Over a discrete valuation ring with uniformiser ϖ and perfect residue field, let W be an equation with nonzero discriminant in the normal form of Step 7: ϖ ∣ a₁, ϖ ∣ a₂ but ϖ² ∤ a₂, ϖ² ∣ a₃, ϖ³ ∣ a₄ and ϖ⁴ ∣ a₆. Then a translation x ↦ x + r, y ↦ y + t over R produces an equation with ϖ ∣ a₁, ϖ ∣ a₂ and ϖ² ∤ a₂ on which the subprocedure stops, at an odd stage n = 2k + 1: ϖ^(k+2) ∣ a₃, ϖ^(k+3) ∣ a₄, ϖ^(2k+4) ∣ a₆ and ϖ^(2k+5) ∤ b₆; or at an even stage n = 2k + 2: ϖ^(k+3) ∣ a₃, ϖ^(k+3) ∣ a₄, ϖ^(2k+5) ∣ a₆ and ϖ^(2k+7) ∤ discrim a₂ a₄ a₆. In both cases ϖ^(n+6) ∣ Δ. (In Tate's algorithm the stopping stage n gives the reduction symbol Iₙ*; that identification is not part of this statement.)