Fricke functions and the level-N analytic coordinate ring #
Definition: ModularCurve_LevelNFunctionField (335f222f-fb10-52a8-85e2-9ca6908b27ec), by Claude,
2026-09-05.
Fix a natural number $N$. For $v = (v_0,v_1) \in (\mathbb{Z}/N\mathbb{Z})^2$ and $\tau$ in the upper
half-plane, ModularCurve.LevelN.wp N v τ is
$((2\pi i)^2)^{-1}$ times the value of the Weierstrass function PeriodPair.weierstrassP of the
period pair PeriodPair.ofTau τ — the pair with
periods $\omega_1 = \tau$, $\omega_2 = 1$, whose lattice is the $\mathbb{Z}$-span of $\{\tau, 1\}$ —
at the argument $(v_0\tau + v_1)/N$, where the integers $v_0, v_1$ are the canonical representatives
(ZMod.val) of the two coordinates of $v$. The Fricke function ModularCurve.LevelN.fricke N v is the pointwise product of this with
$-E_4(\tau)E_6(\tau)/\bigl(2592\,\Delta(\tau)\bigr)$, where $E_4$, $E_6$ and $\Delta$ are Mathlib's
level-one Eisenstein series and discriminant;
ModularCurve.LevelN.jAnalytic is the function
$\tau \mapsto E_4(\tau)^3/\Delta(\tau)$. No holomorphy, modularity or nonvanishing assertion is part
of these definitions: each is simply a function $\mathbb{H} \to \mathbb{C}$, with the usual
conventions for division by zero in $\mathbb{C}$.
The set ModularCurve.LevelN.generators N is
obtained by inserting jAnalytic into the set of those functions $g : \mathbb{H} \to \mathbb{C}$
for which there is a nonzero $v \in (\mathbb{Z}/N\mathbb{Z})^2$ with $g =$ fricke N v; and
ModularCurve.LevelN.ring N is the
$\mathbb{C}$-subalgebra of the algebra of all functions $\mathbb{H} \to \mathbb{C}$ (pointwise
operations) generated by this set, i.e. $\mathbb{C}[j, f_v : v \neq 0]$. The accompanying lemmas
record that jAnalytic and each fricke N v with $v \neq 0$ lie in the generating set and hence in
the subalgebra, and ModularCurve.LevelN.jGen N
packages jAnalytic as an element of that subalgebra, with its underlying function being
jAnalytic again.
Relation to Mathlib. The Eisenstein series ModularForm.E₄, ModularForm.E₆ and
ModularForm.discriminant and the upper half-plane are Mathlib's; the period-pair Weierstrass
function is the project's own, and Mathlib has no Fricke functions or level-$N$ function field,
which are introduced here.
Where it is used. These functions provide the concrete analytic model of the modular curve of
level $N$: the subalgebra ring N is the analytic coordinate ring whose fraction field serves as
the field of modular functions of level $N$, and the Fricke functions are the coordinates in which
the transformation law $f_v(\gamma\tau) = f_{v\gamma}(\tau)$ and the invariance under $\pm\Gamma(N)$
are stated elsewhere in the development.
<!-- Generated by add_prove2me_provenance.py -->
The Weierstrass function of the lattice ℤτ + ℤ at the division point indexed by v,
normalized by (2πi)⁻².
Equations
Instances For
The Fricke function indexed by v, defined by multiplying wp N v by -E₄ * E₆ / (2592 * Δ).
Equations
- ModularCurve.LevelN.fricke N v τ = -(ModularForm.E₄ τ * ModularForm.E₆ τ / ModularForm.discriminant τ) / 2592 * ModularCurve.LevelN.wp N v τ
Instances For
The set consisting of j and the Fricke functions indexed by nonzero level-N vectors.
Equations
- ModularCurve.LevelN.generators N = insert ModularCurve.LevelN.jAnalytic {g : UpperHalfPlane → ℂ | ∃ (v : Fin 2 → ZMod N), v ≠ 0 ∧ g = ModularCurve.LevelN.fricke N v}
Instances For
The complex subalgebra of upper-half-plane functions generated by j and the level-N Fricke
functions.
Equations
Instances For
The analytic j-invariant regarded as an element of the algebra generated by the level-N
functions.