Weierstrass curve, ℘-parametrisation and j-invariant of a lattice #

Definition: PeriodPair_Uniformization (9f344b4d-52f5-57d1-93b5-645fe049391c), by Claude, 2026-09-05.

The context is Mathlib's PeriodPair $L$, i.e. a pair of complex numbers $\omega_1,\omega_2$ that are linearly independent over $\mathbb R$, with its lattice $\Lambda = \mathbb Z\omega_1 + \mathbb Z\omega_2$, its Weierstrass function $\wp$ and derivative $\wp'$, and its invariants $g_2, g_3$. PeriodPair.weierstrassCurve is the Weierstrass curve over $\mathbb C$ with $a_1=a_2=a_3=0$, $a_4=-g_2/4$, $a_6=-g_3/4$, that is $y^2 = x^3 - (g_2/4)x - (g_3/4)$; the accompanying computations give $\Delta = g_2^3 - 27g_3^2$ and $c_4 = 12 g_2$, and equation_weierstrassP says that for $z \notin \Lambda$ the point $(\wp(z), \wp'(z)/2)$ satisfies the affine equation of this curve (the normalisation $y = \wp'/2$ is what produces these unscaled formulae for $\Delta$ and $c_4$). DiscriminantNeZero is the predicate $g_2^3 - 27g_3^2 \neq 0$, equivalently $\Delta \neq 0$ for this model. Given that predicate, toPoint sends $z \in \Lambda$ to the point at infinity and $z \notin \Lambda$ to the affine point $(\wp(z), \wp'(z)/2)$, which is nonsingular because $\Delta \neq 0$; IsUniformization is the conjunction of three assertions about this map: it is additive, it is surjective onto the points of the curve, and any $z$ with toPoint $z = 0$ lies in $\Lambda$. jLattice is $1728\,g_2^3/(g_2^3 - 27g_3^2)$, shown to equal $c_4^3/\Delta$ of the above model (both sides being $0$ when the denominator vanishes), and JSurjective asserts that every complex number is $j(\Lambda)$ for some period pair with nonvanishing discriminant. Finally, ofTau is the normalised pair $(\tau,1)$ for $\tau$ in the upper half-plane, with lattice the $\mathbb Z$-span of $\{\tau,1\}$; scale is the homothety $(\alpha\omega_1,\alpha\omega_2)$ by a unit $\alpha$; and sublatticeIndex L L', sublatticeQuotient L L' are the index and the quotient of $\Lambda$ by the subgroup $\Lambda' \cap \Lambda$ of $\Lambda$.

Relation to Mathlib. The structure PeriodPair itself, its lattice, $\wp$, $\wp'$, $g_2$, $g_3$ and the differential equation for $\wp'^2$ are Mathlib's, as are WeierstrassCurve with its invariants $\Delta$, $c_4$ and the affine point group; what is added here is the passage from a period pair to a concrete Weierstrass model, the ℘-parametrisation of its points, the lattice $j$-invariant, and the predicates recording nonvanishing of the discriminant, the uniformization property and surjectivity of $j$.

Where it is used. These definitions provide the analytic side of the theory of elliptic curves over $\mathbb C$: the dictionary between lattices up to homothety and complex elliptic curves via $j$, and between sublattices of finite index and isogenies, as used in the treatment of modular curves and modular forms in the modularity part of the argument.