Generators of the graded ring of level 1 modular forms: Definitions

This file defines the weight function E₄E₆Weight, the evaluation homomorphism evalE₄E₆ : ℂ[X₀, X₁] →ₐ[ℂ] ⨁ k, M_k(Γ(1)), and the polynomial DeltaPoly, along with basic API lemmas (evaluation on generators, odd-weight vanishing, monomial weight existence, and Δ ∈ range evalE₄E₆).

def E₄E₆Weight : Fin 2 → ℕ

Weight function assigning weight 4 to E₄ (variable 0) and weight 6 to E₆ (variable 1).

Equations

• E₄E₆Weight = ![4, 6]

noncomputable def evalE₄E₆ : MvPolynomial (Fin 2) ℂ →ₐ[ℂ] DirectSum ℤ fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

Evaluation homomorphism sending ℂ[X₀, X₁] to the graded ring of level 1 modular forms via X₀ ↦ E₄ and X₁ ↦ E₆.

Equations

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

noncomputable def DeltaPoly : MvPolynomial (Fin 2) ℂ

The polynomial Δ_poly = (1/1728)(X₀³ - X₁²) in ℂ[X₀, X₁], mapping to Δ under evalE₄E₆.

Equations

• DeltaPoly = (1 / 1728) • (MvPolynomial.X 0 ^ 3 - MvPolynomial.X 1 ^ 2)

Odd-weight vanishing

theorem levelOne_odd_weight_eq_zero {k : ℤ} (hk : Odd k) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : f = 0

For odd weight k, every modular form of weight k for Γ(1) is zero.

theorem levelOne_odd_weight_rank_zero {k : ℤ} (hk : Odd k) : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) = 0

For odd weight k, the space of modular forms of weight k for Γ(1) has rank zero.

Combinatorial helpers for monomial weight decomposition

theorem monomial_weight_exists (k : ℕ) (hk : 4 ≤ k) (hkeven : Even k) : ∃ (a : ℕ) (b : ℕ), 4 * a + 6 * b = k

For even k ≥ 4, there exist a, b ∈ ℕ with 4a + 6b = k.

Q-expansion helpers

theorem Ek_q_exp_zero_pow (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (n : ℕ) : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑(LevelOneEisenstein.E (↑k) hk)) ^ n = 1

The 0th q-expansion coefficient of E_k raised to the n-th power equals 1.

Delta in the range of evalE₄E₆

theorem evalE₄E₆_X0 : evalE₄E₆ (MvPolynomial.X 0) = (DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 4) E₄

Key computation: evalE₄E₆ (X 0) = DirectSum.of _ 4 E₄.

theorem evalE₄E₆_X1 : evalE₄E₆ (MvPolynomial.X 1) = (DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 6) E₆

Key computation: evalE₄E₆ (X 1) = DirectSum.of _ 6 E₆.

theorem evalE₄E₆_C (c : ℂ) : evalE₄E₆ (MvPolynomial.C c) = (algebraMap ℂ (DirectSum ℤ fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k)) c

evalE₄E₆ (C c) = algebraMap ℂ _ c.

theorem evalE₄E₆_Delta_poly : evalE₄E₆ DeltaPoly = (1 / 1728) • ((DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 4) E₄ ^ 3 - (DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 6) E₆ ^ 2)

The evaluation of DeltaPoly under evalE₄E₆.

theorem delta_mem_range_evalE₄E₆ : (DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 12) (ModFormMk (CongruenceSubgroup.Gamma 1) 12 Delta) ∈ Set.range ⇑evalE₄E₆

The discriminant Δ lies in the range of evalE₄E₆.

Additional API lemmas

theorem evalE₄E₆_monomial (a b : ℕ) : evalE₄E₆ (MvPolynomial.X 0 ^ a * MvPolynomial.X 1 ^ b) = (DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 4) E₄ ^ a * (DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 6) E₆ ^ b

evalE₄E₆ maps the monomial X₀^a * X₁^b to (of _ 4 E₄)^a * (of _ 6 E₆)^b.

theorem evalE₄E₆_Delta_poly_grade : (evalE₄E₆ DeltaPoly) 12 = ModFormMk (CongruenceSubgroup.Gamma 1) 12 Delta

The weight-12 component of evalE₄E₆ DeltaPoly is the discriminant Δ.

theorem evalE₄E₆_whc_eq_single (n : ℕ) (p : MvPolynomial (Fin 2) ℂ) (hp : MvPolynomial.IsWeightedHomogeneous E₄E₆Weight p n) : evalE₄E₆ p = (DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) ↑n) ((evalE₄E₆ p) ↑n)

A weighted-homogeneous polynomial evaluates to a single-graded DirectSum element.

theorem DirectSum_of_cast_eq {k₁ k₂ : ℤ} (hk : k₁ = k₂) (x : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k₁) : (DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) k₁) x = (DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) k₂) (hk ▸ x)

Weight casting for DirectSum elements.

theorem qExpansion_coeff_zero_Delta : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑(ModFormMk (CongruenceSubgroup.Gamma 1) 12 Delta)) = 0

The 0th q-expansion coefficient of Δ is 0 (Δ is a cusp form).

theorem surj_of_rank_one {k : ℤ} (hrank : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) = 1) {g : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k} (hg : g ≠ 0) (p : MvPolynomial (Fin 2) ℂ) (hp : evalE₄E₆ p = (DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) k) g) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : (DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) k) f ∈ Set.range ⇑evalE₄E₆

In a 1-dimensional weight space, if the generator is in the image of evalE₄E₆, then all elements are.