The Birch and Swinnerton-Dyer conjecture: the rank of $E(\mathbb{Q})$ and the L-function of an elliptic curve over $\mathbb{Q}$

Read-back

Throughout, a Weierstrass curve over $\mathbb{Q}$ is nothing more than an ordered quintuple of rational numbers $(a_1, a_2, a_3, a_4, a_6)$, thought of as the coefficients of the equation

$$Y^2 + a_1 XY + a_3 Y = X^3 + a_2 X^2 + a_4 X + a_6 .$$

Nothing in this bundle requires the discriminant $\Delta$ of $W$ to be nonzero, requires $W$ to be an elliptic curve, or imposes any other condition on the five coefficients. Both declarations accept an arbitrary such quintuple.

---

BSD.IsLFunction W Λ

This is a proposition about two pieces of data: a Weierstrass curve $W$ over $\mathbb{Q}$ (any quintuple as above) and an arbitrary function $\Lambda : \mathbb{C} \to \mathbb{C}$. The proposition holds exactly when both of the following conditions are satisfied.

(1) Entireness. $\Lambda$ is complex-differentiable at every point of $\mathbb{C}$ (i.e. $\Lambda$ is an entire function).

(2) Agreement on a half-plane. For every complex number $s$ with $\operatorname{Re}(s) > \tfrac{3}{2}$ (strict inequality; $\tfrac32$ is the real number $1.5$),

$$\Lambda(s) = L_W(s),$$

where $L_W(s)$ is the Mathlib quantity WeierstrassCurve.LSeries W s, unfolded as follows. Nothing is asserted about $\Lambda$ on the closed half-plane $\operatorname{Re}(s) \le \tfrac32$ beyond entireness.

Unfolding $L_W(s)$. Let $a_W : \mathbb{N} \to \mathbb{Z}$ be the arithmetic function WeierstrassCurve.LFunction W described below (an arithmetic function is a function on $\mathbb{N} = \{0,1,2,\dots\}$ with value $0$ at $0$). Then

$$L_W(s) \;=\; {\sum_{n}}' \; t_s(n), \qquad t_s(0) = 0, \qquad t_s(n) = \frac{a_W(n)}{n^{s}} \quad (n \ge 1),$$

where $a_W(n)$ is cast from $\mathbb{Z}$ to $\mathbb{C}$, $n^s$ is the complex power $\exp(s \log n)$, and ${\sum}'$ is the total unconditional sum: if the family $(t_s(n))_{n \in \mathbb{N}}$ is unconditionally summable in $\mathbb{C}$ (i.e. the finite partial sums over finite sets of indices converge along the filter of finite subsets), $L_W(s)$ is that sum; if it is not summable, $L_W(s)$ is defined to be $0$. No hypothesis in the bundle asserts summability at any $s$; at any $s$ with $\operatorname{Re}(s) > \tfrac32$ at which the series fails to be summable, condition (2) demands $\Lambda(s) = 0$.

Unfolding $a_W$ (the formal Dirichlet series). Let $\mathcal{O}$ be the ring of integers of the number field $\mathbb{Q}$, and let $\mathfrak{p}$ range over the height-one spectrum of $\mathcal{O}$: the nonzero prime ideals of $\mathcal{O}$. For each such $\mathfrak{p}$ write $K_\mathfrak{p}$ for the $\mathfrak{p}$-adic completion of $\mathbb{Q}$ (Mathlib's adicCompletion), and $R_\mathfrak{p} \subset K_\mathfrak{p}$ for its valuation subring (adicCompletionIntegers, the elements of valuation $\le 1$). Let $W_\mathfrak{p}$ be $W$ with its five coefficients mapped into $K_\mathfrak{p}$ via the canonical map $\mathbb{Q} \to K_\mathfrak{p}$. Then

$$a_W \;=\; {\prod_{\mathfrak{p}}}' \; E_\mathfrak{p},$$

where $E_\mathfrak{p}$ is the local Euler factor (an arithmetic function with values in $\mathbb{Z}$) defined below, and ${\prod}'$ is the total unconditional product in the ring of $\mathbb{Z}$-valued arithmetic functions under Dirichlet convolution, taken in the topology of pointwise convergence with $\mathbb{Z}$ discrete (a net of arithmetic functions converges to $g$ iff for each $n$, the $n$-th coefficients are eventually equal to $g(n)$). If the family $(E_\mathfrak{p})_\mathfrak{p}$ is multipliable in this sense, $a_W$ is its product (when the product exists but is not unique, or when only finitely many factors differ from $1$, Mathlib's specific choice conventions apply); if it is not multipliable, $a_W$ is the constant arithmetic function $\mathbf{1}$, i.e. $\mathbf{1}(1) = 1$ and $\mathbf{1}(n) = 0$ for $n \ne 1$.

