Tate's algorithm: the stopping conditions, and termination

Tate's algorithm reads the reduction symbol of a minimal Weierstrass equation over a discrete valuation ring R with uniformiser ϖ and perfect residue field k. It alternates changes of variables over R with divisibility tests, and stops as soon as one test succeeds. This file records the test at which the algorithm stops as a predicate on an integral equation, WeierstrassCurve.IsTateTerminal W ϖ s, and proves that the algorithm terminates: every minimal equation is carried by a change of variables over R to an equation on which one of the stopping tests succeeds.

The stopping conditions are stated on the coefficients of W without dividing by ϖ. With the residue cubic P(T) = T³ + (a₂/ϖ) T² + (a₄/ϖ²) T + a₆/ϖ³ of the Step 6 normal form, they are:

• I₀: ϖ ∤ Δ (Step 1);
• Iₙ for n ≥ 1: the reduction is singular at the origin (ϖ ∣ a₃, a₄, a₆), ϖ ∤ b₂, and v(Δ) = n (Step 2);
• II, III, IV: the reduction is singular at the origin, ϖ ∣ b₂, and respectively ϖ² ∤ a₆; ϖ² ∣ a₆ and ϖ³ ∤ b₈; ϖ² ∣ a₆, ϖ³ ∣ b₈ and ϖ³ ∤ b₆ (Steps 3 to 5);
• I₀*: the Step 6 normal form ϖ ∣ a₁, a₂, ϖ² ∣ a₃, a₄, ϖ³ ∣ a₆, and P has nonzero discriminant, that is ϖ⁷ ∤ disc(T³ + a₂ T² + a₄ T + a₆) (WeierstrassCurve.pow_seven_dvd_discr_iff);
• Iₙ* for n ≥ 1: the stopping stage n of the subprocedure of Step 7 (WeierstrassCurve.IsTateOddStage, WeierstrassCurve.IsTateEvenStage);
• IV*, III*, II*: the normal forms and tests of Steps 8, 9 and 10.

The equation must be minimal for the algorithm to stop: on a non-minimal equation the triple-root branch may reach Step 11, which rescales the equation and starts again. Minimality is used only there.

The algorithmic Ogg exponent v(Δ) − m + 1 of a symbol with m components (TauCeti.ReductionSymbol.algorithmicOggExponent) is 0 at I₀ and 1 at Iₙ, since there v(Δ) = n; at every additive symbol the stopping conditions force v(Δ) > m, so the exponent is at least 2.

Main definitions

• WeierstrassCurve.IsTateTerminal: Tate's algorithm, run on W, stops with output s without a further change of variables.

Main results

• WeierstrassCurve.exists_isTateTerminal: Tate's algorithm terminates. Over a discrete valuation ring with perfect residue field, a minimal equation with nonzero discriminant is carried by a change of variables over R to an equation on which the algorithm stops.
• WeierstrassCurve.IsTateTerminal.isTateOddStage_zero_of_IStar: every positive Iₙ* stopping condition implies the stage-one normal form.
• WeierstrassCurve.IsTateTerminal.isTateOddStage_of_IStar_two_mul_add_one and WeierstrassCurve.IsTateTerminal.isTateEvenStage_of_IStar_two_mul_add_two: the odd and even stopping conditions supply their respective stage and discriminant tests.
• WeierstrassCurve.isTateTerminal_map_iff: the stopping conditions transfer along a ring map that reflects divisibility by powers of the uniformiser.
• WeierstrassCurve.IsTateTerminal.addVal_Δ_eq: at a symbol Iₙ, the discriminant has valuation n.
• WeierstrassCurve.IsTateTerminal.pow_componentCount_add_one_dvd_Δ: at an additive symbol with m components, ϖ^(m+1) ∣ Δ.
• WeierstrassCurve.IsTateTerminal.dvd_b₂_and_dvd_a₃_and_dvd_a₄_and_dvd_a₆ and WeierstrassCurve.IsTateTerminal.dvd_c₄: at an additive symbol, ϖ divides b₂, a₃, a₄, a₆ and hence c₄.
• WeierstrassCurve.IsTateTerminal.ne_zero: at a symbol other than I₀, the uniformiser ϖ is nonzero.
• WeierstrassCurve.IsTateTerminal.prime_and_not_dvd_of_IVStar: at IV*, with a₃ = ϖ² A₃ and a₆ = ϖ⁴ A₆, the uniformiser is prime and ϖ ∤ A₃² + 4 A₆.
• WeierstrassCurve.IsTateTerminal.dvd_Δ_iff: the algorithm stops at a symbol other than I₀ exactly when ϖ ∣ Δ.
• WeierstrassCurve.IsTateTerminal.two_le_algorithmicOggExponent: at an additive symbol, the algorithmic Ogg exponent is at least 2.

