Modularity conjecture

The Modularity conjecture (also know as the Shimura--Taniyama--Weil conjecture) states that every rational elliptic curve is modular, meaning that it can be associated with a modular form. We state the a_p version of the conjecture, which relates the coefficients of the modular form to the number of points on the elliptic curve over finite fields.

Since we don't have the conductor of the elliptic curve, our definition of a_p(E) differs from that in the literature at primes of bad reduction. For this reason, we state the conjecture with the assumption that p ∤ N, in order to give an equivalent statement.

References:

• Wikipedia
• [F. Diamond and J. Shurman, A First Course in Modular Forms][diamondshurman2005]

def ModularityConjecture.modularFormAn (n : ℕ) {N : ℕ} {k : ℤ} (f : CuspForm (CongruenceSubgroup.Gamma0 N) k) : ℂ

The n-th Fourier coefficient of a modular forms (around the cusp at infinity).

Equations

• ModularityConjecture.modularFormAn n f = (PowerSeries.coeff ℂ n) (ModularFormClass.qExpansion N f)

def ModularityConjecture.ratRed (q : ℚ) (p : ℕ) : ZMod p

We need to reduce a rational modulo p, in practice we wont be dividing by zero since the conductor of the elliptic curve saves us.

Equations

• ModularityConjecture.ratRed q p = ↑q.num * (↑q.den)⁻¹

def ModularityConjecture.setOfPointsModN (E : WeierstrassCurve ℚ) [E.IsElliptic] (n : ℕ) : Set (ZMod n × ZMod n)

The set of points on an elliptic curve over ZMod n.

Equations

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

instance ModularityConjecture.apFintype (E : WeierstrassCurve ℚ) [E.IsElliptic] (p : ℕ+) : Fintype ↑(setOfPointsModN E ↑p)

The set of point mod n is finite.

Equations

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

def ModularityConjecture.WeierstrassCurve.ap (E : WeierstrassCurve ℚ) [E.IsElliptic] (p : ℕ) : ℕ

Note that normally this is written as p + 1 - #E(𝔽ₚ), but since we don't have a point at infinty on this affine curve we only have p

Equations

• ModularityConjecture.WeierstrassCurve.ap E p = p - Cardinal.toNat (Cardinal.mk ↑(ModularityConjecture.setOfPointsModN E p))

def ModularityConjecture.IsNormalisedEigenform {N : ℕ} {k : ℤ} (f : CuspForm (CongruenceSubgroup.Gamma0 N) k) : Prop

Since we don't have Hecke operators yet, we define this via the q-expansion coefficients. See Proposition 5.8.5 of [diamondshurman2005].

Equations

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

def ModularityConjecture.modularityConjecture (E : WeierstrassCurve ℚ) [E.IsElliptic] : Prop

See theorem 8.8.1 of [diamondshurman2005].

Equations

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

theorem ModularityConjecture.modularity_conjecture (E : WeierstrassCurve ℚ) [E.IsElliptic] : modularityConjecture E