Documentation

TauCeti.NumberTheory.ModularForms.FiniteDimensional

Modular forms of non-positive weight #

The two base cases of the dimension formulas. For an arithmetic group 𝒢, Mathlib's norm map gives that a modular form of negative weight vanishes (ModularForm.isZero_of_neg_weight) and that one of weight 0 is constant (ModularForm.eq_const_of_weight_zero). This file draws the linear-algebra consequences: M_k(𝒢) is the zero space for k < 0, and evaluation at any point identifies M_0(𝒢) with ℂ, so it is one-dimensional.

These are the cases the weight induction in the dimension formulas bottoms out at.

Main results #

Ported from the AINTLIB LeanModularForms project (LeanModularForms/Modularforms/DimGenCongLevels/Basic.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), stated for an arithmetic subgroup of GL(2, ℝ) rather than a finite-index subgroup of SL(2, ℤ) — the generality Mathlib's NormTrace results are already in — and with the weight-zero identification exposed as an equivalence instead of being used only inside the proof.

source
theorem ModularForm.subsingleton_of_neg_weight {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {k : ℤ} (hk : k < 0) :
Subsingleton (ModularForm 𝒢 k)

There are no nonzero modular forms of negative weight.

source
theorem ModularForm.finiteDimensional_of_neg_weight {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] [𝒢.HasDetOne] {k : ℤ} (hk : k < 0) :
FiniteDimensional ℂ (ModularForm 𝒢 k)

Modular forms of negative weight form a finite-dimensional space — the zero space.

source
theorem ModularForm.eq_iff_apply_eq_of_weight_zero {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {f g : ModularForm 𝒢 0} (τ : UpperHalfPlane) :
f = g ↔ f τ = g τ

A weight-zero modular form is determined by its value at any single point, since it is constant.

source
noncomputable def ModularForm.evalEquiv {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] [𝒢.HasDetOne] (τ : UpperHalfPlane) :
ModularForm 𝒢 0 ≃ₗ[ℂ] ℂ

Evaluation at a point identifies the weight-zero forms with ℂ: a weight-zero modular form is constant, so evaluating it anywhere loses nothing, and every scalar is attained by the corresponding constant form.

Instances For
    source
    @[simp]
    theorem ModularForm.evalEquiv_apply {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] [𝒢.HasDetOne] (τ : UpperHalfPlane) (f : ModularForm 𝒢 0) :
    (evalEquiv τ) f = f τ

    The equivalence evaluates a form at the chosen point.

    source
    @[simp]
    theorem ModularForm.evalEquiv_symm_apply {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] [𝒢.HasDetOne] (τ : UpperHalfPlane) (c : ℂ) :
    (evalEquiv τ).symm c = const c

    The inverse of the equivalence is the constant form.

    source
    instance ModularForm.finiteDimensional_weight_zero {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] [𝒢.HasDetOne] :
    FiniteDimensional ℂ (ModularForm 𝒢 0)

    Modular forms of weight 0 form a finite-dimensional space.

    source
    theorem ModularForm.finrank_weight_zero {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] [𝒢.HasDetOne] :
    Module.finrank ℂ (ModularForm 𝒢 0) = 1

    The weight-zero modular forms are one-dimensional: they are exactly the constants.