The index of E₀ is finite and bounded

Let v be a valuation on a field F whose valuation ring O is Henselian with maximal ideal generated by ϖ, and let W be an integral Weierstrass equation over F. The points with nonsingular reduction form the subgroup E₀(F) of W(F) (WeierstrassCurve.Affine.nonsingularReduction). This file proves that when Tate's algorithm stops on the integral model at a reduction symbol s, the quotient W(F) / E₀(F) is finite, of order at most the number m of components of s (TauCeti.ReductionSymbol.componentCount), and of order at most 4 unless s is a multiplicative symbol Iₙ with split tangent quadratic.

These are read off the point-index theorems for the individual symbols. None of them needs the residue field to be perfect or finite: at III and at nonsplit Iₙ only an upper bound on the index is used, and that bound holds over any residue field.

For an elliptic curve given by a minimal equation over a Henselian discrete valuation ring with perfect residue field, Tate's algorithm stops after a change of variables over O, which does not change the index. This gives the theorem of Kodaira and Néron (Silverman, The Arithmetic of Elliptic Curves, VII.6.1): E(F) / E₀(F) is finite, and of order at most 4 unless the reduction is split multiplicative, where its order is v(Δ_min) (WeierstrassCurve.Affine.index_nonsingularReduction_eq_localMinimalDiscriminantValuation).

The bound by the component count of the symbol is the form in which the index enters the criterion of Néron, Ogg and Shafarevich (Silverman VII.7.1). There the full n-torsion of a curve with bad reduction forces n to divide [E(F) : E₀(F)] (WeierstrassCurve.Affine.Point.dvd_index_nonsingularReduction) over unramified extensions of F of growing degree. Such an extension keeps ϖ as a uniformiser, so the stopping conditions of Tate's algorithm, which are divisibilities by powers of ϖ, transfer to it (WeierstrassCurve.isTateTerminal_map_iff), and the bound by the component count of the symbol does not grow with the extension.

Main results

• WeierstrassCurve.Affine.finiteIndex_nonsingularReduction_of_isTateTerminal: if Tate's algorithm stops on the integral model, E₀(F) has finite index in W(F).
• WeierstrassCurve.Affine.index_nonsingularReduction_le_componentCount: the index is at most the number of components of the symbol at which the algorithm stops.
• WeierstrassCurve.Affine.index_nonsingularReduction_le_four_of_isTateTerminal: the index is at most 4 unless the algorithm stops at Iₙ with split tangent quadratic.
• WeierstrassCurve.Affine.finiteIndex_nonsingularReduction: the instance that, for an elliptic curve given by a minimal equation over a Henselian discrete valuation ring with perfect residue field, E₀(F) has finite index in E(F).
• WeierstrassCurve.Affine.index_nonsingularReduction_le_four: for such a curve without split multiplicative reduction, the index is at most 4.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, GTM 106, 2nd ed., VII.6.1 and VII.7.1.
• J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, GTM 151, IV.9.

theorem WeierstrassCurve.Affine.finiteIndex_nonsingularReduction_of_isTateTerminal {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [DecidableEq F] [HenselianLocalRing ↥v.valuationSubring] {ϖ : ↥v.valuationSubring} (hϖ : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {ϖ}) {s : TauCeti.ReductionSymbol} (h : (integralModel (↥v.valuationSubring) W).IsTateTerminal ϖ s) : (nonsingularReduction v W).FiniteIndex

E₀ has finite index wherever Tate's algorithm stops. If ϖ generates the maximal ideal of the Henselian valuation ring and Tate's algorithm stops on the integral model of W, then the subgroup E₀(F) of points with nonsingular reduction has finite index in W(F).

theorem WeierstrassCurve.Affine.index_nonsingularReduction_le_componentCount {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [DecidableEq F] [HenselianLocalRing ↥v.valuationSubring] {ϖ : ↥v.valuationSubring} (hϖ : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {ϖ}) {s : TauCeti.ReductionSymbol} (h : (integralModel (↥v.valuationSubring) W).IsTateTerminal ϖ s) : (nonsingularReduction v W).index ≤ s.componentCount

The index of E₀ is at most the number of components. If ϖ generates the maximal ideal of the Henselian valuation ring and Tate's algorithm stops on the integral model of W at the symbol s, then [W(F) : E₀(F)] is at most the number of components of s. The bound depends only on s, not on the residue field.

theorem WeierstrassCurve.Affine.index_nonsingularReduction_le_four_of_isTateTerminal {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) {W : Affine F} [IsIntegral (↥v.valuationSubring) W] [DecidableEq F] [HenselianLocalRing ↥v.valuationSubring] {ϖ : ↥v.valuationSubring} (hϖ : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {ϖ}) {s : TauCeti.ReductionSymbol} (h : (integralModel (↥v.valuationSubring) W).IsTateTerminal ϖ s) (hs : ∀ (n : ℕ), s = TauCeti.ReductionSymbol.I (n + 1) → ¬(integralModel (↥v.valuationSubring) W).HasTateTangentRoot ϖ) : (nonsingularReduction v W).index ≤ 4

The index of E₀ is at most 4 away from split multiplicative reduction. If ϖ generates the maximal ideal of the Henselian valuation ring, Tate's algorithm stops on the integral model of W at the symbol s, and s is not a symbol Iₙ with n ≥ 1 whose tangent quadratic T² + a₁ T − a₂ has a root modulo ϖ, then [W(F) : E₀(F)] ≤ 4.

Minimal equations over a Henselian discrete valuation ring

instance WeierstrassCurve.Affine.finiteIndex_nonsingularReduction {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) [IsDiscreteValuationRing ↥v.valuationSubring] [PerfectField (IsLocalRing.ResidueField ↥v.valuationSubring)] (E : WeierstrassCurve F) [E.IsElliptic] [IsMinimal (↥v.valuationSubring) E] [DecidableEq F] [HenselianLocalRing ↥v.valuationSubring] : (nonsingularReduction v E.toAffine).FiniteIndex

E(F) / E₀(F) is finite (Kodaira, Néron; Silverman, The Arithmetic of Elliptic Curves, VII.6.1). Let the valuation ring of v be a Henselian discrete valuation ring with perfect residue field, and let E be an elliptic curve over F given by a minimal equation. Then the subgroup E₀(F) of points with nonsingular reduction has finite index in E(F).

theorem WeierstrassCurve.Affine.index_nonsingularReduction_le_four {F : Type u_1} {Γ₀ : Type u_2} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) [IsDiscreteValuationRing ↥v.valuationSubring] [PerfectField (IsLocalRing.ResidueField ↥v.valuationSubring)] (E : WeierstrassCurve F) [E.IsElliptic] [IsMinimal (↥v.valuationSubring) E] [DecidableEq F] [HenselianLocalRing ↥v.valuationSubring] (hE : ¬HasSplitMultiplicativeReduction (↥v.valuationSubring) E) : (nonsingularReduction v E.toAffine).index ≤ 4

E(F) / E₀(F) has order at most 4 away from split multiplicative reduction (Kodaira, Néron; Silverman, The Arithmetic of Elliptic Curves, VII.6.1). Let the valuation ring of v be a Henselian discrete valuation ring with perfect residue field, and let E be an elliptic curve over F given by a minimal equation whose reduction is not split multiplicative. Then [E(F) : E₀(F)] ≤ 4. At split multiplicative reduction the index is instead v(Δ_min) (WeierstrassCurve.Affine.index_nonsingularReduction_eq_localMinimalDiscriminantValuation).