The graded ring of level-1 modular forms

This file collects structural results about the graded ring ⨁ k, ModularForm 𝒮ℒ k of level-1 modular forms, beyond those that fall out of the dimension formula directly. In particular, every level-1 modular form is a polynomial in the Eisenstein series E₄ and E₆.

Main definitions

• ModularForm.evalE₄E₆: the evaluation homomorphism ℂ[X₀, X₁] →ₐ[ℂ] ⨁ k, ModularForm 𝒮ℒ k sending X₀ ↦ E₄ and X₁ ↦ E₆.

Main results

• ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq: the pointwise identity Δ = (E₄³ - E₆²) / 1728.
• ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq_graded: the same identity in the graded ring ⨁ k, ModularForm 𝒮ℒ k.
• ModularForm.evalE₄E₆_surjective: evalE₄E₆ is surjective.
• ModularForm.adjoin_E₄_E₆_eq_top: E₄ and E₆ generate ⨁ k, ModularForm 𝒮ℒ k as a ℂ-algebra; in particular it is a finitely generated ℂ-algebra and a Noetherian ring.

Implementation notes

Surjectivity is proved by induction on the weight k. Forms of negative or odd weight, or of weight 2, vanish. Otherwise k = 4 * a + 6 * b for some a b : ℕ, and subtracting a multiple of E₄ ^ a * E₆ ^ b from a form f of weight k leaves a cusp form. That cusp form is Δ times a form of weight k - 12 (CuspForm.discriminantEquiv), which is a polynomial in E₄ and E₆ by induction, and so is Δ = (E₄³ - E₆²) / 1728. The same step covers the weights k < 12, where the form of weight k - 12 is zero.

References

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

theorem ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq (z : UpperHalfPlane) : discriminant z = (E₄ z ^ 3 - E₆ z ^ 2) / 1728

The modular discriminant equals (E₄³ - E₆²) / 1728.

theorem ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq_graded : (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 12) (ModularFormClass.modularForm CuspForm.discriminant) = (1 / 1728) • ((DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 4) E₄ ^ 3 - (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 6) E₆ ^ 2)

The modular discriminant equals (E₄³ - E₆²) / 1728 in the graded ring ⨁ k, ModularForm 𝒮ℒ k.

E₄ and E₆ generate the graded ring

noncomputable def ModularForm.evalE₄E₆ : MvPolynomial (Fin 2) ℂ →ₐ[ℂ] DirectSum ℤ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range)

The evaluation homomorphism from ℂ[X₀, X₁] to the graded ring ⨁ k, ModularForm 𝒮ℒ k of level-1 modular forms, sending X₀ = MvPolynomial.X 0 to E₄ (in weight 4) and X₁ = MvPolynomial.X 1 to E₆ (in weight 6). It is surjective (evalE₄E₆_surjective).

Equations

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

@[simp]

theorem ModularForm.evalE₄E₆_X_zero : evalE₄E₆ (MvPolynomial.X 0) = (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 4) E₄

evalE₄E₆ sends X 0 to E₄, in weight 4 of the graded ring ⨁ k, ModularForm 𝒮ℒ k.

@[simp]

theorem ModularForm.evalE₄E₆_X_one : evalE₄E₆ (MvPolynomial.X 1) = (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 6) E₆

evalE₄E₆ sends X 1 to E₆, in weight 6 of the graded ring ⨁ k, ModularForm 𝒮ℒ k.

theorem ModularForm.evalE₄E₆_surjective : Function.Surjective ⇑evalE₄E₆

The evaluation homomorphism evalE₄E₆ is surjective: every element of the graded ring ⨁ k, ModularForm 𝒮ℒ k, i.e. every finite sum of level-1 modular forms of possibly different weights, is a polynomial in E₄ and E₆.

theorem ModularForm.adjoin_E₄_E₆_eq_top : ℂ[(DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 4) E₄, (DirectSum.of (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range) 6) E₆] = ⊤

E₄ and E₆ generate the graded ring ⨁ k, ModularForm 𝒮ℒ k of level-1 modular forms as a ℂ-algebra.

instance ModularForm.instFiniteTypeComplexDirectSumIntRangeSpecialLinearGroupFinOfNatNatGeneralLinearGroupRealMapGL : Algebra.FiniteType ℂ (DirectSum ℤ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range))

The graded ring ⨁ k, ModularForm 𝒮ℒ k of level-1 modular forms is a finitely generated ℂ-algebra.

instance ModularForm.instIsNoetherianRingDirectSumIntRangeSpecialLinearGroupFinOfNatNatGeneralLinearGroupRealMapGL : IsNoetherianRing (DirectSum ℤ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range))

The graded ring ⨁ k, ModularForm 𝒮ℒ k of level-1 modular forms is a Noetherian ring.