The reduction type read off Tate's algorithm, and semistability

Let R be a discrete valuation ring with uniformiser ϖ and fraction field K, and let W be a Weierstrass equation over R on which Tate's algorithm stops with symbol s (WeierstrassCurve.IsTateTerminal). Such an equation is minimal over K (WeierstrassCurve.IsTateTerminal.isMinimal_baseChange), and this file shows that s determines the reduction type of W in Mathlib's good/multiplicative/additive trichotomy:

• the reduction is good exactly when s = I₀;
• it is multiplicative exactly when s = Iₙ with n ≥ 1, and then n is the valuation of the minimal discriminant, and the reduction is split exactly when the tangent quadratic T² + a₁ T − a₂ splits over the residue field;
• it is additive exactly when s is none of the Iₙ.

The additive symbols are recognised by divisibilities alone: at each of them ϖ divides b₂, a₃, a₄ and a₆, hence c₄ and Δ (WeierstrassCurve.IsTateTerminal.dvd_c₄ and WeierstrassCurve.IsTateTerminal.dvd_Δ_iff). At Iₙ with n ≥ 1 the reduction is singular at the origin and the stopping test asks for ϖ ∤ b₂, which is Tate's test for multiplicative reduction (WeierstrassCurve.hasMultiplicativeReduction_iff_reduction_b₂_ne_zero).

Over a Dedekind domain O with fraction field F, an elliptic curve is semistable (WeierstrassCurve.IsSemistable) exactly when, at every height-one prime v, Tate's algorithm run on an equation of the curve over the localisation O_v stops at some Iₙ whenever it stops; the reverse direction needs the residue fields to be perfect, so that the algorithm runs at all.

Main results

• WeierstrassCurve.IsTateTerminal.hasGoodReduction_iff, WeierstrassCurve.IsTateTerminal.hasMultiplicativeReduction_iff and WeierstrassCurve.IsTateTerminal.hasAdditiveReduction_iff: the reduction type of an equation from the symbol at which the algorithm stops on it.
• WeierstrassCurve.IsTateTerminal.hasGoodReduction_minimal_iff, WeierstrassCurve.IsTateTerminal.hasMultiplicativeReduction_minimal_iff and WeierstrassCurve.IsTateTerminal.hasAdditiveReduction_minimal_iff: the same, for Mathlib's chosen minimal equation E.minimal R of a curve E with a minimal equation on which the algorithm stops.
• WeierstrassCurve.IsTateTerminal.hasGoodReduction_minimal_baseChange_iff, WeierstrassCurve.IsTateTerminal.hasMultiplicativeReduction_minimal_baseChange_iff and WeierstrassCurve.IsTateTerminal.hasAdditiveReduction_minimal_baseChange_iff: the same, for an equation defined over a ring mapping into R, such as an equation over ℤ.
• WeierstrassCurve.IsTateTerminal.hasSplitMultiplicativeReduction_iff: at Iₙ with n ≥ 1, the split test.
• WeierstrassCurve.IsTateTerminal.localMinimalDiscriminantValuation_eq: at Iₙ, n is the valuation of the minimal discriminant.
• WeierstrassCurve.IsSemistable.exists_eq_I_of_isTateTerminal and WeierstrassCurve.isSemistable_iff_forall_isTateTerminal: a curve over the fraction field of a Dedekind domain is semistable exactly when Tate's algorithm only ever stops at symbols Iₙ.

References

• J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, GTM 151, IV.9.
• J. H. Silverman, The Arithmetic of Elliptic Curves, GTM 106, VII.5.
• 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.IsTateTerminal.hasGoodReduction_iff {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} {s : TauCeti.ReductionSymbol} (hϖ : Irreducible ϖ) (h : W.IsTateTerminal ϖ s) : HasGoodReduction R (W.baseChange K) ↔ s = TauCeti.ReductionSymbol.I 0

Tate's algorithm detects good reduction. If the algorithm stops on W at s, the reduction is good exactly when s = I₀.

theorem WeierstrassCurve.IsTateTerminal.hasSplitMultiplicativeReduction_iff {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))) : HasSplitMultiplicativeReduction R (W.baseChange K) ↔ (Polynomial.X ^ 2 + Polynomial.C ((IsLocalRing.residue R) W.a₁) * Polynomial.X - Polynomial.C ((IsLocalRing.residue R) W.a₂)).Splits

Tate's split test. If the algorithm stops on W at Iₙ with n ≥ 1, the reduction is split multiplicative exactly when the tangent quadratic T² + a₁ T − a₂ splits over the residue field.

theorem WeierstrassCurve.IsTateTerminal.hasMultiplicativeReduction_iff {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} {s : TauCeti.ReductionSymbol} (hϖ : Irreducible ϖ) (h : W.IsTateTerminal ϖ s) : HasMultiplicativeReduction R (W.baseChange K) ↔ ∃ (n : ℕ), s = TauCeti.ReductionSymbol.I (n + 1)

