Dimension formula for level 1 modular forms

This file proves the dimension formula for the space of modular forms for 𝒮ℒ (= SL(2, ℤ)) of even weight.

Main results

• CuspForm.discriminantEquiv: CuspForm 𝒮ℒ k ≃ₗ[ℂ] ModularForm 𝒮ℒ (k - 12).
• ModularForm.rank_eq_one_add_rank_cuspForm: rank M_k = 1 + rank S_k for even k ≥ 3.
• ModularForm.dimension_level_one: the full dimension formula for all even k : ℕ.
• ModularForm.levelOne_odd_weight_rank_zero: modular forms of odd weight are zero.
• A FiniteDimensional ℂ (ModularForm 𝒮ℒ k) instance for every k : ℤ.

noncomputable def CuspForm.ofMulDiscriminant {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)) : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k

Multiply a modular form of weight k - 12 by the discriminant to get a cusp form of weight k. Built directly as a CuspForm via CuspForm.mulModularForm.

Equations

• CuspForm.ofMulDiscriminant f = CuspForm.mcast ⋯ (CuspForm.discriminant.mulModularForm f) CuspForm.ofMulDiscriminant._proof_2

@[simp]

theorem CuspForm.ofMulDiscriminant_apply {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)) (z : UpperHalfPlane) : (ofMulDiscriminant f) z = ModularForm.discriminant z * f z

noncomputable def CuspForm.divDiscriminant {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)

Divide a cusp form by the discriminant to get a modular form of weight k - 12.

Equations

• f.divDiscriminant = { toFun := fun (z : UpperHalfPlane) => f z / ModularForm.discriminant z, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem CuspForm.divDiscriminant_apply {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (z : UpperHalfPlane) : f.divDiscriminant z = f z / ModularForm.discriminant z

noncomputable def CuspForm.discriminantEquiv {k : ℤ} : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k ≃ₗ[ℂ] ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)

The linear equivalence between cusp forms of weight k and modular forms of weight k - 12, given by division by the discriminant.

Equations

• CuspForm.discriminantEquiv = { toFun := CuspForm.divDiscriminant, map_add' := ⋯, map_smul' := ⋯, invFun := CuspForm.ofMulDiscriminant, left_inv := ⋯, right_inv := ⋯ }

theorem ModularForm.levelOne_odd_weight_eq_zero {k : ℤ} (hk : Odd k) (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : f = 0

A 𝒮ℒ modular form of odd weight is zero (evaluate at -1 ∈ SL(2, ℤ)).

theorem ModularForm.levelOne_odd_weight_rank_zero {k : ℤ} (hk : Odd k) : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) = 0

Modular forms of odd weight for 𝒮ℒ are zero-dimensional.

theorem CuspForm.rank_eq_zero_of_weight_lt_twelve {k : ℤ} (hk : k < 12) : Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) = 0

Cusp forms of weight k < 12 for 𝒮ℒ are zero-dimensional.

theorem CuspForm.rank_eq_one_of_weight_eq_twelve : Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) = 1

The space of weight 12 cusp forms for 𝒮ℒ has rank 1.

theorem CuspForm.exists_smul_discriminant_of_weight_eq_twelve (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) : ∃ (c : ℂ), c • discriminant = f

Every weight 12 cusp form for 𝒮ℒ is a scalar multiple of the discriminant.

theorem ModularForm.rank_eq_one_add_rank_cuspForm {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) = 1 + Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k)

For even k ≥ 3, the rank of 𝒮ℒ modular forms is one more than the rank of cusp forms.

theorem ModularForm.levelOne_weight_four_rank_one : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 4) = 1

theorem ModularForm.levelOne_weight_six_rank_one : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 6) = 1

theorem ModularForm.E₄_qExpansion_coeff_one : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑E₄) = 240

theorem ModularForm.E₆_qExpansion_coeff_one : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑E₆) = -504

theorem ModularForm.levelOne_weight_two_rank_zero : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2) = 0

Modular forms of weight 2 for 𝒮ℒ are zero.

theorem ModularForm.dimension_level_one (k : ℕ) (hk2 : Even k) : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) = ↑(if 12 ∣ ↑k - 2 then ⌊↑k / 12⌋₊ else ⌊↑k / 12⌋₊ + 1)

The dimension formula for 𝒮ℒ modular forms of even weight.

instance ModularForm.instFiniteDimensionalComplexRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL (k : ℤ) : FiniteDimensional ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)