Generators of the graded ring of level 1 modular forms: Surjectivity #
We prove that evalE₄E₆ is surjective by showing each DirectSum.of _ k f lies in
its range (strong induction on weight), then using the subalgebra closure of the range.
theorem
monomial_coeff_zero_eq_one
(n a b : ℕ)
(hab : 4 * a + 6 * b = n)
:
(PowerSeries.coeff 0)
(UpperHalfPlane.qExpansion 1
⇑(((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)
↑n)) = 1
Helpers for surj_of_rank_one base cases #
Inductive step #
Main surjectivity proof #
The evaluation homomorphism evalE₄E₆ : ℂ[X₀, X₁] →ₐ[ℂ] ⨁_k M_k(Γ(1))
is surjective.