Tate's algorithm detects multiplicative reduction. If the algorithm stops on W at s, the reduction is multiplicative exactly when s = Iₙ for some n ≥ 1.

theorem WeierstrassCurve.IsTateTerminal.hasAdditiveReduction_iff {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} {s : TauCeti.ReductionSymbol} (hϖ : Irreducible ϖ) (h : W.IsTateTerminal ϖ s) : HasAdditiveReduction R (W.baseChange K) ↔ ∀ (n : ℕ), s ≠ TauCeti.ReductionSymbol.I n

Tate's algorithm detects additive reduction. If the algorithm stops on W at s, the reduction is additive exactly when s is none of the Iₙ.

theorem WeierstrassCurve.IsTateTerminal.not_hasAdditiveReduction_iff {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} {s : TauCeti.ReductionSymbol} (hϖ : Irreducible ϖ) (h : W.IsTateTerminal ϖ s) : ¬HasAdditiveReduction R (W.baseChange K) ↔ ∃ (n : ℕ), s = TauCeti.ReductionSymbol.I n

If Tate's algorithm stops on W at s, the reduction is good or multiplicative exactly when s = Iₙ for some n.

The symbol at which the algorithm stops on one minimal equation of a curve E decides the reduction type of Mathlib's chosen minimal equation E.minimal R.

theorem WeierstrassCurve.IsTateTerminal.hasGoodReduction_minimal_iff {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} {s : TauCeti.ReductionSymbol} {E : WeierstrassCurve K} (D : VariableChange K) (hD : D • E = W.baseChange K) (hϖ : Irreducible ϖ) (h : W.IsTateTerminal ϖ s) : HasGoodReduction R (minimal R E) ↔ s = TauCeti.ReductionSymbol.I 0

Tate's algorithm detects good reduction of the chosen minimal equation. If a change of variables carries E to a minimal equation on which the algorithm stops at s, then E.minimal R has good reduction exactly when s = I₀.

theorem WeierstrassCurve.IsTateTerminal.hasAdditiveReduction_minimal_iff {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} {s : TauCeti.ReductionSymbol} {E : WeierstrassCurve K} [E.IsElliptic] (D : VariableChange K) (hD : D • E = W.baseChange K) (hϖ : Irreducible ϖ) (h : W.IsTateTerminal ϖ s) : HasAdditiveReduction R (minimal R E) ↔ ∀ (n : ℕ), s ≠ TauCeti.ReductionSymbol.I n

Tate's algorithm detects additive reduction of the chosen minimal equation. If a change of variables carries the elliptic curve E to a minimal equation on which the algorithm stops at s, then E.minimal R has additive reduction exactly when s is none of the Iₙ.

theorem WeierstrassCurve.IsTateTerminal.hasMultiplicativeReduction_minimal_iff {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} {s : TauCeti.ReductionSymbol} {E : WeierstrassCurve K} [E.IsElliptic] (D : VariableChange K) (hD : D • E = W.baseChange K) (hϖ : Irreducible ϖ) (h : W.IsTateTerminal ϖ s) : HasMultiplicativeReduction R (minimal R E) ↔ ∃ (n : ℕ), s = TauCeti.ReductionSymbol.I (n + 1)

Tate's algorithm detects multiplicative reduction of the chosen minimal equation. If a change of variables carries the elliptic curve E to a minimal equation on which the algorithm stops at s, then E.minimal R has multiplicative reduction exactly when s = Iₙ with n ≥ 1.

The same for an equation W₀ over a ring A mapping into R, such as an equation over ℤ, when a change of variables over R carries it to an equation on which the algorithm stops.

theorem WeierstrassCurve.IsTateTerminal.hasGoodReduction_minimal_baseChange_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {ϖ : R} {s : TauCeti.ReductionSymbol} {A : Type u_3} [CommRing A] [Algebra A K] {φ : A →+* R} {W₀ : WeierstrassCurve A} (hφ : (algebraMap R K).comp φ = algebraMap A K) (C : VariableChange R) (hϖ : Irreducible ϖ) (h : (C • W₀.map φ).IsTateTerminal ϖ s) : HasGoodReduction R (minimal R (W₀.baseChange K)) ↔ s = TauCeti.ReductionSymbol.I 0

Tate's algorithm, run on an equation over a ring mapping into R, detects good reduction of its chosen minimal equation. Let W₀ be an equation over A, mapped into R by φ compatibly with K. If a change of variables C over R carries it to an equation on which the algorithm stops at s, then (W₀.baseChange K).minimal R has good reduction exactly when s = I₀.

