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.

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.

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.