The valence formula at general level, transported along the norm map #
For a finite-index subgroup Γ ≤ SL(2, ℤ), the norm ModularForm.norm 𝒮ℒ f = ∏_{γ ∈ SL(2, ℤ) / Γ} f ∣[k] γ of a weight-k form on Γ is a level-one form of weight k · [SL(2, ℤ) : Γ], and its
divisor is the Γ-divisor of f pushed forward. This file carries out that push-forward on the
interior of the upper half-plane and reads the level-one valence formula back as the
general-level one:
Σ_{P ∈ Γ \ ℍ} (2 / |Stab_Γ P|) · ord_P f + ord_∞(Nm f) = k · [SL(2, ℤ) : Γ] / 12.
The bookkeeping is the orbit–stabiliser count already available in
TauCeti.card_fiber_orbitOfCosetTranslate_mul_cardStabilizerOnOrbit: the cosets of Γ that
translate a point p into a given Γ-orbit P number |Stab_{SL(2, ℤ)} p| / |Stab_Γ P|, and
|Stab_{SL(2, ℤ)} p| = 2 · e_p is twice the level-one elliptic order. Dividing the count by e_p
therefore turns the level-one weight 1 / e_p into the general-level weight 2 / |Stab_Γ P|,
uniformly in P, with no case split on the elliptic points.
The index is the full coset index [SL(2, ℤ) : Γ], not the projective one, and correspondingly
the weight is read on the matrix stabiliser rather than on the projective order e_P. That is the
only choice under which both sides are correct in odd weight with -I ∉ Γ, where the projective
norm is not even well defined; the projective statement
Σ_P (1 / e_P) · ord_P f + (|{±I} ∩ Γ| / 2) · ord_∞(Nm f) = k · [SL(2, ℤ) : ±Γ] / 12 is obtained by multiplying this identity by
|{±I} ∩ Γ| / 2. See
TauCeti.ModularForm.weightedOrderOfVanishingOnSubgroupOrbit.
Main declarations #
TauCeti.ModularForm.weightedOrderOfVanishingOnSubgroupOrbit: the general-level weighted vanishing order2 · ord_P f / |Stab_Γ P|, withTauCeti.ModularForm.weightedOrderOfVanishingOnOrbit_eq_two_mul_dividentifying the level-one weightord_P f / e_Pas the same expression.TauCeti.ModularForm.weightedOrderOfVanishingOnOrbit_norm_eq_finsum_mem: the local redistribution — the level-one weight of the norm at oneSL(2, ℤ)-orbit is the sum of the general-level weights offover theΓ-orbits inside it.TauCeti.ModularForm.finsum_weightedOrderOfVanishingOnSubgroupOrbit_eq_finsum_norm: the global form of the same statement, the two divisor sums being equal.valence_formula_finiteIndex_norm: the norm-intermediate general-level valence formula, with the cusp term still read at level one on the norm.twentyFour_mul_orderOfVanishingOnSubgroupOrbit_le_weight_mul_index_mul_cardStabilizerandorderOfVanishingOnSubgroupOrbit_eq_zero_of_weight_mul_index_mul_cardStabilizer_lt_twentyFour: the single-orbit consequences, bounding the mass at one orbit by the total.
Implementation notes #
The cusp half — distributing ord_∞(Nm f) over the cusps of Γ, each read in its width
parameter — is carried out in Norm/Cusps.lean, which combines it with the identity below into
the full general-level valence formula TauCeti.ModularForm.valence_formula_finiteIndex. The
norm is decomposed orbitwise by
TauCeti.ModularForm.slashInvariantForm_norm_apply_eq_prod_galoisProd, and the resulting orders
are summed in
TauCeti.ModularForm.qExpansionOrderAtCusp_one_norm_eq_sum_orderAtCuspTranslationOrbit.
References #
- F. Diamond and J. Shurman, A first course in modular forms, §3.
- AINTLIB
LeanModularForms— the norm-map route to general level, used there for the finite-index Sturm bound (dim_gen_cong_levels); the redistribution of the exact level-one identity carried out here is new.
The weighted vanishing order of a form on a Γ-orbit: 2 · ord_P f / |Stab_Γ P|, the
summand of the valence formula at general level.
The weight is written through the matrix stabiliser order, not through the projective one:
Nat.card (stabilizer Γ P) = Nat.card ((center SL(2, ℤ)).subgroupOf Γ) * e_P by
TauCeti.card_stabilizer_eq_card_subgroupOf_mul_card_stabilizer_map, so the weight is 1 / e_P
when -I ∈ Γ and 2 / e_P when -I ∉ Γ. That is the right normalisation for the norm map,
whose weight is k · [SL(2, ℤ) : Γ] for the full coset index: both sides of the general-level
formula double when -I ∉ Γ, and dividing by 2 there recovers the projective statement
∑_P (1 / e_P) · ord_P f + (|{±I} ∩ Γ| / 2) · ord_∞(Nm f) = k · [SL(2, ℤ) : ±Γ] / 12.
At level one this is the same weight: weightedOrderOfVanishingOnOrbit_eq_two_mul_div below.
Equations
Instances For
The defining equation of weightedOrderOfVanishingOnSubgroupOrbit.
Evaluating the weighted order on the orbit of p recovers twice the pointwise order divided
by the order of its stabiliser in Γ.
Multiplying the weighted order by the stabiliser order recovers twice the plain vanishing order.
The level-one weight is the same weight. ord_P f / e_P is 2 · ord_P f divided by the
order of the matrix stabiliser, because -I lies in SL(2, ℤ) and fixes every point. This is
what makes weightedOrderOfVanishingOnSubgroupOrbit the general-level form of
weightedOrderOfVanishingOnOrbit rather than a second convention.
The level-one weight at a point redistributes over the Γ-orbits above it. The weighted
vanishing order of the norm at the SL(2, ℤ)-orbit of p is the sum of the general-level
weighted orders of f over the Γ-orbits inside that orbit.
This is the local form of the general-level valence formula: each coset of Γ in SL(2, ℤ)
contributes one factor to the norm, the cosets landing in one Γ-orbit are counted by the
orbit-stabiliser identity, and the stabiliser weight is exactly what converts that count into
the weight 2 / |Stab_Γ P|.
The general-level weighted order is nonnegative: a modular form is holomorphic and the weight is positive.
Only finitely many Γ-orbits carry nonzero weighted order: the weight cannot create support
where the order has none.
The interior mass of the norm, redistributed over the Γ-orbits. The level-one weighted
divisor sum of ModularForm.norm 𝒮ℒ f is the general-level weighted divisor sum of f.
Each SL(2, ℤ)-orbit splits into finitely many Γ-orbits, and
weightedOrderOfVanishingOnOrbit_norm_eq_finsum_mem evaluates the level-one weight at that orbit
as the sum of the general-level weights over the pieces.
The valence formula at general level, interior part. For a nonzero weight-k modular
form on a finite-index subgroup Γ ≤ SL(2, ℤ), the weighted divisor sum over Γ \ ℍ, together
with the cusp order of the level-one norm, is k · [SL(2, ℤ) : Γ] / 12.
Σ_{P ∈ Γ \ ℍ} (2 / |Stab_Γ P|) · ord_P f + ord_∞(Nm f) = k · [SL(2, ℤ) : Γ] / 12.
This is valence_formula_weighted transported along the norm map: the interior mass is already
indexed by the Γ-orbits, weighted as the roadmap's 1 / e_P up to the factor
|Stab_Γ P| = |{±I} ∩ Γ| · e_P (see weightedOrderOfVanishingOnSubgroupOrbit), and the index
is the full coset index, as it must be for odd weight with -I ∉ Γ.
The cusp term is still read at level one, on the norm. Distributing it over the cusps of Γ,
each weighted by its width, is the remaining step of the general-level formula; the norm's
q-expansion order at ∞ is decomposed in TauCeti.ModularForm.qExpansion_one_norm_order_eq.
Consequences for a single orbit #
The mass at one orbit is bounded by the total mass. Every other term of the general-level
valence formula is nonnegative, so 24 · ord_P f ≤ k · [SL(2, ℤ) : Γ] · |Stab_Γ P| for a nonzero
form — the general-level counterpart of
TauCeti.ModularForm.twelve_mul_orderOfVanishingOnOrbit_le_weight_mul_ellipticOrder, with the
24 in place of 12 because the weight is read on the matrix stabiliser.
A small enough weighted degree forces vanishing order zero at an orbit. If f is nonzero
this says that f does not vanish there; the statement also covers the zero form, whose vanishing
order is zero by convention.