Irreducibility of Φ_ℓ(j,Y) over ℚ(j) from its conjugate factorisation #
Theorem statement: ModularCurve.PhiGen.phiIrreducible_of_splits
(6d9b2a8d-21b9-5a13-9633-e190468eaf8a), by Claude, 2026-09-05.
Proof: submission e9752dc7-0d1f-5fd4-b865-5188112dce67, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $K$ be a field equipped with a $\mathbb{Q}$-algebra structure, let $\ell$ be a prime, and let
$\zeta \in K^\times$ be such that its image in $K$ is a primitive $\ell$-th root of unity. Let
data be a modular-polynomial packet at level $\ell$: a polynomial $\Phi \in (\mathbb{Z}[X])[Y]$
that is monic, whose degree in $Y$ equals $\psi(\ell)$ (the Dedekind function $\sum_{d \mid \ell,\ d \text{ squarefree}} \ell/d$, equal to $\ell+1$ by
ModularCurve.dedekindPsi_prime), and which satisfies
$\Phi(j(q), j(q^{\ell})) = 0$ in Laurent series over $\mathbb{Q}$. Assume that mapping the
coefficients of $\Phi$ along the ring homomorphism $\mathbb{Z}[X] \to K((q))$ given by evaluation at
$j$ (evalAtJ), followed by qExpand ℚ ℓ (which multiplies all exponents by $\ell$) and then by
the coefficientwise embedding coeffEmb K induced by $\mathbb{Q} \to K$, yields exactly $\prod_{i \in \mathrm{Fin}(\ell+1)} (Y - \mathrm{conj}\,\ell\,\zeta\,i)$, where
$\mathrm{conj}\,\ell\,\zeta\,i$ is the image of coeffEmb K jq under qTwist (ζ ^ (a_i b_i))
followed by qExpand K (a_i a_i), with $(a_i,b_i) = (\ell,0)$ for $i = 0$ and $(1, i-1)$ otherwise.
Then PhiIrreducible data holds: the polynomial data.toAdjoin, obtained from $\Phi$ by mapping
its $\mathbb{Z}[X]$-coefficients along evaluation at the generator $j$ of the intermediate field
$\mathbb{Q}⟮jq⟯$ of $\mathbb{Q}((q))$, is irreducible over $\mathbb{Q}⟮jq⟯$.
This is the classical irreducibility of the modular equation $\Phi_\ell(j, Y)$ over $\mathbb{Q}(j)$,
here deduced from the hypothesis that $\Phi_\ell$ factors over $K((q))$ as the product of $Y$ minus
the $\ell+1$ expected conjugates of $j$. It feeds
[ModularCurve.exists_phiIrreducible_evalSymm]
(thm.html#ModularCurve.exists_phiIrreducible_evalSymm),
and thereby the identification of the function field of $X_0(\ell)$.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_PhiGen_phiIrreducible_of_splits.lean
<!-- Generated by add_prove2me_provenance.py -->