Reduction symbols in Tate's algorithm

This file defines the output symbols of Tate's algorithm and the component count attached to each symbol. The count is the input to the algorithmic Ogg exponent.

The family I n includes I 0 (good reduction) and I n for positive n; IStar n includes I₀* at n = 0 and Iₙ* for positive n.

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.

inductive TauCeti.ReductionSymbol : Type

The reduction symbols output by Tate's algorithm. The parameterized families encode Iₙ and Iₙ*; their zero cases are I₀ and I₀*.

• I (n : ℕ) : ReductionSymbol

  The Iₙ family, with I₀ denoting good reduction.

• II : ReductionSymbol

  The additive reduction symbol II.

• III : ReductionSymbol

  The additive reduction symbol III.

• IV : ReductionSymbol

  The additive reduction symbol IV.

• IStar (n : ℕ) : ReductionSymbol

  The additive family Iₙ*, with I₀* at n = 0.

• IVStar : ReductionSymbol

  The additive reduction symbol IV*.

• IIIStar : ReductionSymbol

  The additive reduction symbol III*.

• IIStar : ReductionSymbol

  The additive reduction symbol II*.

def TauCeti.instDecidableEqReductionSymbol.decEq (x✝ x✝¹ : ReductionSymbol) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TauCeti.instDecidableEqReductionSymbol : DecidableEq ReductionSymbol

def TauCeti.instReprReductionSymbol.repr : ReductionSymbol → ℕ → Std.Format

@[instance_reducible]

instance TauCeti.instReprReductionSymbol : Repr ReductionSymbol

def TauCeti.ReductionSymbol.componentCount : ReductionSymbol → ℕ

The number of geometric irreducible components specified by a reduction symbol.

@[simp]

theorem TauCeti.ReductionSymbol.componentCount_I (n : ℕ) : (I n).componentCount = max 1 n

@[simp]

theorem TauCeti.ReductionSymbol.componentCount_II : II.componentCount = 1

@[simp]

theorem TauCeti.ReductionSymbol.componentCount_III : III.componentCount = 2

@[simp]

theorem TauCeti.ReductionSymbol.componentCount_IV : IV.componentCount = 3

@[simp]

theorem TauCeti.ReductionSymbol.componentCount_IStar (n : ℕ) : (IStar n).componentCount = n + 5

@[simp]

theorem TauCeti.ReductionSymbol.componentCount_IVStar : IVStar.componentCount = 7

@[simp]

theorem TauCeti.ReductionSymbol.componentCount_IIIStar : IIIStar.componentCount = 8

@[simp]

theorem TauCeti.ReductionSymbol.componentCount_IIStar : IIStar.componentCount = 9

theorem TauCeti.ReductionSymbol.componentCount_pos (symbol : ReductionSymbol) : 0 < symbol.componentCount

Every reduction symbol has at least one component.

def TauCeti.ReductionSymbol.algorithmicOggExponent (symbol : ReductionSymbol) (vΔ : ℕ) : ℤ

The algorithmic Ogg exponent attached to a symbol and a minimal discriminant valuation vΔ: vΔ - m + 1, where m is the component count. It is integer-valued so that the formula remains exact for arbitrary inputs; when the symbol and equation come from Tate's algorithm, its branch conditions ensure this exponent is nonnegative.

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_def (symbol : ReductionSymbol) (vΔ : ℕ) : symbol.algorithmicOggExponent vΔ = ↑vΔ - ↑symbol.componentCount + 1

The exponent is the discriminant valuation minus the component count plus one.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_I_zero (vΔ : ℕ) : (I 0).algorithmicOggExponent vΔ = ↑vΔ

The good reduction symbol I₀ has Ogg exponent vΔ; in particular it is zero at valuation zero.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_I {n : ℕ} (hn : n ≠ 0) (vΔ : ℕ) : (I n).algorithmicOggExponent vΔ = ↑vΔ - ↑n + 1

A multiplicative symbol Iₙ, n ≠ 0, has Ogg exponent vΔ - n + 1; in particular it is one when the minimal discriminant valuation is n.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_II (vΔ : ℕ) : II.algorithmicOggExponent vΔ = ↑vΔ

The additive symbol II has Ogg exponent vΔ.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_III (vΔ : ℕ) : III.algorithmicOggExponent vΔ = ↑vΔ - 1

The additive symbol III has Ogg exponent vΔ - 1.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_IV (vΔ : ℕ) : IV.algorithmicOggExponent vΔ = ↑vΔ - 2

The additive symbol IV has Ogg exponent vΔ - 2.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_IStar (n vΔ : ℕ) : (IStar n).algorithmicOggExponent vΔ = ↑vΔ - ↑n - 4

The additive symbol Iₙ* has Ogg exponent vΔ - n - 4.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_IVStar (vΔ : ℕ) : IVStar.algorithmicOggExponent vΔ = ↑vΔ - 6

The additive symbol IV* has Ogg exponent vΔ - 6.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_IIIStar (vΔ : ℕ) : IIIStar.algorithmicOggExponent vΔ = ↑vΔ - 7

The additive symbol III* has Ogg exponent vΔ - 7.

@[simp]

theorem TauCeti.ReductionSymbol.algorithmicOggExponent_IIStar (vΔ : ℕ) : IIStar.algorithmicOggExponent vΔ = ↑vΔ - 8

The additive symbol II* has Ogg exponent vΔ - 8.