Orders of the point stabilisers of the modular group #
The stabiliser of a point of ℍ in SL(2, ℤ) is finite, and its order depends only on the
orbit. Off the two elliptic orbits that order is 2 — the centre ±1, which acts trivially —
while on the orbit of i it is 4 and on the orbit of ρ it is 6. Dividing by the centre
these are the PSL(2, ℤ)-orders e_i = 2, e_ρ = 3 and e_P = 1 elsewhere, the weights the
valence formula attaches to its orbits.
Mathlib classifies the stabilising matrices (ModularGroup.stabilizer_I,
ModularGroup.stabilizer_ρ, ModularGroup.stabilizer_of_ne), but only at a point of the closed
fundamental domain 𝒟. Added here is the passage to an arbitrary point of ℍ, which
ModularGroup.exists_smul_mem_fd and conjugation supply, together with the resulting counts.
The three orbit-level counts are stated with their hypotheses on the class of z in
MulAction.orbitRel.Quotient SL(2, ℤ) ℍ, rather than on a fundamental-domain representative,
because that is the form the valence formula's index type consumes: its non-elliptic orbits are
literally the q with q ≠ ⟦i⟧ and q ≠ ⟦ρ⟧.
Main declarations #
TauCeti.ModularGroup.finite_stabilizer: every point stabiliser is finite, so the elliptic order is defined at every point ofℍ.TauCeti.ModularGroup.card_stabilizer_IandTauCeti.ModularGroup.card_stabilizer_ρ: the orders4and6at the two elliptic points themselves.TauCeti.ModularGroup.card_stabilizer_of_orbit_eq_IandTauCeti.ModularGroup.card_stabilizer_of_orbit_eq_ρ: the same orders everywhere on those two orbits.TauCeti.ModularGroup.card_stabilizer_eq_two_of_orbit_ne_I_of_orbit_ne_ρ: order2on every other orbit.TauCeti.ModularGroup.card_stabilizer_eq_card_center_mul_card_stabilizer_psl: for anyΓ ≤ SL(2, ℤ), the stabiliser order inΓsplits off the part of the centre thatΓcontains, leaving the projective order inΓ's image inPSL(2, ℤ).TauCeti.ModularGroup.card_stabilizer_eq_two_mul_card_stabilizer_psl: the projective order is the matrix one halved.TauCeti.ModularGroup.card_stabilizer_psl_I,TauCeti.ModularGroup.card_stabilizer_psl_ρandTauCeti.ModularGroup.card_stabilizer_psl_eq_one_of_orbit_ne_I_of_orbit_ne_ρ: the resulting elliptic orderse_i = 2,e_ρ = 3ande_P = 1.TauCeti.ModularGroup.ellipticOrder: those orders assembled into a single functione_Pon the orbit space, withTauCeti.ModularGroup.ellipticOrder_I,TauCeti.ModularGroup.ellipticOrder_ρ,TauCeti.ModularGroup.ellipticOrder_pos,TauCeti.ModularGroup.ellipticOrder_le_threeandTauCeti.ModularGroup.cardStabilizerOnOrbit_eq_two_mul_ellipticOrder.
References #
- Diamond–Shurman, A First Course in Modular Forms, §2.3 — the elliptic points of
SL(2, ℤ)and their stabiliser orders.
Every point stabiliser is finite, so the elliptic order e_P is defined at every point
of ℍ and not only inside the fundamental domain.
The stabiliser of i has order 4: the centre ±1 together with ±S, the inversion
fixing i. In PSL(2, ℤ) this is the elliptic order e_i = 2.
The stabiliser of ρ has order 6: the centre ±1 together with ±ST and ±T⁻¹S,
the two rotations of order three fixing ρ. In PSL(2, ℤ) this is the elliptic order
e_ρ = 3.
Order 4 everywhere on the orbit of i, not just at i: conjugate stabilisers have
equal order, so card_stabilizer_I propagates along the orbit.
Order 6 everywhere on the orbit of ρ, not just at ρ; the companion of
card_stabilizer_of_orbit_eq_I.
Away from the two elliptic orbits the stabiliser is just the centre, of order 2, so
e_P = 1 in PSL(2, ℤ). No fundamental-domain membership is asked of z: the exclusions are
read on its orbit, which is what the valence formula's non-elliptic index type carries.
The projective orders e_P #
The stabiliser order in Γ splits off the part of the centre that Γ contains. For any
Γ ≤ SL(2, ℤ), the order of the stabiliser of z in Γ is the order of Γ ⊓ ±1 times the
order of the stabiliser in the image of Γ in PSL(2, ℤ) — the projective, elliptic order. The
factor is 2 when -I ∈ Γ and 1 otherwise, by
Matrix.SpecialLinearGroup.card_center_subgroupOf_eq_two_iff.
This is the general-level form of the halving below, and it is exactly one application of
TauCeti.card_stabilizer_eq_card_subgroupOf_mul_card_stabilizer_map: no quotient action of Γ
has to be built, because the image of Γ in PSL(2, ℤ) is a subgroup of PSL(2, ℤ), which
already acts on ℍ. Compatibility of the two actions is definitional, since PSL(2, R) is
SL(2, R) ⧸ center and pslMk_smul is rfl.
The SL(2, ℤ)-stabiliser order is twice the PSL(2, ℤ) one. The two differ exactly by
the centre ±1, which acts trivially on ℍ, so every projective stabiliser is the matrix one
halved — the passage from the counts 4, 6, 2 to the elliptic orders e_P.
The elliptic order at i is e_i = 2 — the order of the PSL(2, ℤ)-stabiliser, not the
weight: the valence formula weights that orbit by the reciprocal 1 / e_i = 1 / 2.
The elliptic order at ρ is e_ρ = 3 — again the stabiliser order; the valence formula
weights that orbit by 1 / e_ρ = 1 / 3.
Every non-elliptic orbit has e_P = 1: away from the orbits of i and ρ, the
PSL(2, ℤ)-action on ℍ is free.
The elliptic order of an orbit #
The elliptic order e_P of an SL(2, ℤ)-orbit of ℍ: the order of the stabiliser, in
PSL(2, ℤ), of any point of the orbit. It is 2 on the orbit of i, 3 on the orbit of ρ
and 1 everywhere else, and the valence formula weights an orbit by its reciprocal 1 / e_P.
The index type is the SL(2, ℤ)-orbit space, because that is the one the order divisor
TauCeti.ModularForm.orderOfVanishingOnOrbit is defined on, while the count is taken in
PSL(2, ℤ), which is the group acting effectively. So this is not an instance of the generic
TauCeti.cardStabilizerOnOrbit, whose quotient and whose group are the same; the two are
related by cardStabilizerOnOrbit_eq_two_mul_ellipticOrder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluating ellipticOrder on the orbit of z recovers the PSL(2, ℤ)-stabiliser order
at z.
The matrix stabiliser order is twice the elliptic order, orbitwise: the centre ±1 acts
trivially. This is card_stabilizer_eq_two_mul_card_stabilizer_psl read on the orbit space, and
it is what relates ellipticOrder to the generic TauCeti.cardStabilizerOnOrbit.
e_i = 2.
e_ρ = 3.
e_P = 1 off the two elliptic orbits: away from them PSL(2, ℤ) acts freely.
The elliptic order is positive, so the weight 1 / e_P is defined and nonzero.
Every elliptic order is at most 3.