Tate's algorithm: the local index

When Tate's algorithm stops on an integral Weierstrass equation W over a discrete valuation ring R with uniformiser ϖ and residue field k, it reads off the stopping equation, besides the reduction symbol, the local index c, or Tamagawa number. For complete R it is the index [E(K) : E₀(K)] of the points with nonsingular reduction, and geometrically it counts the components of multiplicity one of the special fibre of the minimal regular model that are defined over k (Silverman, Advanced Topics, IV.9, Table 4.1). At the symbols I₀, II, III, III* and II* it is determined by the symbol. At the others it depends on whether a polynomial over k read off the stopping equation has roots in k:

• Iₙ, n ≥ 1: c = n if the tangent quadratic T² + a₁ T − a₂ splits over k, and otherwise c = gcd(2, n);
• IV: c = 3 if Y² + (a₃/ϖ) Y − a₆/ϖ² splits over k, and otherwise c = 1;
• I₀*: c = 1 + N, where N is the number of roots in k of the residue cubic P(T) = T³ + (a₂/ϖ) T² + (a₄/ϖ²) T + a₆/ϖ³;
• Iₙ*, n ≥ 1: c = 4 if the quadratic at which the subprocedure of Step 7 stops splits over k, and otherwise c = 2. At stage n = 2k + 1 this is Y² + (a₃/ϖ^(k+2)) Y − a₆/ϖ^(2k+4), and at stage n = 2k + 2 it is (a₂/ϖ) X² + (a₄/ϖ^(k+3)) X + a₆/ϖ^(2k+5);
• IV*: c = 3 if Y² + (a₃/ϖ²) Y − a₆/ϖ⁴ splits over k, and otherwise c = 1.

As for the stopping conditions (WeierstrassCurve.IsTateTerminal), these tests are stated on the coefficients of W without dividing by ϖ, and over any commutative ring. A monic quadratic splits as soon as it has one root, and substituting y = ϖ^m s turns a root s of Y² + (a₃/ϖ^m) Y − a₆/ϖ^(2m) modulo ϖ into a solution y of y² + a₃ y − a₆ ≡ 0 modulo ϖ^(2m+1) divisible by ϖ^m. That is the predicate WeierstrassCurve.HasTateYRoot, and WeierstrassCurve.hasTateYRoot_iff recovers the residue quadratic once the divisibilities of the stopping equation are written out; likewise for WeierstrassCurve.HasTateXRoot and for the roots of the residue cubic, which are counted in R ⧸ (ϖ).

The local index is defined here as a function W.tateLocalIndex ϖ s of the equation, the uniformiser and the symbol: it is the value Tate's algorithm reports when it stops on W with symbol s. Over a Henselian valuation ring with finite residue field it equals the index [E(K) : E₀(K)], and hence does not depend on the equation on which the algorithm stops; both facts are proved with the point groups, in Affine/Point/Index/TateAlgorithm.lean.

Main definitions

• WeierstrassCurve.HasTateTangentRoot: T² + a₁ T − a₂ has a root modulo ϖ.
• WeierstrassCurve.HasTateYRoot and WeierstrassCurve.HasTateXRoot: the residue quadratics of Steps 5, 7 and 8 have a root.
• WeierstrassCurve.tateCubicRoots: the roots in R ⧸ (ϖ) of the residue cubic of Step 6.
• WeierstrassCurve.tateLocalIndex: the local index Tate's algorithm reports.

Main results

