Documentation

TauCeti.Analysis.Complex.ModularForms.LevelOne.JInputs

The level-one modular invariant #

The classical modular invariant is the quotient E₄³ / Δ. The denominator has no zeros in the upper half-plane, so the quotient is holomorphic there. Its weight is zero: the weight factors of its numerator and denominator cancel under the modular group. The identity j - 1728 = E₆² / Δ identifies the fibres above 0 and 1728 with the zero loci of E₄ and E₆, respectively.

At the two elliptic points ρ = e^{2πi/3} and i the orders are exact: E₄ vanishes at ρ and E₆ at i, both to order one, so j vanishes to order 3 at ρ and j - 1728 to order 2 at i. These are the ramification data of j over the elliptic points. Orders are read in the coordinate of ℂ, as the analytic order of the composite with ofComplex.

At the cusp j has a simple pole. In the coordinate q = e^{2πiτ} the product q j is holomorphic, and its q-expansion is pinned down by q j · Δ = q E₄³; dividing by q gives the q-expansion of j, which begins j = q⁻¹ + 744 + 196884 q + ⋯.

Implementation notes #

The vanishing comes from the stabilizers: S fixes i and S * T fixes ρ, with automorphy factors iᵏ and (ρ + 1)ᵏ in weight k, so a form invariant under S vanishes at i unless 4 ∣ k, and one invariant under S * T vanishes at ρ unless 6 ∣ k (TauCeti.NumberTheory.ModularForms.EllipticPoints); in particular E₆ vanishes at i and E₄ at ρ. That the zeros are simple comes from Ramanujan's formulas D E₄ = (E₂ E₄ - E₆) / 3 and D E₆ = (E₂ E₆ - E₄²) / 2 (Mathlib's Derivative.normalizedDerivOfComplex_E₄ and Derivative.normalizedDerivOfComplex_E₆): at a zero of E₄ the derivative is -E₆ / 3, and at a zero of E₆ it is -E₄² / 2, neither of which vanishes because Δ = (E₄³ - E₆²) / 1728 has no zeros.

Main results #

References #

source
noncomputable def TauCeti.ModularForm.j (z : UpperHalfPlane) :
ℂ

The normalized modular invariant j = E₄³ / Δ on the upper half-plane.

