Galois structure of the level-N modular function field #
Theorem statement: ModularCurve.LevelN.exists_monoidHom_algEquiv_fixedField_eq_adjoin
(05254901-c2d0-58c4-921f-8fa611dadbd3), by Claude, 2026-09-05.
Proof: submission 7e7f48c7-04f5-5ade-a712-5cfe259aa413, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
Let $N$ be a non-zero natural number and let $A_N$ denote ModularCurve.LevelN.ring N, the $\mathbb{C}$-subalgebra of the algebra of
all functions $\mathfrak{H} \to \mathbb{C}$ generated by $j = E_4^3/\Delta$ (written jAnalytic)
together with the functions fricke N v for the non-zero $v \in (\mathbb{Z}/N)^2$. Let $K$ be a
field carrying compatible $\mathbb{C}$- and $A_N$-algebra structures (a scalar tower $\mathbb{C} \to A_N \to K$) and which is a fraction field of $A_N$. The assertion is the existence of a proof hst
that $A_N$ is stable under $F \mapsto (\tau \mapsto F(\gamma \cdot \tau))$ for every $\gamma \in \mathrm{SL}_2(\mathbb{Z})$, and of a group homomorphism $\sigma : \mathrm{SL}_2(\mathbb{Z}) \to (K \simeq_{\mathbb{C}} K)$ into the $\mathbb{C}$-algebra automorphisms of $K$, such that:
$\sigma_\gamma$ sends the image in $K$ of $F \in A_N$ to the image of $\tau \mapsto F(\gamma^{-1} \cdot \tau)$; the kernel of $\sigma$ is the subgroup generated by $\Gamma(N)$ and $-1$; the fixed
field of the range of $\sigma$ is the intermediate field $\mathbb{C}$-generated by the image of $j$
(jGen N); that image is transcendental over $\mathbb{C}$; $K$ is finite-dimensional over
$\mathbb{C}(j)$ of degree equal to the index of $\Gamma(N) \sqcup \langle -1 \rangle$ in
$\mathrm{SL}_2(\mathbb{Z})$; and $K/\mathbb{C}(j)$ is Galois.
This is the classical description of the function field of the modular curve $X(N)$ over
$\mathbb{C}$: it is a Galois extension of $\mathbb{C}(j) = \mathbb{C}(X(1))$ with group
$\mathrm{SL}_2(\mathbb{Z})/\pm\Gamma(N)$ acting by $F \mapsto F \circ \gamma^{-1}$. It underlies the
later counting of fibres and double cosets and the genus estimates for the level-$N$ function field,
such as
[ModularCurve.LevelN.twelve_mul_add_mul_index_le_genusFF]
(thm.html#ModularCurve.LevelN.twelve_mul_add_mul_index_le_genusFF)
and
[ModularCurve.natCard_doubleCoset_le_card_fibres_of_finrank_eq_index]
(thm.html#ModularCurve.natCard_doubleCoset_le_card_fibres_of_finrank_eq_index).
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_LevelN_exists_monoidHom_algEquiv_fixedField_eq_adjoin.lean
<!-- Generated by add_prove2me_provenance.py -->