DimensionFormulas

noncomputable def mulDeltaMap (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

Multiplication by the discriminant Δ, as a map from weight k - 12 to weight k.

Equations

• mulDeltaMap k f = ModularForm.mcast ⋯ (f.mul (ModFormMk (CongruenceSubgroup.Gamma 1) 12 Delta)) mulDeltaMap._proof_1

theorem mcast_apply {a b : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (h : a = b) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) a) (z : UpperHalfPlane) : (ModularForm.mcast h f ⋯) z = f z

theorem mul_Delta_map_eq (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) (z : UpperHalfPlane) : (mulDeltaMap k f) z = f z * Delta z

theorem mul_Delta_map_eq_mul (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) : ⇑(mulDeltaMap k f) = ⇑(f.mul (ModFormMk (CongruenceSubgroup.Gamma 1) 12 Delta))

theorem qExpansion_coe_smul {n : ℕ} [NeZero n] {k : ℤ} (a : ℂ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) k) : UpperHalfPlane.qExpansion ↑n ⇑(a • f) = UpperHalfPlane.qExpansion (↑n) (a • ⇑f)

theorem qExpansion_coe_smul_cusp {n : ℕ} [NeZero n] {k : ℤ} (a : ℂ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) k) : UpperHalfPlane.qExpansion ↑n ⇑(a • f) = UpperHalfPlane.qExpansion (↑n) (a • ⇑f)

theorem qExpansion_coe_sub {k : ℤ} (f g : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : UpperHalfPlane.qExpansion ↑1 ⇑(f - g) = UpperHalfPlane.qExpansion (↑1) (⇑f - ⇑g)

theorem mul_Delta_IsCuspForm (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) : IsCuspForm (CongruenceSubgroup.Gamma 1) k (mulDeltaMap k f)

noncomputable def ModformMulDelta' (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

Multiplication by the discriminant Δ packaged as a cusp form of weight k.

Equations

• ModformMulDelta' k f = IsCuspFormToCuspForm (CongruenceSubgroup.Gamma 1) k (mulDeltaMap k f) ⋯

theorem slashInvariantForm_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 Modform_mul_Delta_apply (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) (z : UpperHalfPlane) : (ModformMulDelta' k f) z = f z * Delta z

noncomputable def CuspFormsIsoModforms (k : ℤ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k ≃ₗ[ℂ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)

The linear isomorphism between weight-k cusp forms and weight-(k - 12) modular forms, given by dividing by Δ.

Equations

• One or more equations did not get rendered due to their size.

theorem delta_eq_E4E6_const : ∃ (c : ℂ), c • Delta = DeltaE4E6Aux

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 : ModFormMk (CongruenceSubgroup.Gamma 1) 12 DeltaE4E6Aux = (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_E6_aux_q_one_term : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑DeltaE4E6Aux) = 1

theorem Delta_E4_eqn : Delta = DeltaE4E6Aux

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 weight_two_zero (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 2) : f = 0

theorem dim_modforms_eq_one_add_dim_cuspforms (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k) = 1 + Module.rank ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k)

theorem dim_weight_two : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 2) = 0

theorem floor_lem1 (k a : ℚ) (ha : 0 < a) (hak : a ≤ k) : 1 + ⌊(k - a) / a⌋₊ = ⌊k / a⌋₊

theorem dim_modforms_lvl_one (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k) = ↑(if 12 ∣ ↑k - 2 then ⌊↑k / 12⌋₊ else ⌊↑k / 12⌋₊ + 1)

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