The L-function of a Weierstrass curve

In this file, we define the L-function of a Weierstrass curve.

Main definitions

• WeierstrassCurve.LFunction: the L-function of a Weierstrass equation.

References

• J Silverman, The Arithmetic of Elliptic Curves

noncomputable def WeierstrassCurve.localPolynomial (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : Polynomial ℤ

The local polynomial associated to a Weierstrass curve W over a nonarchimedean local field. In the case of good reduction it is given by 1 - a T + q T ^ 2 where q is the cardinality of the residue field κ and a = q + 1 - |W(κ)|. Note that q (and also |W(κ)|) is defined via Nat.card, so q has junk value 0 when the residue field is infinite.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def WeierstrassCurve.localPowerSeries (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : PowerSeries ℤ

The local power series associated to a Weierstrass curve over a nonarchimedean local field.

Equations

• WeierstrassCurve.localPowerSeries R W = (↑(WeierstrassCurve.localPolynomial R W)).invOfUnit 1

noncomputable def WeierstrassCurve.localEulerFactor (R : Type u_1) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve K) : ArithmeticFunction ℤ

The local Euler factor associated to a Weierstrass curve over a nonarchimedean local field.

Equations

• WeierstrassCurve.localEulerFactor R W = (ArithmeticFunction.ofPowerSeries (Nat.card (IsLocalRing.ResidueField R))) (WeierstrassCurve.localPowerSeries R W)

noncomputable def WeierstrassCurve.LFunction {K : Type u_1} [Field K] [NumberField K] (W : WeierstrassCurve K) : ArithmeticFunction ℤ

The L-function of a Weierstrass curve W over a number field K as a formal Dirichlet series.

For each prime ideal p of the ring of integers of K with norm ‖p‖ residue field κ_p, we define the local polynomial fₚ(T) as:

• fₚ = 1 - aₚ T + ‖p‖ T ^ 2 where aₚ = ‖p‖ + 1 - |W(κ_p)| if W has good reduction at p,
• fₚ = 1 - T if W has split multiplicative reduction at p,
• fₚ = 1 + T if W has nonsplit multiplicative reduction at p,
• fₚ = 1 if W has additive reduction at p. Then the L-function of W is the formal Dirichlet series defined as the product of 1 / fₚ(‖p‖⁻ˢ) as p ranges over all prime ideals of the ring of integers of K.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def WeierstrassCurve.LSeries {K : Type u_1} [Field K] [NumberField K] (W : WeierstrassCurve K) (s : ℂ) : ℂ

The L-series of a Weierstrass curve over a number field.

Equations

• W.LSeries s = LSeries (Int.cast ∘ ⇑W.LFunction) s