Dimension formulas for level-one modular forms

Mathlib (≥ v4.30.0) proves the level-one dimension formulas in Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (ModularForm.dimension_level_one, the rank lemmas for small weights, and CuspForm.discriminantEquiv) and the identity Δ = (E₄³ - E₆²) / 1728 in Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing. Those results are stated for the subgroup 𝒮ℒ; this file transports the ones the project uses to the Γ(1)-indexed spaces used here (CongruenceSubgroup.Gamma_one_coe_eq_SL).

theorem mul_apply {k₁ k₂ : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k₁) (g : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k₂) (z : UpperHalfPlane) : (f.mul g) z = f z * g z

theorem cuspform_weight_lt_12_zero (k : ℤ) (hk : k < 12) : Module.rank ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) = 0

theorem IsCuspForm_weight_lt_eq_zero (k : ℤ) (hk : k < 12) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : IsCuspForm (CongruenceSubgroup.Gamma 1) k f) : f = 0

theorem Delta_E4_E6_eq : ModForm_mk (CongruenceSubgroup.Gamma 1) 12 Delta_E4_E6_aux = (1 / 1728) • ((DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) 4) E₄ ^ 3 - (DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) 6) E₆ ^ 2) 12

theorem Delta_E4_eqn : Delta = Delta_E4_E6_aux

theorem weight_six_one_dimensional : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6) = 1

theorem weight_four_one_dimensional : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4) = 1

theorem weight_eight_one_dimensional (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (hk3 : k < 12) : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k) = 1

theorem dim_gen_cong_levels (k : ℤ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hΓ : Γ.index ≠ 0) : FiniteDimensional ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)