Unfolding $E_\mathfrak{p}$ (the local Euler factor). Fix $\mathfrak{p}$, and write $K = K_\mathfrak{p}$, $R = R_\mathfrak{p}$, $\kappa = R/\mathfrak{m}_R$ for the residue field of $R$, and $v$ for the multiplicative valuation on $K$ associated to $\mathfrak{m}_R$ (values in $\mathbb{Z}^{\mathrm{m}}_0 = \{0\} \cup \{\text{powers of a generator}\}$, normalised so that $v(x) = 1$ means $x$ is a unit of $R$ and $v(x) < 1$ means $x \in \mathfrak{m}_R$).

Step (a): a minimal model. A Weierstrass curve $V$ over $K$ is called integral (relative to $R$) if there exists a Weierstrass curve over $R$ whose coefficients map to those of $V$. It is called minimal if the change of variables $C = 1$ is maximal, among all changes of variables $C$ over $K$ such that $C \cdot V$ is integral, for the quantity $\tilde v(C \cdot V)$, where $\tilde v(U) = v(\Delta_U)$ if $U$ is integral and $\tilde v(U) = \bot$ (the smallest possible value) otherwise. (Since $v(\Delta) \le 1$ for integral curves, maximality of the multiplicative valuation means the discriminant is "least divisible" by $\mathfrak{m}_R$ among integral models.) Let $W' := W_\mathfrak{p}^{\min}$ be $C_0 \cdot W_\mathfrak{p}$ for some change of variables $C_0$ over $K$, chosen by the axiom of choice, such that $C_0 \cdot W_\mathfrak{p}$ is minimal. (Mathlib proves such a $C_0$ exists for every Weierstrass curve over $K$; which one is chosen is unspecified.) $W'$ is minimal and in particular integral.

