Level-one modular forms of weight divisible by 4 are polynomials in E₄ and Δ

A level-one modular form f of weight k with 4 ∣ k is a combination

f = ∑_{4 a + 12 b = k} c (a, b) • E₄ ^ a * Δ ^ b

with uniquely determined coefficients c (a, b) ∈ ℂ. In other words, the part ⨁_{4 ∣ k} M_k(SL(2, ℤ)) of the graded ring of level-one modular forms is ℂ[E₄, Δ]. This is the shape in which the theta series of an even unimodular lattice, whose weight is divisible by 4, is identified inside the graded ring.

Existence is proved by induction on the weight, as in Mathlib's proof that E₄ and E₆ generate the graded ring (ModularForm.evalE₄E₆_surjective), but with E₄ ^ (k / 4) in place of a general monomial in E₄ and E₆. Subtracting the constant term of f times E₄ ^ (k / 4) leaves a cusp form, which is Δ times a form of weight k - 12 (CuspForm.discriminantEquiv); the case of weight k - 12 is the induction hypothesis.

The induction also keeps track of the field of definition of the coefficients. The q-expansion of E₄ has rational coefficients, and that of Δ has integer coefficients and is q times a power series with constant term 1, so dividing by Δ preserves the property of having all q-expansion coefficients in the image of a field K →+* ℂ. Hence a form whose q-expansion has coefficients in the image of K, such as a form with rational q-expansion, has its coefficients c (a, b) in K.

Uniqueness holds in every weight, and is the linear independence of the functions E₄ ^ a * Δ ^ b with 4 a + 12 b = k: in a vanishing combination, divide by the smallest power Δ ^ b₀ that occurs, which is legitimate because Δ has no zeros on ℍ. As im τ → ∞, E₄ tends to 1 and Δ to 0, so the quotient tends to the coefficient of the unique pair (a₀, b₀) of weight k, which therefore vanishes.

Main statements

• ModularForm.linearIndepOn_E₄_pow_mul_discriminant_pow: the functions E₄ ^ a * Δ ^ b with 4 a + 12 b = k are linearly independent.
• ModularForm.existsUnique_finsupp_E₄_discriminant: a level-one modular form of weight k with 4 ∣ k is a unique combination of the E₄ ^ a * Δ ^ b with 4 a + 12 b = k.
• ModularForm.existsUnique_finsupp_E₄_discriminant_of_qExpansion_mem_range: if the q-expansion of such a form has coefficients in the image of a field K under K →+* ℂ, then so do its coefficients in the E₄ ^ a * Δ ^ b.

References

• J.-P. Serre, A Course in Arithmetic, Ch. VII, §3.2.

theorem ModularForm.linearIndepOn_E₄_pow_mul_discriminant_pow (k : ℤ) : LinearIndepOn ℂ (fun (ab : ℕ × ℕ) (τ : UpperHalfPlane) => E₄ τ ^ ab.1 * discriminant τ ^ ab.2) {ab : ℕ × ℕ | 4 * ↑ab.1 + 12 * ↑ab.2 = k}

The functions E₄ ^ a * Δ ^ b with 4 a + 12 b = k, the products of a single weight k, are linearly independent over ℂ.

Coefficients in a subfield

theorem ModularForm.existsUnique_finsupp_E₄_discriminant_of_qExpansion_mem_range {K : Type u_1} [Field K] (φ : K →+* ℂ) {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (hk : 4 ∣ k) (hf : UpperHalfPlane.qExpansion 1 ⇑f ∈ (PowerSeries.map φ).range) : ∃! c : ℕ × ℕ →₀ K, (∀ ab ∈ c.support, 4 * ↑ab.1 + 12 * ↑ab.2 = k) ∧ ⇑f = fun (τ : UpperHalfPlane) => c.sum fun (ab : ℕ × ℕ) (z : K) => φ z * E₄ τ ^ ab.1 * discriminant τ ^ ab.2

Level-one forms of weight divisible by 4 are polynomials in E₄ and Δ, with coefficients in a subfield. If the q-expansion of a level-one modular form f of weight k with 4 ∣ k is the image of a power series over a field K under φ : K →+* ℂ, then f = ∑_{4 a + 12 b = k} φ (c (a, b)) • E₄ ^ a * Δ ^ b for a unique finitely supported family of coefficients c (a, b) ∈ K. For K = ℚ this says that a form with rational q-expansion is a rational polynomial in E₄ and Δ.

theorem ModularForm.existsUnique_finsupp_E₄_discriminant {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (hk : 4 ∣ k) : ∃! c : ℕ × ℕ →₀ ℂ, (∀ ab ∈ c.support, 4 * ↑ab.1 + 12 * ↑ab.2 = k) ∧ ⇑f = fun (τ : UpperHalfPlane) => c.sum fun (ab : ℕ × ℕ) (z : ℂ) => z * E₄ τ ^ ab.1 * discriminant τ ^ ab.2

Level-one forms of weight divisible by 4 are polynomials in E₄ and Δ. A level-one modular form f of weight k with 4 ∣ k is f = ∑_{4 a + 12 b = k} c (a, b) • E₄ ^ a * Δ ^ b for a unique finitely supported family of coefficients c (a, b) ∈ ℂ.