• WeierstrassCurve.hasTateTangentRoot_iff_splits: over a discrete valuation ring, the tangent test is the splitting of T² + a₁ T − a₂ over the residue field.
• WeierstrassCurve.IsTateTerminal.tateLocalIndex_of_hasSplitMultiplicativeReduction and WeierstrassCurve.IsTateTerminal.tateLocalIndex_of_not_hasSplitMultiplicativeReduction: at Iₙ on a minimal equation, c = n at split and c = gcd(2, n) at nonsplit multiplicative reduction.
• WeierstrassCurve.hasTateYRoot_iff, WeierstrassCurve.hasTateXRoot_iff, WeierstrassCurve.mk_mem_tateCubicRoots_iff and WeierstrassCurve.mem_tateCubicRoots_iff: the tests are root conditions for the residue polynomials.
• WeierstrassCurve.hasTateYRoot_iff_exists_residue_root and WeierstrassCurve.hasTateXRoot_iff_exists_residue_root: over a local domain whose maximal ideal is generated by ϖ, the quadratic tests in y and in x are the existence of a root in the residue field.
• WeierstrassCurve.hasTateTangentRoot_iff_exists_residue_root: over a local ring whose maximal ideal is generated by ϖ, the tangent test is the existence of a root of T² + a₁ T − a₂ in the residue field.
• WeierstrassCurve.natCard_tateCubicRoots_eq: over a local domain whose maximal ideal is generated by ϖ, the roots of the residue cubic in R ⧸ (ϖ) are as many as its roots in the residue field.
• WeierstrassCurve.natCard_tateCubicRoots_le: the residue cubic has at most three roots.
• WeierstrassCurve.tateLocalIndex_pos, WeierstrassCurve.IsTateTerminal.tateLocalIndex_le_componentCount and WeierstrassCurve.IsTateTerminal.tateLocalIndex_le_four: 1 ≤ c ≤ m for the component count m of the symbol, and c ≤ 4 at every additive symbol.

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.HasTateTangentRoot {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) : Prop

The split test of Step 2 of Tate's algorithm: the tangent quadratic T² + a₁ T − a₂ has a root modulo ϖ. On an equation whose reduction is singular at the origin, its roots are the slopes of the tangent lines there.

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

The quadratic test in y at level m of Tate's algorithm: the quadratic Y² + (a₃/ϖ^m) Y − a₆/ϖ^(2m) has a root modulo ϖ, stated without dividing by ϖ as the existence of y divisible by ϖ^m with ϖ^(2m+1) ∣ y² + a₃ y − a₆. Tate's algorithm applies it at Step 5 (m = 1), at Step 8 (m = 2), and at the odd stages n = 2k + 1 of Step 7 (m = k + 2).

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

The quadratic test in x at level m of Tate's algorithm: the quadratic (a₂/ϖ) X² + (a₄/ϖ^(m+1)) X + a₆/ϖ^(2m+1) has a root modulo ϖ, stated without dividing by ϖ as the existence of x divisible by ϖ^m with ϖ^(2m+2) ∣ a₂ x² + a₄ x + a₆. Tate's algorithm applies it at the even stages n = 2k + 2 of Step 7 (m = k + 2).

def WeierstrassCurve.tateCubicRoots {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) : Set (R ⧸ Ideal.span {ϖ})

The roots of the residue cubic of Step 6 of Tate's algorithm: the classes t modulo ϖ of the t₀ with ϖ⁴ ∣ (ϖ t₀)³ + a₂ (ϖ t₀)² + a₄ (ϖ t₀) + a₆. On the normal form of Step 6 these are the roots of P(T) = T³ + (a₂/ϖ) T² + (a₄/ϖ²) T + a₆/ϖ³ (mem_tateCubicRoots_iff).

