feat(NumberTheory/ModularForms): E₄ and E₆ generate the graded ring of level-1 modular forms freely

Mathlib.lean

@@ -5702,6 +5702,7 @@ public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
+public import Mathlib.NumberTheory.ModularForms.GradedRing
 public import Mathlib.NumberTheory.ModularForms.Identities
 public import Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
 public import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold

Mathlib/Algebra/DirectSum/Basic.lean

@@ -139,6 +139,9 @@ theorem of_eq_of_ne (i j : ι) (x : β i) (h : j ≠ i) : (of _ i x) j = 0 :=
 lemma of_apply {i : ι} (j : ι) (x : β i) : of β i x j = if h : i = j then Eq.recOn h x else 0 :=
   DFinsupp.single_apply
 
+theorem of_eq_of_eq {i j : ι} (h : i = j) (x : β i) : of β i x = of β j (h ▸ x) := by
+  subst h; rfl
+
 theorem mk_apply_of_mem {s : Finset ι} {f : ∀ i : (↑s : Set ι), β i.val} {n : ι} (hn : n ∈ s) :
     mk β s f n = f ⟨n, hn⟩ :=
   DFinsupp.mk_of_mem hn

Mathlib/Algebra/DirectSum/Module.lean

@@ -93,6 +93,13 @@ theorem mk_smul (s : Finset ι) (c : R) (x) : mk M s (c • x) = c • mk M s x
 theorem of_smul (i : ι) (c : R) (x) : of M i (c • x) = c • of M i x :=
   (lof R ι M i).map_smul c x
 
+theorem of_eq_sub_add_smul {ι : Type*} [DecidableEq ι] {M : ι → Type*}
+    [∀ i, AddCommGroup (M i)] {R : Type*} [Semiring R] [∀ i, Module R (M i)]
+    {i : ι} (f g : M i) (c : R) :
+    of M i f = of M i (f - c • g) + c • of M i g := by
+  rw [← of_smul, ← map_add]
+  exact (congr_arg (of M i) (sub_add_cancel f (c • g))).symm
+
 variable {R}
 
 theorem support_smul [∀ (i : ι) (x : M i), Decidable (x ≠ 0)] (c : R) (v : ⨁ i, M i) :

Mathlib/NumberTheory/ModularForms/Basic.lean

@@ -565,6 +565,12 @@ def mcast {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : Modu
   holo' := f.holo'
   bdd_at_cusps' hc := h ▸ f.bdd_at_cusps' (hΓ ▸ hc)
 
+theorem cast_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k₁ k₂ : ℤ}
+    (heq : k₁ = k₂) (f : ModularForm Γ k₁) (z : ℍ) :
+    (heq ▸ f : ModularForm Γ k₂) z = f z := by
+  subst heq
+  rfl
+
 @[ext (iff := false)]
 theorem gradedMonoid_eq_of_cast {Γ : Subgroup (GL (Fin 2) ℝ)} {a b : GradedMonoid (ModularForm Γ)}
     (h : a.fst = b.fst) (h2 : mcast h a.snd = b.snd) : a = b := by

Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean

@@ -136,6 +136,22 @@ lemma isCuspForm_iff_coeffZero_eq_zero (f : ModularForm 𝒮ℒ k) :
     (periodic_comp_ofComplex _ one_mem_strictPeriods_SL)]
   exact (CuspFormClass.zero_at_infty g).valueAtInfty_eq_zero
 
+/-- Subtracting `(qExpansion 1 f).coeff 0 • g` from `f` (where `g` has constant qExpansion 1)
+gives a cusp form. -/
+lemma sub_smul_isCuspForm (f g : ModularForm 𝒮ℒ k)
+    (hg : (qExpansion 1 g).coeff 0 = 1) :
+    ModularForm.IsCuspForm (f - (qExpansion 1 f).coeff 0 • g) := by
+  set c := (qExpansion 1 f).coeff 0
+  rw [ModularForm.isCuspForm_iff_coeffZero_eq_zero,
+    show qExpansion 1 ⇑(f - c • g : ModularForm 𝒮ℒ k) =
+          qExpansion 1 ⇑f - qExpansion 1 ⇑(c • g : ModularForm 𝒮ℒ k) from
+        (ModularForm.qExpansionAddHom one_pos one_mem_strictPeriods_SL k).map_sub f (c • g),
+    show qExpansion 1 ⇑(c • g : ModularForm 𝒮ℒ k) = c • qExpansion 1 ⇑g from
+      ModularForm.qExpansion_smul (h := 1) (Γ := 𝒮ℒ) (k := k)
+        one_pos one_mem_strictPeriods_SL c g,
+    map_sub, PowerSeries.coeff_smul]
+  simp [hg, c]
+
 end SL2Z
 
 end ModularForm

