Explicit function-field models for X₀(N) and X(N)

ModularCurve.x0_twoJModel identifies the field of ratios of integral q-expansions of modular forms on Γ₀(N) with ℚ(j(q), j(qᴺ)). Its degree over ℚ(j(q)) is the Dedekind psi function. The equality is proved by comparing this field with the field generated by all j(qᵈ) for d ∣ N, using the existing generation theorem and the matching upper and lower degree bounds.

ModularCurve.x0_modularPolynomialPresentation makes the corresponding quotient presentation explicit: ℚ(X)[Y] / (Φ_N(X,Y)) is isomorphic to the q-expansion field, with the images of X and Y equal to j(q) and j(qᴺ). Here AdjoinRoot is the polynomial quotient, not its fraction field; irreducibility makes the quotient itself a field. This statement is over ℚ, like the two-j model above, rather than an assertion about arbitrary coefficient fields.

ModularCurve.LevelN.frickeFunctionFieldModel describes the full-level Fricke-function model over ℂ. The ring LevelN.ring N is ℂ[j, f_v : v ≠ 0], where the f_v are normalized Weierstrass ℘-values at N-torsion points. For any fraction field of this ring, the theorem gives the action by precomposition, its kernel ±Γ(N), fixed field ℂ(j), and the Galois property with degree [SL₂(ℤ) : ±Γ(N)]. The model is expressed over ℂ, not as an arithmetic model over ℚ. It also includes LevelN.FrickeGeneration: every Γ(N)-invariant meromorphic function of at most exponential growth at all cusps is a fraction of elements of this ring. Equality is on punctured neighbourhoods, and the denominator is nonzero there. Thus the claim concerns all such modular functions, not only functions assumed in advance to be Fricke-rational.

theorem ModularCurve.x0_twoJModel (N : ℕ) [NeZero N] : qExpFunctionFieldC ℚ (CongruenceSubgroup.Gamma0 N) = ℚ⟮jq, jqN N⟯ ∧ ℚ⟮jq⟯.relfinrank (qExpFunctionFieldC ℚ (CongruenceSubgroup.Gamma0 N)) = dedekindPsi N

The q-expansion field of X₀(N) is generated by the two j-functions and has degree ψ(N) over the j-line. The q-expansion field is defined independently using ratios of modular forms.

noncomputable def ModularCurve.ModularPolynomialData.toRatFunc {N : ℕ} [NeZero N] (data : ModularPolynomialData N) : Polynomial (RatFunc ℚ)

View the integral modular polynomial as a polynomial in Y over the rational function field ℚ(X), by sending its inner polynomial variable to RatFunc.X.

Equations

• data.toRatFunc = Polynomial.map (Polynomial.aeval RatFunc.X).toRingHom data.Φ

theorem ModularCurve.x0_modularPolynomialPresentation (N : ℕ) [NeZero N] : ∃ (data : ModularPolynomialData N), PhiIrreducible data ∧ ∃ (e : AdjoinRoot data.toRatFunc ≃ₐ[ℚ] ↥(qExpFunctionFieldC ℚ (CongruenceSubgroup.Gamma0 N))), ↑(e ((algebraMap (RatFunc ℚ) (AdjoinRoot data.toRatFunc)) RatFunc.X)) = jq ∧ ↑(e (AdjoinRoot.root data.toRatFunc)) = jqN N

The modular-polynomial quotient is the X₀(N) q-expansion field. The isomorphism is the evaluation map sending the rational-function variable X to j and the quotient generator Y to j_N. AdjoinRoot p denotes Polynomial (RatFunc ℚ) ⧸ Ideal.span {p}.

def ModularCurve.LevelN.FrickeGeneration (N : ℕ) : Prop

Every meromorphic modular function for Γ(N), with at most exponential growth at all cusps, is a rational expression in j and the nonzero Fricke functions. Equality is as meromorphic functions: locally on punctured neighbourhoods, not at arbitrarily assigned values at poles.

Equations

• One or more equations did not get rendered due to their size.

theorem ModularCurve.LevelN.frickeGeneration (N : ℕ) [NeZero N] : FrickeGeneration N

Fricke functions generate all meromorphic modular functions of level N.

theorem ModularCurve.LevelN.frickeFunctionFieldModel (N : ℕ) [NeZero N] (K : Type u_1) [Field K] [Algebra ℂ K] [Algebra (↥(ring N)) K] [IsScalarTower ℂ (↥(ring N)) K] [IsFractionRing (↥(ring N)) K] : FrickeGeneration N ∧ ∃ (hst : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), ∀ f ∈ ring N, (fun (τ : UpperHalfPlane) => f (γ • τ)) ∈ ring N) (σ : Matrix.SpecialLinearGroup (Fin 2) ℤ →* Gal(K/ℂ)), (∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : UpperHalfPlane → ℂ) (hf : f ∈ ring N), (σ γ) ((algebraMap (↥(ring N)) K) ⟨f, hf⟩) = (algebraMap (↥(ring N)) K) ⟨fun (τ : UpperHalfPlane) => f (γ⁻¹ • τ), ⋯⟩) ∧ σ.ker = CongruenceSubgroup.Gamma N ⊔ Subgroup.zpowers (-1) ∧ IntermediateField.fixedField σ.range = ℂ⟮(algebraMap (↥(ring N)) K) (jGen N)⟯ ∧ Transcendental ℂ ((algebraMap (↥(ring N)) K) (jGen N)) ∧ FiniteDimensional (↥ℂ⟮(algebraMap (↥(ring N)) K) (jGen N)⟯) K ∧ Module.finrank (↥ℂ⟮(algebraMap (↥(ring N)) K) (jGen N)⟯) K = (CongruenceSubgroup.Gamma N ⊔ Subgroup.zpowers (-1)).index ∧ IsGalois (↥ℂ⟮(algebraMap (↥(ring N)) K) (jGen N)⟯) K

The full-level Fricke-function field is Galois over the j-line, with the standard modular action, kernel ±Γ(N), and degree equal to the corresponding subgroup index. The generation clause includes every meromorphic modular function of controlled cusp growth.