noncomputable def WeierstrassCurve.tateLocalIndex {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (ϖ : R) : TauCeti.ReductionSymbol → ℕ

The local index reported by Tate's algorithm when it stops on W, with uniformiser ϖ, at the symbol s (Silverman, Advanced Topics, IV.9): 1 at I₀, II and II*; 2 at III and III*; at Iₙ with n ≥ 1, n if the tangent quadratic splits and gcd(2, n) otherwise; at IV and IV*, 3 or 1 according as the quadratic of Step 5 or Step 8 has a root; at I₀*, one more than the number of roots of the residue cubic; at Iₙ* with n ≥ 1, 4 or 2 according as the quadratic at which Step 7 stops has a root.

The value is meaningful when W.IsTateTerminal ϖ s. Over a Henselian valuation ring with finite residue field it is the point-group index [E(K) : E₀(K)] (WeierstrassCurve.Affine.index_nonsingularReduction_eq_tateLocalIndex), so it does not depend on the equation on which the algorithm stops.

theorem WeierstrassCurve.hasTateTangentRoot_def {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.HasTateTangentRoot ϖ ↔ ∃ (t : R), ϖ ∣ t ^ 2 + W.a₁ * t - W.a₂

theorem WeierstrassCurve.hasTateYRoot_def {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {m : ℕ} : W.HasTateYRoot ϖ m ↔ ∃ (y : R), ϖ ^ m ∣ y ∧ ϖ ^ (2 * m + 1) ∣ y ^ 2 + W.a₃ * y - W.a₆

theorem WeierstrassCurve.hasTateXRoot_def {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {m : ℕ} : W.HasTateXRoot ϖ m ↔ ∃ (x : R), ϖ ^ m ∣ x ∧ ϖ ^ (2 * m + 2) ∣ W.a₂ * x ^ 2 + W.a₄ * x + W.a₆

theorem WeierstrassCurve.mem_tateCubicRoots {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} {t : R ⧸ Ideal.span {ϖ}} : t ∈ W.tateCubicRoots ϖ ↔ ∃ (t₀ : R), (Ideal.Quotient.mk (Ideal.span {ϖ})) t₀ = t ∧ ϖ ^ 4 ∣ (ϖ * t₀) ^ 3 + W.a₂ * (ϖ * t₀) ^ 2 + W.a₄ * (ϖ * t₀) + W.a₆

@[simp]

theorem WeierstrassCurve.tateLocalIndex_I_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.I 0) = 1

@[simp]

theorem WeierstrassCurve.tateLocalIndex_I_add_one_of_hasTateTangentRoot {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (h : W.HasTateTangentRoot ϖ) (n : ℕ) : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.I (n + 1)) = n + 1

@[simp]

theorem WeierstrassCurve.tateLocalIndex_I_add_one_of_not_hasTateTangentRoot {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (h : ¬W.HasTateTangentRoot ϖ) (n : ℕ) : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.I (n + 1)) = Nat.gcd 2 (n + 1)

@[simp]

theorem WeierstrassCurve.tateLocalIndex_I_one {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.I 1) = 1

At I₁ the local index is 1, whether or not the tangent quadratic splits.

@[simp]

theorem WeierstrassCurve.tateLocalIndex_II {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.tateLocalIndex ϖ TauCeti.ReductionSymbol.II = 1

@[simp]

theorem WeierstrassCurve.tateLocalIndex_III {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.tateLocalIndex ϖ TauCeti.ReductionSymbol.III = 2

@[simp]

theorem WeierstrassCurve.tateLocalIndex_IV_of_hasTateYRoot {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (h : W.HasTateYRoot ϖ 1) : W.tateLocalIndex ϖ TauCeti.ReductionSymbol.IV = 3

@[simp]

theorem WeierstrassCurve.tateLocalIndex_IV_of_not_hasTateYRoot {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (h : ¬W.HasTateYRoot ϖ 1) : W.tateLocalIndex ϖ TauCeti.ReductionSymbol.IV = 1

@[simp]

theorem WeierstrassCurve.tateLocalIndex_IStar_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.IStar 0) = 1 + Nat.card ↑(W.tateCubicRoots ϖ)

theorem WeierstrassCurve.tateLocalIndex_IStar_odd {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (k : ℕ) [Decidable (W.HasTateYRoot ϖ (k + 2))] : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.IStar (2 * k + 1)) = if W.HasTateYRoot ϖ (k + 2) then 4 else 2

At the odd stage n = 2k + 1 of Step 7, the test is the quadratic in y at level k + 2.

theorem WeierstrassCurve.tateLocalIndex_IStar_even {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (k : ℕ) [Decidable (W.HasTateXRoot ϖ (k + 2))] : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.IStar (2 * k + 2)) = if W.HasTateXRoot ϖ (k + 2) then 4 else 2

At the even stage n = 2k + 2 of Step 7, the test is the quadratic in x at level k + 2.

@[simp]

theorem WeierstrassCurve.tateLocalIndex_IVStar_of_hasTateYRoot {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (h : W.HasTateYRoot ϖ 2) : W.tateLocalIndex ϖ TauCeti.ReductionSymbol.IVStar = 3

@[simp]

theorem WeierstrassCurve.tateLocalIndex_IVStar_of_not_hasTateYRoot {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (h : ¬W.HasTateYRoot ϖ 2) : W.tateLocalIndex ϖ TauCeti.ReductionSymbol.IVStar = 1

@[simp]

theorem WeierstrassCurve.tateLocalIndex_IIIStar {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.tateLocalIndex ϖ TauCeti.ReductionSymbol.IIIStar = 2

@[simp]

theorem WeierstrassCurve.tateLocalIndex_IIStar {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} : W.tateLocalIndex ϖ TauCeti.ReductionSymbol.IIStar = 1

theorem WeierstrassCurve.tateLocalIndex_pos {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} (s : TauCeti.ReductionSymbol) : 0 < W.tateLocalIndex ϖ s

The local index is positive.

The residue polynomials

theorem WeierstrassCurve.hasTateYRoot_iff {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : ϖ ≠ 0) {m : ℕ} {b₃ b₆ : R} (h₃ : W.a₃ = ϖ ^ m * b₃) (h₆ : W.a₆ = ϖ ^ (2 * m) * b₆) : W.HasTateYRoot ϖ m ↔ ∃ (s : R), ϖ ∣ s ^ 2 + b₃ * s - b₆

The quadratic test in y is a root condition for the residue quadratic. If a₃ = ϖ^m b₃ and a₆ = ϖ^(2m) b₆, then W.HasTateYRoot ϖ m says that Y² + b₃ Y − b₆ has a root modulo ϖ.

theorem WeierstrassCurve.hasTateYRoot_iff_exists_residue_root {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} [IsLocalRing R] (hϖ : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}) (hϖ0 : ϖ ≠ 0) {m : ℕ} {b₃ b₆ : R} (h₃ : W.a₃ = ϖ ^ m * b₃) (h₆ : W.a₆ = ϖ ^ (2 * m) * b₆) : W.HasTateYRoot ϖ m ↔ ∃ (t : IsLocalRing.ResidueField R), t ^ 2 + (IsLocalRing.residue R) b₃ * t - (IsLocalRing.residue R) b₆ = 0

The quadratic test in y is a root condition over the residue field. If the maximal ideal of the local domain R is generated by ϖ ≠ 0, a₃ = ϖ^m b₃ and a₆ = ϖ^(2m) b₆, then W.HasTateYRoot ϖ m says that Y² + b₃ Y − b₆ has a root in the residue field of R.

theorem WeierstrassCurve.hasTateXRoot_iff {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : ϖ ≠ 0) {m : ℕ} {b₂ b₄ b₆ : R} (h₂ : W.a₂ = ϖ * b₂) (h₄ : W.a₄ = ϖ ^ (m + 1) * b₄) (h₆ : W.a₆ = ϖ ^ (2 * m + 1) * b₆) : W.HasTateXRoot ϖ m ↔ ∃ (s : R), ϖ ∣ b₂ * s ^ 2 + b₄ * s + b₆

The quadratic test in x is a root condition for the residue quadratic. If a₂ = ϖ b₂, a₄ = ϖ^(m+1) b₄ and a₆ = ϖ^(2m+1) b₆, then W.HasTateXRoot ϖ m says that b₂ X² + b₄ X + b₆ has a root modulo ϖ.

theorem WeierstrassCurve.hasTateXRoot_iff_exists_residue_root {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} [IsLocalRing R] (hϖ : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}) (hϖ0 : ϖ ≠ 0) {m : ℕ} {b₂ b₄ b₆ : R} (h₂ : W.a₂ = ϖ * b₂) (h₄ : W.a₄ = ϖ ^ (m + 1) * b₄) (h₆ : W.a₆ = ϖ ^ (2 * m + 1) * b₆) : W.HasTateXRoot ϖ m ↔ ∃ (t : IsLocalRing.ResidueField R), (IsLocalRing.residue R) b₂ * t ^ 2 + (IsLocalRing.residue R) b₄ * t + (IsLocalRing.residue R) b₆ = 0

The quadratic test in x is a root condition over the residue field. If the maximal ideal of the local domain R is generated by ϖ ≠ 0, a₂ = ϖ b₂, a₄ = ϖ^(m+1) b₄ and a₆ = ϖ^(2m+1) b₆, then W.HasTateXRoot ϖ m says that b₂ X² + b₄ X + b₆ has a root in the residue field of R.

theorem WeierstrassCurve.hasTateTangentRoot_iff_exists_residue_root {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {ϖ : R} [IsLocalRing R] (hϖ : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}) : W.HasTateTangentRoot ϖ ↔ ∃ (t : IsLocalRing.ResidueField R), t ^ 2 + (IsLocalRing.residue R) W.a₁ * t - (IsLocalRing.residue R) W.a₂ = 0

The tangent test is a root condition over the residue field. If the maximal ideal of the local ring R is generated by ϖ, then W.HasTateTangentRoot ϖ says that the tangent quadratic T² + a₁ T − a₂ has a root in the residue field of R.

theorem WeierstrassCurve.mk_mem_tateCubicRoots_iff {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : ϖ ≠ 0) {b₂ b₄ b₆ : R} (h₂ : W.a₂ = ϖ * b₂) (h₄ : W.a₄ = ϖ ^ 2 * b₄) (h₆ : W.a₆ = ϖ ^ 3 * b₆) (t₀ : R) : (Ideal.Quotient.mk (Ideal.span {ϖ})) t₀ ∈ W.tateCubicRoots ϖ ↔ ϖ ∣ t₀ ^ 3 + b₂ * t₀ ^ 2 + b₄ * t₀ + b₆

The residue cubic test on a representative. If a₂ = ϖ b₂, a₄ = ϖ² b₄ and a₆ = ϖ³ b₆, as on the normal form of Step 6, then the class of t₀ is a root of the residue cubic exactly when ϖ ∣ t₀³ + b₂ t₀² + b₄ t₀ + b₆.

theorem WeierstrassCurve.mem_tateCubicRoots_iff {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : ϖ ≠ 0) {b₂ b₄ b₆ : R} (h₂ : W.a₂ = ϖ * b₂) (h₄ : W.a₄ = ϖ ^ 2 * b₄) (h₆ : W.a₆ = ϖ ^ 3 * b₆) (t : R ⧸ Ideal.span {ϖ}) : t ∈ W.tateCubicRoots ϖ ↔ (Polynomial.X ^ 3 + Polynomial.C ((Ideal.Quotient.mk (Ideal.span {ϖ})) b₂) * Polynomial.X ^ 2 + Polynomial.C ((Ideal.Quotient.mk (Ideal.span {ϖ})) b₄) * Polynomial.X + Polynomial.C ((Ideal.Quotient.mk (Ideal.span {ϖ})) b₆)).IsRoot t

The roots of the residue cubic. If a₂ = ϖ b₂, a₄ = ϖ² b₄ and a₆ = ϖ³ b₆, as on the normal form of Step 6, then W.tateCubicRoots ϖ is the set of roots in R ⧸ (ϖ) of the cubic T³ + b₂ T² + b₄ T + b₆.

theorem WeierstrassCurve.natCard_tateCubicRoots_eq {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} [IsLocalRing R] (hϖ : IsLocalRing.maximalIdeal R = Ideal.span {ϖ}) (hϖ0 : ϖ ≠ 0) {b₂ b₄ b₆ : R} (h₂ : W.a₂ = ϖ * b₂) (h₄ : W.a₄ = ϖ ^ 2 * b₄) (h₆ : W.a₆ = ϖ ^ 3 * b₆) : Nat.card ↑(W.tateCubicRoots ϖ) = Nat.card ↑{t : IsLocalRing.ResidueField R | t ^ 3 + (IsLocalRing.residue R) b₂ * t ^ 2 + (IsLocalRing.residue R) b₄ * t + (IsLocalRing.residue R) b₆ = 0}

The roots of the residue cubic, counted in the residue field. If the maximal ideal of the local domain R is generated by ϖ ≠ 0, a₂ = ϖ b₂, a₄ = ϖ² b₄ and a₆ = ϖ³ b₆, then W.tateCubicRoots ϖ has as many elements as the set of roots of T³ + b₂ T² + b₄ T + b₆ in the residue field of R.

theorem WeierstrassCurve.natCard_tateCubicRoots_le {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : Prime ϖ) : Nat.card ↑(W.tateCubicRoots ϖ) ≤ 3

The residue cubic has at most three roots when ϖ is prime. On the normal form of Step 6 these are the roots of the monic cubic of mem_tateCubicRoots_iff.

theorem WeierstrassCurve.IsTateTerminal.tateLocalIndex_le_componentCount {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : Prime ϖ) {s : TauCeti.ReductionSymbol} (h : W.IsTateTerminal ϖ s) : W.tateLocalIndex ϖ s ≤ s.componentCount

The local index is at most the number of components. At each symbol s at which Tate's algorithm stops, the local index is at most the component count m of s.

theorem WeierstrassCurve.IsTateTerminal.tateLocalIndex_le_four {R : Type u_1} [CommRing R] [IsDomain R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : Prime ϖ) {s : TauCeti.ReductionSymbol} (h : W.IsTateTerminal ϖ s) (hs : ∀ (n : ℕ), s ≠ TauCeti.ReductionSymbol.I n) : W.tateLocalIndex ϖ s ≤ 4

The local index is at most 4 at additive reduction. At each symbol other than the Iₙ at which Tate's algorithm stops, the local index is at most 4.

The split test over a discrete valuation ring

theorem WeierstrassCurve.hasTateTangentRoot_iff_splits {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {W : WeierstrassCurve R} {ϖ : R} (hϖ : Irreducible ϖ) : W.HasTateTangentRoot ϖ ↔ (Polynomial.X ^ 2 + Polynomial.C ((IsLocalRing.residue R) W.a₁) * Polynomial.X - Polynomial.C ((IsLocalRing.residue R) W.a₂)).Splits

The tangent test is the splitting of the tangent quadratic over the residue field: over a discrete valuation ring with uniformiser ϖ, T² + a₁ T − a₂ has a root modulo ϖ exactly when its reduction splits over the residue field.

theorem WeierstrassCurve.IsTateTerminal.tateLocalIndex_of_hasSplitMultiplicativeReduction {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve R} {ϖ : R} (hϖ : Irreducible ϖ) {n : ℕ} (h : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.I (n + 1))) (hs : HasSplitMultiplicativeReduction R (W.baseChange K)) : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.I (n + 1)) = n + 1

At split multiplicative reduction, the local index of Iₙ is n. On an equation at which Tate's algorithm stops at Iₙ with n ≥ 1.

theorem WeierstrassCurve.IsTateTerminal.tateLocalIndex_of_not_hasSplitMultiplicativeReduction {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {W : WeierstrassCurve R} {ϖ : R} (hϖ : Irreducible ϖ) {n : ℕ} (h : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.I (n + 1))) (hs : ¬HasSplitMultiplicativeReduction R (W.baseChange K)) : W.tateLocalIndex ϖ (TauCeti.ReductionSymbol.I (n + 1)) = Nat.gcd 2 (n + 1)

At nonsplit multiplicative reduction, the local index of Iₙ is gcd(2, n). On an equation at which Tate's algorithm stops at Iₙ with n ≥ 1.