Step (b): the reduction and the point count. Let $I$ be a Weierstrass curve over $R$, again chosen by the axiom of choice, whose coefficients map to those of $W'$ (an "integral model" of $W'$). Let $\overline{W'}$ be the Weierstrass curve over $\kappa$ obtained by reducing the five coefficients of $I$ modulo $\mathfrak{m}_R$. Set

$$q := \#\kappa \in \mathbb{N}, \qquad N := \#\,\overline{W'}(\kappa) \in \mathbb{N}, \qquad a := q + 1 - N \in \mathbb{Z},$$

where both $\#$ are Mathlib's Nat.card: the cardinality of the type if it is finite, and $0$ if it is infinite. Here $\overline{W'}(\kappa)$ denotes the type of nonsingular points in affine coordinates on $\overline{W'}$: it consists of one distinguished element (the point at infinity) together with all pairs $(x,y) \in \kappa \times \kappa$ such that

$$y^2 + \bar a_1 xy + \bar a_3 y = x^3 + \bar a_2 x^2 + \bar a_4 x + \bar a_6 \quad\text{and}\quad \bigl(\bar a_1 y \ne 3x^2 + 2\bar a_2 x + \bar a_4 \;\;\text{or}\;\; 2y + \bar a_1 x + \bar a_3 \ne 0\bigr),$$

i.e. the pairs satisfying the Weierstrass equation at which at least one partial derivative of the Weierstrass polynomial is nonzero. (Points of $\overline{W'}$ that satisfy the equation but at which both partial derivatives vanish are not counted.) In particular, if $\kappa$ were infinite then $q = 0$, and $N = 0$ whenever the point type is infinite.

Step (c): the local polynomial. Define $f_\mathfrak{p}(T) \in \mathbb{Z}[T]$ by the following case split (the first applicable case is used; the case split is classical, i.e. not required to be decidable):

• if $W'$ has good reduction — meaning $W'$ is minimal and $v(\Delta_{W'}) = 1$ (the discriminant of $W'$ is a unit of $R$) — then $f_\mathfrak{p}(T) = 1 - aT + qT^2$ with $a, q$ as in step (b);
• otherwise, if $W'$ has split multiplicative reduction — meaning $W'$ is minimal, $v(\Delta_{W'}) < 1$, $v(c_4(W')) = 1$, and the polynomial

$$c_4(I)\,T^2 + a_1(I)\,c_4(I)\,T - \bigl(54\, b_6(I) - 3\, b_2(I)\, b_4(I) + a_2(I)\, c_4(I)\bigr),$$

with coefficients computed from the chosen integral model $I$ and then reduced to $\kappa$, splits over $\kappa$ (belongs to the multiplicative monoid generated by constant polynomials and monic linear polynomials $T + c$, $c \in \kappa$) — then $f_\mathfrak{p}(T) = 1 - T$;

• otherwise, if $W'$ has multiplicative reduction — meaning $W'$ is minimal, $v(\Delta_{W'}) < 1$ and $v(c_4(W')) = 1$ (given the previous case failed, this is the non-split case) — then $f_\mathfrak{p}(T) = 1 + T$;
• otherwise (which, $W'$ being minimal, is exactly the case $v(\Delta_{W'}) < 1$ and $v(c_4(W')) < 1$, "additive reduction"), $f_\mathfrak{p}(T) = 1$.

Here $b_2, b_4, b_6, c_4, \Delta$ are the standard polynomial expressions in the coefficients $a_i$ ($b_2 = a_1^2 + 4a_2$, $b_4 = 2a_4 + a_1 a_3$, $b_6 = a_3^2 + 4a_6$, $b_8 = a_1^2 a_6 + 4a_2 a_6 - a_1 a_3 a_4 + a_2 a_3^2 - a_4^2$, $c_4 = b_2^2 - 24 b_4$, $\Delta = -b_2^2 b_8 - 8 b_4^3 - 27 b_6^2 + 9 b_2 b_4 b_6$).

Step (d): the reciprocal power series. Let $g_\mathfrak{p}(T) \in \mathbb{Z}[[T]]$ be the formal power series obtained from $f_\mathfrak{p}$ by Mathlib's invOfUnit with the unit $1$: its constant coefficient is $1$, and for $n \ge 1$ its $n$-th coefficient is $-\sum_{i + j = n,\; j < n} [T^i] f_\mathfrak{p} \cdot [T^j] g_\mathfrak{p}$. Since in all four cases $f_\mathfrak{p}$ has constant coefficient $1$, this is the genuine multiplicative inverse $g_\mathfrak{p} = 1/f_\mathfrak{p}$ in $\mathbb{Z}[[T]]$.

Step (e): substituting $T = q^{-s}$. $E_\mathfrak{p}$ is the arithmetic function ofPowerSeries q g_p:

• if $q > 1$: $E_\mathfrak{p}(n) = [T^k]\, g_\mathfrak{p}$ when $n = q^k$ for some $k \in \mathbb{N}$, and $E_\mathfrak{p}(n) = 0$ when $n$ is not a power of $q$;
• if $q \le 1$ (in particular if $q = 0$ because $\kappa$ is infinite): $E_\mathfrak{p}$ is the junk value $c \cdot \mathbf{1}$ where $c$ is the constant coefficient of $g_\mathfrak{p}$ (here $c = 1$), i.e. $E_\mathfrak{p}(1) = 1$ and $E_\mathfrak{p}(n) = 0$ for $n \ne 1$.

This completes the unfolding of $a_W$, hence of $L_W(s)$, hence of condition (2).

Summary of what is not assumed by IsLFunction: no condition on $\Delta_W$ (singular curves are allowed); no summability of the Dirichlet series anywhere; no convergence of the Euler product; no uniqueness statement about $\Lambda$; no functional equation; no condition on $\Lambda$ for $\operatorname{Re}(s) \le \tfrac32$ other than being part of an entire function.

---

BSD.rank W

This is a natural number attached to any Weierstrass curve $W$ over $\mathbb{Q}$ (again any quintuple; no elliptic hypothesis). It is defined as

$$\operatorname{rank}(W) \;:=\; \operatorname{finrank}_{\mathbb{Z}}\bigl(W(\mathbb{Q})\bigr),$$

with the following meanings.

The module $W(\mathbb{Q})$. W.toAffine is $W$ itself, regarded in affine coordinates (a notational re-labelling, not a change of data). Its type of points, W.toAffine.Point, consists of one distinguished element $0$ (the point at infinity) together with all pairs $(x,y) \in \mathbb{Q} \times \mathbb{Q}$ satisfying

$$y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6 \quad\text{and}\quad \bigl(a_1 y \ne 3x^2 + 2a_2 x + a_4 \;\;\text{or}\;\; 2y + a_1 x + a_3 \ne 0\bigr),$$

i.e. the rational solutions of the Weierstrass equation at which at least one partial derivative is nonzero. If $W$ happens to be singular, its singular rational points (if any) are simply excluded from this type; the type is defined regardless. This type carries the standard chord–tangent abelian group law of Mathlib (negation $(x,y) \mapsto (x, -y - a_1 x - a_3)$; the sum of two points is $0$ when they are negatives of one another and otherwise is given by the usual secant/tangent formulas), which Mathlib defines for every Weierstrass curve over a field, without requiring the curve to be elliptic. The abelian group is regarded as a $\mathbb{Z}$-module in the usual way ($n \cdot P = P + \dots + P$).

$\operatorname{finrank}_\mathbb{Z}$. For a $\mathbb{Z}$-module $M$, Mathlib defines

$$\operatorname{rank}_\mathbb{Z}(M) := \sup\{\, |S| : S \subseteq M,\ S \text{ is } \mathbb{Z}\text{-linearly independent}\,\}$$

as a cardinal (the supremum over all subsets $S$ such that no nontrivial finite $\mathbb{Z}$-linear combination of distinct elements of $S$ is $0$; the supremum need not be attained), and

$$\operatorname{finrank}_\mathbb{Z}(M) := \operatorname{toNat}\bigl(\operatorname{rank}_\mathbb{Z}(M)\bigr),$$

where $\operatorname{toNat}$ sends a finite cardinal to the corresponding natural number and sends every infinite cardinal to $0$. Consequently:

• if the supremum of sizes of $\mathbb{Z}$-linearly independent subsets of $W(\mathbb{Q})$ is a finite number $r$, then $\operatorname{rank}(W) = r$;
• if that supremum is infinite (there are arbitrarily large, or an infinite, $\mathbb{Z}$-linearly independent subset), then $\operatorname{rank}(W) = 0$;
• torsion elements (elements $P \ne 0$ with $nP = 0$ for some $n \ge 1$) never belong to a linearly independent subset, so they do not contribute;
• the definition does not require $W(\mathbb{Q})$ to be finitely generated, and for $\mathbb{Z}$-modules $\operatorname{finrank}_\mathbb{Z}$ can be nonzero for non-finitely-generated modules (e.g. $\operatorname{finrank}_\mathbb{Z}(\mathbb{Q}) = 1$); no finiteness hypothesis of any kind is stated or used in this declaration.