Equations
Instances For
    source
    theorem TauCeti.ModularForm.j_apply (z : UpperHalfPlane) :
    j z = ModularForm.E₄ z ^ 3 / ModularForm.discriminant z
    source
    theorem TauCeti.ModularForm.j_mdifferentiable :
    MDiff j

    The modular invariant is holomorphic on the upper half-plane.

    source
    @[simp]
    theorem TauCeti.ModularForm.j_smul (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) :
    j ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ • z) = j z

    The weight factors cancel, so j is invariant under SL₂(ℤ).

    source
    theorem TauCeti.ModularForm.j_sub_1728 (z : UpperHalfPlane) :
    j z - 1728 = ModularForm.E₆ z ^ 2 / ModularForm.discriminant z

    The identity j - 1728 = E₆² / Δ.

    source
    @[simp]
    theorem TauCeti.ModularForm.j_eq_zero_iff (z : UpperHalfPlane) :
    j z = 0 ↔ ModularForm.E₄ z = 0

    The zero fibre of j is exactly the zero locus of E₄.

    source
    @[simp]
    theorem TauCeti.ModularForm.j_eq_1728_iff (z : UpperHalfPlane) :
    j z = 1728 ↔ ModularForm.E₆ z = 0

    The fibre of j above 1728 is exactly the zero locus of E₆.

    The elliptic points #

    source
    @[simp]
    theorem TauCeti.ModularForm.E₄_ρ :
    ModularForm.E₄ UpperHalfPlane.ρ = 0

    E₄ vanishes at ρ.

    source
    @[simp]
    theorem TauCeti.ModularForm.E₆_I :
    ModularForm.E₆ UpperHalfPlane.I = 0

    E₆ vanishes at i.

    source
    theorem TauCeti.ModularForm.E₆_ρ_ne_zero :
    ModularForm.E₆ UpperHalfPlane.ρ ≠ 0

    E₆ does not vanish at ρ.

    source
    theorem TauCeti.ModularForm.E₄_I_ne_zero :
    ModularForm.E₄ UpperHalfPlane.I ≠ 0

    E₄ does not vanish at i.

    source
    @[simp]
    theorem TauCeti.ModularForm.j_ρ :
    j UpperHalfPlane.ρ = 0

    The value j ρ = 0.

    source
    @[simp]
    theorem TauCeti.ModularForm.j_I :
    j UpperHalfPlane.I = 1728

    The value j i = 1728.

    source
    @[simp]
    theorem TauCeti.ModularForm.analyticOrderAt_E₄_comp_ofComplex_ρ :
    analyticOrderAt (⇑ModularForm.E₄ ∘ ↑UpperHalfPlane.ofComplex) ↑UpperHalfPlane.ρ = 1

    E₄ has a simple zero at ρ.

    source
    @[simp]
    theorem TauCeti.ModularForm.analyticOrderAt_E₆_comp_ofComplex_I :
    analyticOrderAt (⇑ModularForm.E₆ ∘ ↑UpperHalfPlane.ofComplex) Complex.I = 1

    E₆ has a simple zero at i.

    source
    @[simp]
    theorem TauCeti.ModularForm.analyticOrderAt_j_comp_ofComplex_ρ :
    analyticOrderAt (j ∘ ↑UpperHalfPlane.ofComplex) ↑UpperHalfPlane.ρ = 3

    The modular invariant vanishes to order exactly 3 at the elliptic point ρ.

    source
    @[simp]
    theorem TauCeti.ModularForm.analyticOrderAt_j_sub_1728_comp_ofComplex_I :
    analyticOrderAt ((j - 1728) ∘ ↑UpperHalfPlane.ofComplex) Complex.I = 2

    The function j - 1728 vanishes to order exactly 2 at the elliptic point i.

    The q-expansion #

    j has a simple pole at the cusp, so its expansion is that of the holomorphic function q j, divided by q. Writing q = e^{2πiτ}, the expansion begins j = q⁻¹ + 744 + 196884 q + ⋯.

    source
    theorem TauCeti.ModularForm.periodic_j_comp_ofComplex :
    Function.Periodic (j ∘ ↑UpperHalfPlane.ofComplex) 1

    The modular invariant is 1-periodic, read on ℂ through ofComplex.

    source
    theorem TauCeti.ModularForm.periodic_qParam_mul_j_comp_ofComplex :
    Function.Periodic ((fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) ∘ ↑UpperHalfPlane.ofComplex) 1

    The function q j is 1-periodic, read on ℂ through ofComplex.

    source
    theorem TauCeti.ModularForm.mdifferentiable_qParam_mul_j :
    MDiff fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ

    The function q j is holomorphic on the upper half-plane.

    source
    theorem TauCeti.ModularForm.tendsto_qParam_mul_j_atImInfty :
    Filter.Tendsto (fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) UpperHalfPlane.atImInfty (nhds 1)

    The pole of j at the cusp is simple with leading coefficient 1: q j → 1 at i∞.

    source
    theorem TauCeti.ModularForm.isBoundedAtImInfty_qParam_mul_j :
    UpperHalfPlane.IsBoundedAtImInfty fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ

    The function q j is bounded at i∞.

    source
    theorem TauCeti.ModularForm.analyticAt_cuspFunction_qParam_mul_j :
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) 0

    The cusp function of q j is analytic at q = 0, so j, read in the coordinate q, is meromorphic at the cusp.

    source
    theorem TauCeti.ModularForm.hasSum_qExpansion_qParam_mul_j (τ : UpperHalfPlane) :
    HasSum (fun (m : ℕ) => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) • Function.Periodic.qParam 1 ↑τ ^ m) (Function.Periodic.qParam 1 ↑τ * j τ)

    The q-expansion of q j converges to q j on the whole upper half-plane.

    source
    theorem TauCeti.ModularForm.qExpansion_qParam_mul_j_mul_qExpansion_discriminant :
    (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) * UpperHalfPlane.qExpansion 1 ModularForm.discriminant = PowerSeries.X * UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄ ^ 3

    The q-expansion of q j is determined by q j · Δ = q E₄³: its product with the expansion of Δ is X times the cube of the expansion of E₄.

    source
    theorem TauCeti.ModularForm.qExpansion_qParam_mul_j_coeff_zero :
    (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) = 1

    The constant coefficient of q j is 1: the leading term of j is q⁻¹.

    source
    @[simp]
    theorem TauCeti.ModularForm.cuspFunction_qParam_mul_j_zero :
    UpperHalfPlane.cuspFunction 1 (fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) 0 = 1

    The analytic cusp function of q j takes the value 1 at zero.

    source
    theorem TauCeti.ModularForm.cuspFunction_j_eventuallyEq :
    UpperHalfPlane.cuspFunction 1 j =ᶠ[nhdsWithin 0 {0}ᶜ] fun (q : ℂ) => UpperHalfPlane.cuspFunction 1 (fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) q / q

    In a punctured neighbourhood of zero, j in its width-one q-coordinate is the analytic cusp function of q j divided by q.

    source
    theorem TauCeti.ModularForm.meromorphicAt_cuspFunction_j :
    MeromorphicAt (UpperHalfPlane.cuspFunction 1 j) 0

    The modular invariant is meromorphic at zero in its width-one q-coordinate.

    source
    @[simp]
    theorem TauCeti.ModularForm.meromorphicOrderAt_cuspFunction_j :
    meromorphicOrderAt (UpperHalfPlane.cuspFunction 1 j) 0 = -1

    The modular invariant has order exactly -1 at zero in its width-one q-coordinate.

    source
    theorem TauCeti.ModularForm.qExpansion_qParam_mul_j_coeff_one :
    (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) = 744

    The q-coefficient of q j is 744, the constant term of j.

    source
    theorem TauCeti.ModularForm.qExpansion_qParam_mul_j_coeff_two :
    (PowerSeries.coeff 2) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) = 196884

    The q²-coefficient of q j is 196884, the coefficient of q in j.

    source
    theorem TauCeti.ModularForm.hasSum_j_sub_inv_qParam (τ : UpperHalfPlane) :
    HasSum (fun (m : ℕ) => (PowerSeries.coeff (m + 1)) (UpperHalfPlane.qExpansion 1 fun (τ : UpperHalfPlane) => Function.Periodic.qParam 1 ↑τ * j τ) • Function.Periodic.qParam 1 ↑τ ^ m) (j τ - (Function.Periodic.qParam 1 ↑τ)⁻¹)

    The q-expansion of j. For every τ in the upper half-plane, j τ - q⁻¹ = ∑ₘ cₘ₊₁ qᵐ, where cₘ are the q-expansion coefficients of q j; thus j = q⁻¹ + 744 + 196884 q + ⋯.

    source
    theorem TauCeti.ModularForm.tendsto_j_sub_inv_qParam_atImInfty :
    Filter.Tendsto (fun (τ : UpperHalfPlane) => j τ - (Function.Periodic.qParam 1 ↑τ)⁻¹) UpperHalfPlane.atImInfty (nhds 744)

    The constant term of j is 744: j - q⁻¹ → 744 at i∞.