Generators of the graded ring of level 1 modular forms: Injectivity and main results

The proof decomposes a polynomial into its weighted-homogeneous components (with respect to the weight function ![4, 6]), shows each component maps independently to a single graded piece of the direct sum, and establishes per-weight injectivity by strong induction on the weight. The main results are the algebra isomorphism modularFormsEquivMvPolynomial and the generation theorem E₄E₆_generate.

theorem evalE₄E₆_injective : Function.Injective ⇑evalE₄E₆

The evaluation homomorphism evalE₄E₆ is injective (E₄ and E₆ are algebraically independent).

Main isomorphism and corollaries

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

The graded ring of level 1 modular forms is isomorphic to the weighted polynomial ring in E₄ and E₆.

Equations

• modularFormsEquivMvPolynomial = AlgEquiv.ofBijective evalE₄E₆ modularFormsEquivMvPolynomial._proof_3

theorem E₄E₆_generate : ℂ[(DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 4) E₄, (DirectSum.of (fun (k : ℤ) => ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) 6) E₆] = ⊤

E₄ and E₆ generate the entire graded ring of level 1 modular forms.