Mathlib/NumberTheory/ModularForms/QExpansion.lean

@@ -9,6 +9,7 @@ public import Mathlib.Analysis.Complex.TaylorSeries
 public import Mathlib.Analysis.Complex.UpperHalfPlane.Exp
 public import Mathlib.NumberTheory.ModularForms.Basic
 public import Mathlib.NumberTheory.ModularForms.Identities
+public import Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
 public import Mathlib.RingTheory.PowerSeries.Basic
 
 /-!
@@ -592,6 +593,14 @@ protected lemma qExpansion_pow [Γ.HasDetPlusMinusOne] (hh : 0 < h)
     rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
       pow_succ]
 
+protected lemma mul_ne_zero [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods)
+    {a b : ℤ} {f : ModularForm Γ a} {g : ModularForm Γ b} (hf : f ≠ 0) (hg : g ≠ 0) :
+    f.mul g ≠ 0 := by
+  rw [Ne, ← ModularForm.qExpansion_eq_zero_iff hh hΓ,
+    ModularForm.qExpansion_mul hh hΓ, mul_eq_zero, not_or]
+  exact ⟨(ModularForm.qExpansion_eq_zero_iff hh hΓ _).not.mpr hf,
+    (ModularForm.qExpansion_eq_zero_iff hh hΓ _).not.mpr hg⟩
+
 /-- The qExpansion map as an additive group hom. to power series over `ℂ`. -/
 def qExpansionAddHom (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ) :
     ModularForm Γ k →+ PowerSeries ℂ where

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

@@ -245,6 +245,32 @@ theorem add {w : σ → M} (hφ : IsWeightedHomogeneous w φ n) (hψ : IsWeighte
     IsWeightedHomogeneous w (φ + ψ) n :=
   (weightedHomogeneousSubmodule R w n).add_mem hφ hψ
 
+/-- The difference of two weighted homogeneous polynomials of degree `n` is weighted homogeneous
+  of weighted degree `n`. -/
+theorem sub {R : Type*} [CommRing R] {w : σ → M} {φ ψ : MvPolynomial σ R}
+    (hφ : IsWeightedHomogeneous w φ n) (hψ : IsWeightedHomogeneous w ψ n) :
+    IsWeightedHomogeneous w (φ - ψ) n :=
+  (weightedHomogeneousSubmodule R w n).sub_mem hφ hψ
+
+/-- A weighted homogeneous polynomial of degree `n` is zero if no monomial has weight `n`. -/
+theorem eq_zero_of_no_monomials {w : σ → M} (hφ : IsWeightedHomogeneous w φ n)
+    (hno : ∀ d : σ →₀ ℕ, weight w d ≠ n) : φ = 0 := by
+  rw [← support_eq_empty, ← Finset.not_nonempty_iff_eq_empty]
+  rintro ⟨d, hd⟩
+  exact hno _ (hφ (mem_support_iff.mp hd))
+
+/-- A weighted homogeneous polynomial of degree `n` whose support degrees are all equal to a
+fixed `d₀` is a single monomial. -/
+theorem eq_monomial_of_unique_weight {w : σ → M} (hφ : IsWeightedHomogeneous w φ n) (d₀ : σ →₀ ℕ)
+    (huniq : ∀ d, weight w d = n → d = d₀) : φ = monomial d₀ (coeff d₀ φ) := by
+  classical
+  ext d
+  rw [coeff_monomial]
+  by_cases hd : d = d₀
+  · simp [hd]
+  rw [if_neg (Ne.symm hd)]
+  exact hφ.coeff_eq_zero d (fun h => hd (huniq d h))
+
 /-- The sum of weighted homogeneous polynomials of degree `n` is weighted homogeneous of
   weighted degree `n`. -/
 theorem sum {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) (n : M) {w : σ → M}