The order divisor at general level, on the orbit space #
For a subgroup Γ ≤ SL(2, ℤ), the vanishing order of a modular form on Γ is constant on
Γ-orbits of the upper half-plane: every element of Γ acts through a matrix of determinant
1, and the order is invariant along positive-determinant elements of the group of the form.
This file descends the order to the orbit space Γ \ ℍ and records that, for Γ of finite
index, only finitely many orbits carry nonzero order — the summation index of the general-level
valence formula.
The orbit space is spelled MulAction.orbitRel.Quotient (Γ : Subgroup (GL (Fin 2) ℝ)) ℍ, the
index type the rest of the general-level API already uses; the Γ-orbits and the orbits of the
image of Γ in GL (Fin 2) ℝ are the same subsets of ℍ.
Because that is an ordinary MulAction.orbitRel.Quotient, the other function the valence
formula indexes over it — the stabiliser order — needs no modular-specific definition at all:
TauCeti.cardStabilizerOnOrbit in GroupTheory/GroupAction/Stabilizer.lean applies to this
quotient directly. Only the vanishing order, below, needs the determinant-1 argument that
makes it well defined here.
The finiteness is not reproved here. It is
TauCeti.ModularForm.finite_image_orbit_mk_setOf_orderOfVanishingAt_ne_zero_subgroup, which
bounds the image of the nonzero-order set in 𝒢 \ ℍ for any 𝒢 ≤ GL (Fin 2) ℝ of finite
relative index in 𝒮ℒ, by the norm-map route of the Tau Ceti ModularForms roadmap's Layer 1
milestone “General level — by the coset norm”. What this file adds is the order function
on the quotient, which that statement deliberately does not provide: a general 𝒢 may contain
elements of negative determinant, under which the order is not known to be invariant, while the
image of a subgroup of SL(2, ℤ) has determinant 1 throughout.
Main declarations #
TauCeti.ModularForm.slOrbitOfSubgroupOrbit: theSL(2, ℤ)-orbit containing aΓ-orbit, withTauCeti.ModularForm.finite_preimage_slOrbitOfSubgroupOrbit— anSL(2, ℤ)-orbit contains only finitely manyΓ-orbits.TauCeti.ModularForm.orderOfVanishingOnSubgroupOrbit: the order descended to theΓ-orbit space.TauCeti.ModularForm.orderOfVanishingOnSubgroupOrbit_nonneg: that order is nonnegative.TauCeti.ModularForm.hasFiniteSupport_orderOfVanishingOnSubgroupOrbit: finite support of the interior order divisor of a general-level modular form.TauCeti.ModularForm.orderOfVanishingAt_quotientFunc_eq_orderOfVanishingOnSubgroupOrbit: a coset factor of the norm vanishes atpto the orderfhas on the orbitpis translated into.TauCeti.ModularForm.orderOfVanishingAt_norm_eq_finsum_orbit: hence the order of the norm atpis a sum overΓ \ ℍ, each orbit weighted by how many cosets translatepinto it.
References #
- AINTLIB
LeanModularForms— the descent here is the level-one one,TauCeti.ModularForm.orderOfVanishingOnOrbitinOrder/Orbits.lean, which is ported from AINTLIB, transposed fromSL(2, ℤ)toΓ. TauCeti.ModularForm.finite_image_orbit_mk_setOf_orderOfVanishingAt_ne_zero_subgroupinNorm/Order.lean— the general-𝒢form of the norm-map route, arrived at concurrently with this file and consumed by it here, rather than reproved.- F. Diamond and J. Shurman, A first course in modular forms, Chapter 3.
The SL(2, ℤ)-orbit containing a Γ-orbit.
Equations
- TauCeti.ModularForm.slOrbitOfSubgroupOrbit o = Quotient.liftOn' o (fun (p : UpperHalfPlane) => Quotient.mk'' p) ⋯
Instances For
Every coset translate of p stays in the SL(2, ℤ)-orbit of p.
Conversely, every Γ-orbit inside the SL(2, ℤ)-orbit of p is a coset translate of p.
The stabiliser of a point in 𝒮ℒ has the order the level-one elliptic bookkeeping records:
twice the elliptic order of its orbit, the extra factor being ±I.
A Γ-orbit outside the SL(2, ℤ)-orbit of p is no coset translate of p.
The multiplicity of a Γ-orbit among the coset translates of p. For a Γ-orbit inside
the SL(2, ℤ)-orbit of p, the number of cosets translating p into it, times the order of its
stabiliser in Γ, is the order of the stabiliser of p in SL(2, ℤ) — twice the elliptic order
of the level-one orbit.
The stabiliser weight is positive. A point of ℍ has a finite, nonempty stabiliser in any
subgroup of SL(2, ℤ) — it sits inside the finite SL(2, ℤ)-stabiliser, whose order the
orbit-stabiliser identity divides — so its cardinality never vanishes.
A single SL(2, ℤ)-orbit contains only finitely many Γ-orbits: each is a coset translate
of any of its points, and the coset space is finite.
The vanishing order of a form for Γ ≤ SL(2, ℤ), descended to the Γ-orbit space of
the upper half-plane.
Equations
Instances For
Evaluating the descended order on the orbit of p recovers the vanishing order at p.
The vanishing order on an orbit is nonnegative: a modular form is holomorphic, so it has no poles.
The coset factors of the norm see exactly the orbits of the translates of the point.
The factor indexed by q vanishes at p to the order f itself has on the orbit into which
q translates p.
This is what turns the coset sum of orderOfVanishingAt_norm into a sum over orbits: the
summand depends on q only through orbitOfCosetTranslate p q.
A modular form for a finite-index subgroup Γ ≤ SL(2, ℤ) has nonzero vanishing order on
only finitely many Γ-orbits in the upper half-plane.
This is the finite-support statement for the interior part of the general-level divisor. As at level one, the zero form needs no exclusion: its order vanishes identically, so its support is empty.
The order of the norm at a point, regrouped over the orbit space. The vanishing order
of ModularForm.norm 𝒮ℒ f at p is the sum, over the Γ-orbits of the upper half-plane, of
the descended order of f on the orbit weighted by how many cosets translate p into it.
This is the interior half of the general-level valence formula: the left-hand side is a level
one quantity, which the level-one formula evaluates, while the right-hand side is indexed by
Γ \ ℍ. The fibre counts become the ramification weights 1 / e_P once the stabiliser
comparison converts them.