The upper half-plane as a subset of ℂ: complex numbers with strictly positive
imaginary part.
Instances For
The local uniformizer q_N(τ) = exp(2πiτ/N) at the cusp i∞ for level N.
Instances For
f : ℍ → ℂ is meromorphic at the cusp i∞ if, after the substitution
q = q_N(τ), it agrees near 0 with a meromorphic function in q.
Instances For
f : ℍ → ℂ is meromorphic at every cusp (= every SL₂(ℤ)-translate of i∞).
Instances For
f : ℍ → ℂ is meromorphic on the upper half-plane if it extends to a meromorphic
function on the open set {Im z > 0} ⊆ ℂ.
Instances For
f is invariant under the subgroup Γ ≤ SL₂(ℤ), i.e. f(γ τ) = f(τ) for
all γ ∈ Γ and τ ∈ ℍ.
Instances For
f : ℍ → ℂ is holomorphic on the upper half-plane if it extends to an analytic
function on the open set {Im z > 0} ⊆ ℂ.
Instances For
The modular j-function j : ℍ → ℂ.
Instances For
The j-function is surjective from ℍ to ℂ.
The j-function is meromorphic on the upper half-plane (in fact holomorphic).
The j-function is invariant under the full modular group SL₂(ℤ).
The j-function is meromorphic at every cusp.
Scaling of the upper half-plane by a positive integer N: sends τ ∈ ℍ to
N τ ∈ ℍ.
Instances For
The level-N j-function j_N(τ) := j(N τ) (cf. Theorem 19.13).
Instances For
A modular function for the congruence subgroup Γ (Definition 19.2): a function
f : ℍ → ℂ that is meromorphic on ℍ, Γ-invariant, and meromorphic at the cusps.
- meromorphicOnH : ModularFunction.IsMeromorphicOnH f
- invariant : ModularFunction.IsInvariantUnder f Γ
- meromorphicAtCusps : ModularFunction.IsMeromorphicAtCusps f
Instances For
Auxiliary version of Theorem 19.8: every modular function for Γ(1) = SL₂(ℤ) is
a rational function of j(τ), witnessed by a pair (P, Q) of polynomials.
Theorem 19.8: every modular function for Γ(1) is a rational function of j(τ);
equivalently ℂ(Γ(1)) = ℂ(j).
If f = P(j)/Q(j) is holomorphic on ℍ, then Q(j(τ)) is never zero on ℍ.
The level-N j-function j_N is meromorphic on ℍ: it is the composition of
j with the (holomorphic) scaling τ ↦ N τ.
The level-N j-function j_N(τ) = j(N τ) is invariant under Γ₀(N)
(Theorem 19.13).
The level-N j-function is meromorphic at every cusp.
Theorem 19.13: j_N(τ) := j(Nτ) is a modular function for Γ₀(N).
The (classical) modular polynomial Φ_N(X, Y) ∈ ℤ[X, Y] as a MvPolynomial
indexed by Fin 2, characterized in Definition 19.15 as the minimal polynomial of
j_N over ℂ(j).
Instances For
The modular polynomial Φ_N, repackaged for positive N : ℕ+.
Instances For
modularPolynomial N = Phi N (definitional unfolding for simp).
Evaluate Φ_N(j₁, j₂) in an arbitrary commutative ring R via the integer
casts.
Instances For
Two j-invariants j₁, j₂ ∈ F admit a cyclic N-isogeny over F: there are
elliptic curves E₁, E₂ with those j-invariants and a surjective group
homomorphism E₁ → E₂ whose kernel is cyclic of order N.
Instances For
Theorem 20.7: the modular polynomial is symmetric, Φ_N(X, Y) = Φ_N(Y, X).
Symmetry of the evaluation Φ_N(j₁, j₂) = Φ_N(j₂, j₁), derived from phi_symmetric.
Dedekind's ψ function ψ(N) = N ∏_{p | N}(1 + 1/p), equal to the index
[Γ(1) : Γ₀(N)] and the degree of Φ_N in each variable.
Instances For
Theorem 19.14: the degree of Φ_N in the variable Y equals
[Γ(1) : Γ₀(N)] = ψ(N).
The two variable-degrees of Φ_N agree, by the symmetry Φ_N(X, Y) = Φ_N(Y, X).
Consequently, the degree of Φ_N in the variable X also equals ψ(N).
The diagonal modular polynomial Φ_N(X, X) ∈ ℤ[X], obtained by specializing both
variables of Φ_N to the same indeterminate.
Instances For
For prime N, Φ_N(X, X) = -X^{2N} + r(X) with deg r < 2N; in particular the
leading term is -X^{2N} (a strengthening of Lemma 20.7's tail).
For prime N, the leading coefficient of Φ_N(X, X) is -1.
Corollary 19.10: every modular function for Γ(1) that is holomorphic on ℍ is a
polynomial in j(τ). The witness P is constructed from a rational-function
representation by checking that the denominator polynomial has degree 0.
The matrix-product entry formula (g₁ g₂)_{ij} = g₁_{i0} g₂_{0j} + g₁_{i1} g₂_{1j}
for SL₂(ℤ)-matrices, expressed via sl2zEntry.
The extended upper half-plane ℍ* = ℍ ⊔ ℚ ∪ {∞}, obtained by adjoining the
rational cusps and the cusp at infinity to ℍ.
Instances For
Inclusion ℍ ↪ ℍ*.
Instances For
Inclusion of a rational cusp r ∈ ℚ ↪ ℍ*.
Instances For
The cusp at infinity in ℍ*.
Instances For
The action of SL₂(ℤ) on the cusps ℚ ∪ {∞}, given by the linear-fractional
formula γ · r = (ar + b)/(cr + d) and γ · ∞ = a/c (with c = 0 mapping to ∞).
Instances For
The identity matrix acts trivially on the cusps.
Auxiliary algebraic identity used in proving the multiplicative law for
cuspAction: handles the case where the denominator vanishes for g₂.
Companion identity to cuspAction_factor_denom_zero for the numerator.
If the denominator of the linear-fractional action of g₂ on r vanishes, then
the numerator cannot also vanish (consequence of det g₂ = 1).
The cusp action at ∞ is compatible with multiplication in SL₂(ℤ):
(g₁ g₂) · ∞ = g₁ · (g₂ · ∞).
The cusp action at a rational cusp r is compatible with multiplication in
SL₂(ℤ): (g₁ g₂) · r = g₁ · (g₂ · r).
Multiplicativity of the cusp action on all of WithTop ℚ, combining the cases
for the cusp at infinity and the finite rational cusps.
The SL₂(ℤ)-action on ℍ*, defined cases-wise: the Möbius action on the upper
half-plane component, and cuspAction on the cusp component.
Instances For
Register smulExt as the scalar multiplication of SL₂(ℤ) on ℍ*.
The SL₂(ℤ)-action on ℍ* is a MulAction, with 1 · x = x and
(g₁ g₂) · x = g₁ · (g₂ · x).
Restriction of the SL₂(ℤ)-action on ℍ* to the congruence subgroup Γ₀(N).
The modular curve X₀(N) = Γ₀(N) \ ℍ* as the orbit space of Γ₀(N) acting on
the extended upper half-plane.
Instances For
Canonical projection ℍ* → X₀(N), sending a point to its Γ₀(N)-orbit.
Instances For
The modular j-function ℍ → ℂ, accessed inside the ModularFunctionField
namespace.
Instances For
f : ℍ → ℂ is a rational function of j(τ) if there exist polynomials p, q
with q ≠ 0 such that q(j(τ)) · f(τ) = p(j(τ)) for all τ ∈ ℍ.
Instances For
The q-expansion of a polynomial in j, viewed as a Laurent series in q.
Instances For
The leading-order coefficient of the q-expansion of P(j) at order
-deg P is the leading coefficient of P (since j = 1/q + O(1)).
Each coefficient of the q-expansion of a monomial a · X^d in j is an
integer multiple of a.
The q-expansion of an arbitrary function f : ℍ → ℂ as a Laurent series.
Instances For
For a polynomial P, the q-expansion of τ ↦ P(j(τ)) equals qExpJ P.
Corollary 19.10 in this namespace: every holomorphic modular function for Γ(1)
is a polynomial in j(τ).
Deprecated name for holomorphic_modular_is_polynomial_in_j (Corollary 19.10).
A Laurent series f has coefficients in an additive subgroup A ⊆ ℂ if every
coefficient f.coeff n belongs to A.
Instances For
A function f : ℍ → ℂ has q-expansion coefficients in the additive subgroup
A ⊆ ℂ.
Instances For
A polynomial P : ℂ[X] has all its coefficients in the additive subgroup
A ⊆ ℂ.
Instances For
If the q-expansion of P(j) has all coefficients in A, then so does P
itself. Proved by induction on the degree, peeling off leading terms.
Lemma 19.18 (Hasse q-expansion principle): if a holomorphic modular function
f for Γ(1) has q-expansion coefficients in an additive subgroup A ⊆ ℂ, then
f(τ) = P(j(τ)) for some polynomial P ∈ A[X].
Scaling of the upper half-plane τ ↦ N τ (the level-N version inside the
ModularPolynomial namespace).
Instances For
The translate-and-scale map τ ↦ (τ + k)/N, used to describe the Γ₀(N)-orbit
representatives appearing in Lemma 19.16 and the conjugates of j_N.
Instances For
j_N(τ) := j(N τ), the level-N j-function, here defined inside the
ModularPolynomial namespace.
Instances For
The conjugate j_N-value j((τ + k)/N); these conjugates are the roots of
Φ_N(j(τ), Y) for N prime.
Instances For
The modular polynomial Φ_N viewed with complex coefficients, before checking
integrality (used to bootstrap Theorem 19.17).
Instances For
The polynomial Φ_N^ℂ(j(τ), j_N(τ)) vanishes identically on ℍ: this is the
defining property of Φ_N as a minimal polynomial of j_N over ℂ(j).
For prime N, each conjugate j_N-value also satisfies Φ_N^ℂ(j(τ), ·) = 0,
exhibiting the N + 1 roots of the modular polynomial.
The integer modular polynomial Phi N, mapped to ℂ, recovers the complex
modular polynomial PhiComplex N.
Theorem 19.17: Φ_N has integer coefficients, i.e. Φ_N ∈ ℤ[X, Y]. The witness
is Phi N, which maps via integers to PhiComplex N.
Matrix-entry computation: S · T^k = !![0, -1; 1, k] in SL₂(ℤ).
Matrix-entry computation: S · T^m · S⁻¹ = !![1, 0; -m, 1] in SL₂(ℤ).
For prime N, every γ ∈ SL₂(ℤ) lies in Γ₀(N) or in one of the N right
cosets Γ₀(N) · S · T^k for 0 ≤ k < N (the "cover" half of Lemma 19.16).
Part of Lemma 19.16: the coset representative S · T^k itself never lies in
Γ₀(N) for prime N.
Lemma 19.16: for prime N, the right cosets of Γ₀(N) in Γ(1) are exactly
{Γ₀(N)} ∪ {Γ₀(N) · S · T^k : 0 ≤ k < N}. This is packaged as three conjuncts:
covering, non-membership of representatives, and pairwise distinctness.
Theorem 19.14 (restated): the degree of Φ_N in Y equals the Dedekind ψ
function, which is the index [Γ(1) : Γ₀(N)].
The diagonal evaluation Φ_N(j₀, j₀) agrees with evaluating the univariate
diagonal polynomial diagPhi N at j₀.
A Laurent series f : LaurentSeries ℂ has integer coefficients: every
f.coeff n is in the image of ℤ → ℂ.
Instances For
Corollary 19.6 (integrality part): the q-expansion of j(τ) has all integer
coefficients.
Corollary 19.6 (leading-term): the q⁻¹-coefficient of j(τ) is 1.
Corollary 19.6 (constant term): the q⁰-coefficient of j(τ) is 744.
Corollary 19.6 (order at the cusp): all coefficients of j(τ) below q⁻¹
vanish, i.e. j has a simple pole of residue 1 at i∞.