Coset substitutions and the generic modular polynomial Φℓ #

Definition: ModularCurve_PhiGen (6c538294-6e83-5a61-acbf-af8f4937d322), by Claude, 2026-09-05.

Working with formal Laurent series (Hahn series over $\mathbb{Z}$), the module sets up the substitution calculus behind the modular equation. For a commutative ring $R$ and a unit $u \in R^\times$, qTwist u is the ring endomorphism of $R((t))$ with $(\mathrm{qTwist}\,u\,f)_k = u^k f_k$, i.e. the substitution $t \mapsto ut$; helper lemmas record its effect on monomials, that it preserves supports, is injective, that $\mathrm{qTwist}\,u \circ \mathrm{qTwist}\,v = \mathrm{qTwist}(uv)$, and that it commutes with the $N$-fold expansion qExpand at the cost of replacing $u$ by $u^N$. Over a field $K$, cosetSubst ζ a b is qTwist (ζ ^ (a * b)) followed by qExpand K (a * a), the formal substitution $q \mapsto \zeta^{ab} t^{a^2}$. With $\ell$ prime, $K$ a $\mathbb{Q}$-algebra field and $\zeta \in K^\times$, the index functions cosetA, cosetB encode the pairs $(a,b) = (\ell,0)$ at index $0$ and $(1,b)$ at index $b+1$, and conj ℓ ζ i applies cosetSubst ζ (cosetA ℓ i) (cosetB ℓ i) to the base change coeffEmb K jq of $j(q)$; its normal forms are $j$ expanded in $t^{\ell^2}$ at index $0$ and $\mathrm{qTwist}(\zeta^b)$ of $j$ at index $b+1$. phiProd ℓ conj is $\prod_{i \in \mathrm{Fin}(\ell+1)}(X - C(\mathrm{conj}\,i))$ in $K((t))[X]$, shown monic of degree $\ell+1$, nonzero, and vanishing at each $\mathrm{conj}\,i$. Several predicates pin down the expected shape of this product: PhiGenDescends c says each coefficient of phiProd ℓ (conj ℓ ζ) is the base change of the $\ell$-fold expansion of $c_k \in \mathbb{Q}((q))$; PoleOrderLE/TPoleOrderLE (vanishing of all coefficients in degrees $< -n$), JSimplePole and IntCoeffs (every coefficient lies in $\mathbb{Z}$) are the pole and integrality conditions. Further auxiliary notions: evalAtJqN N, evaluation of $\mathbb{Z}[X]$ at $j(q^N)$; EvalSymm Φ, the assertion that the bivariate $\Phi \in \mathbb{Z}[X][Y]$ takes the same value on $(x,y)$ and $(y,x)$ for all $x,y \in \mathbb{Q}((q))$; ModularPolynomialFamily, the existence, for every prime $\ell$, of a ModularPolynomialData ℓ (a monic $\Phi$ of degree $\psi(\ell)$ with $\Phi(j, j(q^\ell)) = 0$) whose $\Phi$ is EvalSymm; PhiIrreducible data, irreducibility of $\Phi$ pushed into $\mathbb{Q}(j(q))[X]$; the subalgebra $\mathbb{Q}[j(q)] \subseteq \mathbb{Q}((q))$ with its distinguished element and evaluation map; and swapBivar, the involution of $\mathbb{Z}[X][Y]$ interchanging the two variables.

Relation to Mathlib. Mathlib supplies the Laurent series ring as Hahn series over $\mathbb{Z}$ together with aeval/eval₂ evaluation; the substitutions $t \mapsto ut$ and $q \mapsto \zeta^{ab}t^{a^2}$, the family of conjugates of $j$, and modular polynomials are the project's own.

Where it is used. These definitions provide the formal $q$-expansion vocabulary in which the modular equation $\Phi_\ell(X,Y)$ is produced, with its degree, symmetry, integrality and irreducibility properties, for the theory of the modular curves $X_0(N)$ entering the modularity and level-lowering steps.

Coset substitutions and the generic modular polynomial Φℓ​ #

Coset substitutions and the generic modular polynomial Φℓ #