Coefficientwise Galois action on base-changed Laurent subfields; J0(N) #
Definition: ModularCurve_ArithmeticGalois (c3f06811-4d0c-5470-a95b-b2a84dae4304), by Claude,
2026-09-05.
Fix a field $L$ with a $\mathbb{Q}$-algebra structure and an intermediate field $F_0$ of
$\mathbb{Q}((q))/\mathbb{Q}$, and let $L\cdot F_0 =$ laurentBaseChange L F₀ be the intermediate
field of $L((q))/L$ generated over $L$ by the coefficientwise image of $F_0$ under $\mathbb{Q}\to L$. For $\sigma : L \simeq_{\mathbb{Q}} L$, arithmeticRingAut F₀ σ is the ring automorphism of
$L\cdot F_0$ obtained by applying $\sigma$ to each Laurent coefficient (coeffMap), with inverse
given by $\sigma^{-1}$; stability of $L\cdot F_0$ under this operation is inherited from
coeffMap_mem_laurentBaseChange, and arithmeticRingAut_algebraMap records that it covers $\sigma$
on the constants. arithmeticGalois F₀ packages this as a monoid homomorphism from $L \simeq_{\mathbb{Q}} L$ into SemilinearAut L (L·F₀), the project's group of pairs (automorphism of
the big field, automorphism of the constant field) commuting with the structure map: $\sigma \mapsto (\mathrm{arithmeticRingAut}\,\sigma,\ \sigma)$. Accompanying lemmas identify its two components and
the induced scalar action.
Pulling back along arithmeticGalois gives SMul and DistribMulAction instances of
$L\simeq_{\mathbb{Q}}L$ on Pic0 L (L·F₀), the group of degree-zero divisors (finitely supported
$\mathbb{Z}$-combinations of the project's places of $L\cdot F_0/L$) modulo principal divisors.
Specialising to $\overline{\mathbb{Q}} =$ AlgebraicClosure ℚ and $F_0 =$ modularFunctionFieldFull N (the field generated over $\mathbb{Q}$ by the $q$-expansions $j(q^d)$ for $d \mid N$), the
abbreviations modularFunctionFieldBar N and JZero N name the base-changed field and its
degree-zero divisor class group; JZero.torsionGaloisRep N n is SemilinearAut.torsionRep composed
with arithmeticGalois, a homomorphism from $\overline{\mathbb{Q}} \simeq_{\mathbb{Q}} \overline{\mathbb{Q}}$ to the $\mathbb{Z}/n$-linear endomorphisms of the $n$-torsion of JZero N.
Nothing about genus, dimension or finiteness is asserted; $J_0(N)$ is here defined as this divisor
class group, with no geometric modular curve intervening. $N$ is an arbitrary natural number.
Relation to Mathlib. Mathlib supplies LaurentSeries, IntermediateField and
AlgebraicClosure; the notions of place, degree-zero divisor class group Pic0, semilinear
automorphism group SemilinearAut and modular function field used here are the project's own, as is
the coefficientwise ring homomorphism coeffMap (a packaging of HahnSeries.map). Mathlib declares
no action of $L\simeq_{\mathbb{Q}}L$ on an intermediate field of $L((q))/L$ or on its divisor class
group.
Where it is used. The mod $n$ representation JZero.torsionGaloisRep is the form in which the
Galois action on torsion of the Jacobian of $X_0(N)$ enters the argument: it is the source of the
two-dimensional mod $\ell$ representations attached to modular forms that are compared, via level
lowering and Ribet's theorem, with the representation on $\ell$-torsion of a Frey curve.
<!-- Generated by add_prove2me_provenance.py -->
The automorphism of the base-changed function field induced by acting on its algebraic constants.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The semilinear Galois action on the base-changed function field.
Equations
- ModularCurve.arithmeticGalois F₀ = { toFun := fun (σ : Gal(L/ℚ)) => ⟨(ModularCurve.arithmeticRingAut F₀ σ, σ.toRingEquiv), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The base change of the full rational modular function field to an algebraic closure of the rationals.
Equations
Instances For
The degree-zero divisor-class group of the base-changed full modular function field.
Equations
Instances For
The arithmetic Galois representation on the torsion of the degree-zero divisor-class group.
Equations
- One or more equations did not get rendered due to their size.