theorem WeierstrassCurve.IsTateTerminal.hasMultiplicativeReduction_minimal_baseChange_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {ϖ : R} {s : TauCeti.ReductionSymbol} {A : Type u_3} [CommRing A] [Algebra A K] {φ : A →+* R} {W₀ : WeierstrassCurve A} [(W₀.baseChange K).IsElliptic] (hφ : (algebraMap R K).comp φ = algebraMap A K) (C : VariableChange R) (hϖ : Irreducible ϖ) (h : (C • W₀.map φ).IsTateTerminal ϖ s) : HasMultiplicativeReduction R (minimal R (W₀.baseChange K)) ↔ ∃ (n : ℕ), s = TauCeti.ReductionSymbol.I (n + 1)

Tate's algorithm, run on an equation over a ring mapping into R, detects multiplicative reduction of its chosen minimal equation. Let W₀ be an equation over A, mapped into R by φ compatibly with K. If a change of variables C over R carries it to an equation on which the algorithm stops at s, then (W₀.baseChange K).minimal R has multiplicative reduction exactly when s = Iₙ with n ≥ 1.

theorem WeierstrassCurve.IsTateTerminal.hasAdditiveReduction_minimal_baseChange_iff {R : Type u_1} [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {ϖ : R} {s : TauCeti.ReductionSymbol} {A : Type u_3} [CommRing A] [Algebra A K] {φ : A →+* R} {W₀ : WeierstrassCurve A} [(W₀.baseChange K).IsElliptic] (hφ : (algebraMap R K).comp φ = algebraMap A K) (C : VariableChange R) (hϖ : Irreducible ϖ) (h : (C • W₀.map φ).IsTateTerminal ϖ s) : HasAdditiveReduction R (minimal R (W₀.baseChange K)) ↔ ∀ (n : ℕ), s ≠ TauCeti.ReductionSymbol.I n

Tate's algorithm, run on an equation over a ring mapping into R, detects additive reduction of its chosen minimal equation. Let W₀ be an equation over A, mapped into R by φ compatibly with K. If a change of variables C over R carries it to an equation on which the algorithm stops at s, then (W₀.baseChange K).minimal R has additive reduction exactly when s is none of the Iₙ.

theorem WeierstrassCurve.IsTateTerminal.localMinimalDiscriminantValuation_eq {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} [(W.baseChange K).IsElliptic] (hϖ : Irreducible ϖ) {n : ℕ} (h : W.IsTateTerminal ϖ (TauCeti.ReductionSymbol.I n)) : localMinimalDiscriminantValuation R (W.baseChange K) = n

At Iₙ, the index is the valuation of the minimal discriminant.

Semistability over a Dedekind domain

theorem WeierstrassCurve.IsSemistable.exists_eq_I_of_isTateTerminal {O : Type u_1} [CommRing O] [IsDedekindDomain O] {F : Type u_2} [Field F] [Algebra O F] [IsFractionRing O F] {W : WeierstrassCurve F} [W.IsElliptic] (h : IsSemistable O W) (v : IsDedekindDomain.HeightOneSpectrum O) {W' : WeierstrassCurve (Localization.AtPrime v.asIdeal)} (D : VariableChange F) (hD : D • W = W'.baseChange F) {ϖ : Localization.AtPrime v.asIdeal} (hϖ : Irreducible ϖ) {s : TauCeti.ReductionSymbol} (hs : W'.IsTateTerminal ϖ s) : ∃ (n : ℕ), s = TauCeti.ReductionSymbol.I n

On a semistable curve, Tate's algorithm only stops at symbols Iₙ. At a height-one prime v, let W' be an equation over the localisation O_v of the curve, and suppose Tate's algorithm, run with a uniformiser ϖ, stops on W' at s. Then s = Iₙ for some n.

theorem WeierstrassCurve.isSemistable_iff_forall_isTateTerminal {O : Type u_1} [CommRing O] [IsDedekindDomain O] {F : Type u_2} [Field F] [Algebra O F] [IsFractionRing O F] {W : WeierstrassCurve F} [W.IsElliptic] [∀ (v : IsDedekindDomain.HeightOneSpectrum O), PerfectField (IsLocalRing.ResidueField (Localization.AtPrime v.asIdeal))] : IsSemistable O W ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum O) (W' : WeierstrassCurve (Localization.AtPrime v.asIdeal)) (D : VariableChange F) (ϖ : Localization.AtPrime v.asIdeal) (s : TauCeti.ReductionSymbol), D • W = W'.baseChange F → Irreducible ϖ → W'.IsTateTerminal ϖ s → ∃ (n : ℕ), s = TauCeti.ReductionSymbol.I n

Semistability is read off Tate's algorithm. Over a Dedekind domain whose localisations at height-one primes have perfect residue fields, an elliptic curve is semistable exactly when, at every height-one prime v, Tate's algorithm run on any equation of the curve over O_v, with any uniformiser, stops at some Iₙ whenever it stops.