The output of the algorithm is not shown here to be independent of the choices made along the way.

References

• J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, GTM 151, IV.9.
• 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.IsTateTerminal {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) : TauCeti.ReductionSymbol → Prop

The stopping conditions of Tate's algorithm. W.IsTateTerminal ϖ s says that Tate's algorithm, run on the integral equation W with uniformiser ϖ, stops with output s without a further change of variables. The conditions are those listed in the module docstring; for Iₙ* the stage n = 2k + 1 or n = 2k + 2 is the normal form IsTateOddStage ϖ k or IsTateEvenStage ϖ k of the subprocedure of Step 7.

@[simp]

theorem WeierstrassCurve.isTateTerminal_I_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.I 0) ↔ ¬ϖ ∣ W.Δ

@[simp]

theorem WeierstrassCurve.isTateTerminal_I_add_one {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {n : ℕ} : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.I (n + 1)) ↔ ϖ ∣ W.a₃ ∧ ϖ ∣ W.a₄ ∧ ϖ ∣ W.a₆ ∧ ¬ϖ ∣ W.b₂ ∧ ϖ ^ (n + 1) ∣ W.Δ ∧ ¬ϖ ^ (n + 2) ∣ W.Δ

@[simp]

theorem WeierstrassCurve.isTateTerminal_II {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.IsTateTerminal ϖ TauCeti.ReductionSymbol.II ↔ ϖ ∣ W.b₂ ∧ ϖ ∣ W.a₃ ∧ ϖ ∣ W.a₄ ∧ ϖ ∣ W.a₆ ∧ ¬ϖ ^ 2 ∣ W.a₆

@[simp]

theorem WeierstrassCurve.isTateTerminal_III {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.IsTateTerminal ϖ TauCeti.ReductionSymbol.III ↔ ϖ ∣ W.b₂ ∧ ϖ ∣ W.a₃ ∧ ϖ ∣ W.a₄ ∧ ϖ ^ 2 ∣ W.a₆ ∧ ¬ϖ ^ 3 ∣ W.b₈

@[simp]

theorem WeierstrassCurve.isTateTerminal_IV {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.IsTateTerminal ϖ TauCeti.ReductionSymbol.IV ↔ ϖ ∣ W.b₂ ∧ ϖ ∣ W.a₃ ∧ ϖ ∣ W.a₄ ∧ ϖ ^ 2 ∣ W.a₆ ∧ ϖ ^ 3 ∣ W.b₈ ∧ ¬ϖ ^ 3 ∣ W.b₆

@[simp]

theorem WeierstrassCurve.isTateTerminal_IStar_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.IStar 0) ↔ ϖ ∣ W.a₁ ∧ ϖ ∣ W.a₂ ∧ ϖ ^ 2 ∣ W.a₃ ∧ ϖ ^ 2 ∣ W.a₄ ∧ ϖ ^ 3 ∣ W.a₆ ∧ ¬ϖ ^ 7 ∣ { a := 1, b := W.a₂, c := W.a₄, d := W.a₆ }.discr

@[simp]

theorem WeierstrassCurve.isTateTerminal_IStar_add_one {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {n : ℕ} : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.IStar (n + 1)) ↔ (∃ (k : ℕ), n = 2 * k ∧ IsTateOddStage ϖ k W ∧ ¬ϖ ^ (2 * k + 5) ∣ W.b₆) ∨ ∃ (k : ℕ), n = 2 * k + 1 ∧ IsTateEvenStage ϖ k W ∧ ¬ϖ ^ (2 * k + 7) ∣ discrim W.a₂ W.a₄ W.a₆

theorem WeierstrassCurve.IsTateTerminal.isTateOddStage_zero_of_IStar {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {n : ℕ} (h : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.IStar (n + 1))) : IsTateOddStage ϖ 0 W

Both branches of the stopping test for Iₙ* satisfy the normal form of stage 1 of the subprocedure: ϖ ∣ a₁, ϖ ∥ a₂, ϖ² ∣ a₃, ϖ³ ∣ a₄ and ϖ⁴ ∣ a₆.

theorem WeierstrassCurve.IsTateTerminal.isTateOddStage_of_IStar_two_mul_add_one {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {k : ℕ} (h : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.IStar (2 * k + 1))) : IsTateOddStage ϖ k W ∧ ¬ϖ ^ (2 * k + 5) ∣ W.b₆

The stopping test at I*_{2k+1} is the odd stage k with ϖ^(2k+5) ∤ b₆.

theorem WeierstrassCurve.IsTateTerminal.isTateEvenStage_of_IStar_two_mul_add_two {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {k : ℕ} (h : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.IStar (2 * k + 2))) : IsTateEvenStage ϖ k W ∧ ¬ϖ ^ (2 * k + 7) ∣ discrim W.a₂ W.a₄ W.a₆

The stopping test at I*_{2k+2} is the even stage k with ϖ^(2k+7) ∤ a₄² − 4 a₂ a₆.

@[simp]

theorem WeierstrassCurve.isTateTerminal_IVStar {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.IsTateTerminal ϖ TauCeti.ReductionSymbol.IVStar ↔ ϖ ∣ W.a₁ ∧ ϖ ^ 2 ∣ W.a₂ ∧ ϖ ^ 2 ∣ W.a₃ ∧ ϖ ^ 3 ∣ W.a₄ ∧ ϖ ^ 4 ∣ W.a₆ ∧ ¬ϖ ^ 5 ∣ W.b₆

@[simp]

theorem WeierstrassCurve.isTateTerminal_IIIStar {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.IsTateTerminal ϖ TauCeti.ReductionSymbol.IIIStar ↔ ϖ ∣ W.a₁ ∧ ϖ ^ 2 ∣ W.a₂ ∧ ϖ ^ 3 ∣ W.a₃ ∧ ϖ ^ 3 ∣ W.a₄ ∧ ϖ ^ 5 ∣ W.a₆ ∧ ¬ϖ ^ 4 ∣ W.a₄

@[simp]

theorem WeierstrassCurve.isTateTerminal_IIStar {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.IsTateTerminal ϖ TauCeti.ReductionSymbol.IIStar ↔ ϖ ∣ W.a₁ ∧ ϖ ^ 2 ∣ W.a₂ ∧ ϖ ^ 3 ∣ W.a₃ ∧ ϖ ^ 4 ∣ W.a₄ ∧ ϖ ^ 5 ∣ W.a₆ ∧ ¬ϖ ^ 6 ∣ W.a₆

theorem WeierstrassCurve.isTateTerminal_map_iff {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {S : Type u_2} [CommRing S] (f : R →+* S) (hf : ∀ (n : ℕ) (x : R), f ϖ ^ n ∣ f x ↔ ϖ ^ n ∣ x) {s : TauCeti.ReductionSymbol} : (W.map f).IsTateTerminal (f ϖ) s ↔ W.IsTateTerminal ϖ s

The stopping conditions are read along a ring map that reflects divisibility by powers of the uniformiser. If f ϖ ^ n ∣ f x ↔ ϖ ^ n ∣ x for all n and x, then Tate's algorithm stops on W.map f with uniformiser f ϖ exactly where it stops on W with uniformiser ϖ. For instance the cast from ℤ to a discrete valuation ring with uniformiser a prime p reflects divisibility by powers of p (Nat.Prime.pow_dvd_intCast_iff), so the symbol of an integral equation over ℤ can be computed over ℤ.

theorem WeierstrassCurve.IsTateTerminal.pow_componentCount_add_one_dvd_Δ {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} [IsDomain R] (hϖ : Prime ϖ) {s : TauCeti.ReductionSymbol} (h : W.IsTateTerminal ϖ s) (hs : ∀ (n : ℕ), s ≠ TauCeti.ReductionSymbol.I n) : ϖ ^ (s.componentCount + 1) ∣ W.Δ

At a stopping symbol other than Iₙ with m components, ϖ^(m+1) divides the discriminant. This is the bound that makes the algorithmic Ogg exponent at least 2 there.

theorem WeierstrassCurve.IsTateTerminal.dvd_b₂_and_dvd_a₃_and_dvd_a₄_and_dvd_a₆ {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {s : TauCeti.ReductionSymbol} (h : W.IsTateTerminal ϖ s) (hs : ∀ (n : ℕ), s ≠ TauCeti.ReductionSymbol.I n) : ϖ ∣ W.b₂ ∧ ϖ ∣ W.a₃ ∧ ϖ ∣ W.a₄ ∧ ϖ ∣ W.a₆

At a stopping symbol other than Iₙ, the equation is in the additive normal form of Step 2 of Tate's algorithm: ϖ divides b₂, a₃, a₄ and a₆.

theorem WeierstrassCurve.IsTateTerminal.dvd_c₄ {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {s : TauCeti.ReductionSymbol} (h : W.IsTateTerminal ϖ s) (hs : ∀ (n : ℕ), s ≠ TauCeti.ReductionSymbol.I n) : ϖ ∣ W.c₄

At a stopping symbol other than Iₙ, ϖ divides c₄. In the additive normal form ϖ divides b₂ and b₄, and c₄ = b₂² − 24 b₄.

theorem WeierstrassCurve.IsTateTerminal.ne_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {s : TauCeti.ReductionSymbol} (h : W.IsTateTerminal ϖ s) (hs : s ≠ TauCeti.ReductionSymbol.I 0) : ϖ ≠ 0

At a stopping symbol other than I₀, the uniformiser is nonzero. If ϖ = 0, the divisibility conditions force the relevant coefficients to vanish, and then the stopping test ¬ 0 ^ k ∣ _ fails.

theorem WeierstrassCurve.IsTateTerminal.prime_and_not_dvd_of_IVStar {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : (Ideal.span {ϖ}).IsPrime) (h : W.IsTateTerminal ϖ TauCeti.ReductionSymbol.IVStar) {A₃ A₆ : R} (h₃ : W.a₃ = ϖ ^ 2 * A₃) (h₆ : W.a₆ = ϖ ^ 4 * A₆) : Prime ϖ ∧ ¬ϖ ∣ A₃ ^ 2 + 4 * A₆

At the symbol IV*, the residue quadratic has distinct roots. If (ϖ) is a prime ideal, a₃ = ϖ² A₃ and a₆ = ϖ⁴ A₆, then the test ϖ⁵ ∤ b₆ = ϖ⁴ (A₃² + 4 A₆) says that ϖ is prime and does not divide the discriminant A₃² + 4 A₆ of T² + A₃ T − A₆.

theorem WeierstrassCurve.IsTateTerminal.dvd_Δ_iff {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {s : TauCeti.ReductionSymbol} (h : W.IsTateTerminal ϖ s) : ϖ ∣ W.Δ ↔ s ≠ TauCeti.ReductionSymbol.I 0

Tate's algorithm stops at a symbol other than I₀ exactly when ϖ divides the discriminant.

theorem WeierstrassCurve.pow_seven_dvd_discr_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} {W : WeierstrassCurve R} (hϖ : Irreducible ϖ) {A₂ A₄ A₆ : R} (hA₂ : W.a₂ = ϖ * A₂) (hA₄ : W.a₄ = ϖ ^ 2 * A₄) (hA₆ : W.a₆ = ϖ ^ 3 * A₆) : ϖ ^ 7 ∣ { a := 1, b := W.a₂, c := W.a₄, d := W.a₆ }.discr ↔ { a := 1, b := (IsLocalRing.residue R) A₂, c := (IsLocalRing.residue R) A₄, d := (IsLocalRing.residue R) A₆ }.discr = 0

The I₀* test is the residue-cubic test. If a₂ = ϖ A₂, a₄ = ϖ² A₄ and a₆ = ϖ³ A₆, then ϖ⁷ divides the discriminant of T³ + a₂ T² + a₄ T + a₆ exactly when the residue cubic T³ + A₂ T² + A₄ T + A₆ over the residue field has zero discriminant.

theorem WeierstrassCurve.IsTateTerminal.addVal_Δ_eq {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} {W : WeierstrassCurve R} (hϖ : Irreducible ϖ) {n : ℕ} (h : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.I n)) : (IsDiscreteValuationRing.addVal R) W.Δ = ↑n

At the symbol Iₙ, the discriminant has valuation n.

theorem WeierstrassCurve.IsTateTerminal.two_le_algorithmicOggExponent {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} {W : WeierstrassCurve R} (hϖ : Irreducible ϖ) {s : TauCeti.ReductionSymbol} (h : W.IsTateTerminal ϖ s) (hs : ∀ (n : ℕ), s ≠ TauCeti.ReductionSymbol.I n) {n : ℕ} (hn : (IsDiscreteValuationRing.addVal R) W.Δ = ↑n) : 2 ≤ s.algorithmicOggExponent n

The algorithmic Ogg exponent at an additive symbol is at least 2. If Tate's algorithm stops on W with a symbol other than Iₙ, and n is the valuation of the discriminant, then n − m + 1 ≥ 2, where m is the component count of the symbol.

Termination

theorem WeierstrassCurve.exists_isTateTerminal {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {ϖ : R} {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [PerfectField (IsLocalRing.ResidueField R)] (hϖ : Irreducible ϖ) (W : WeierstrassCurve R) (hΔ : W.Δ ≠ 0) [IsMinimal R (W.baseChange K)] : ∃ (C : VariableChange R) (s : TauCeti.ReductionSymbol), (C • W).IsTateTerminal ϖ s

Tate's algorithm terminates. Over a discrete valuation ring with uniformiser ϖ and perfect residue field, a Weierstrass equation over R with nonzero discriminant that is minimal over the fraction field K is carried by a change of variables over R to an equation on which one of the stopping tests of Tate's algorithm succeeds.