The Petersson product under a slash and as an integral over translated domains #
Slashing by α ∈ GL(2, ℝ) of positive determinant moves the Petersson integrand along the
Möbius action, and the invariant measure of ℍ does not see that motion. Writing
D = det α > 0, Mathlib's UpperHalfPlane.petersson_slash reads
petersson k (f ∣[k] α) (h ∣[k] α) τ = D ^ (k - 2) * petersson k f h (α • τ),
so integrating over a domain S and changing variables gives
⟪f ∣[k] α, h ∣[k] α⟫_S = D ^ (k - 2) * ⟪f, h⟫_{α • S}.
Feeding h ∣[k] α⁻¹ into that identity moves a slash across the pairing, one argument at a
time — the adjoint formula for a single slash:
⟪f ∣[k] α, h⟫_S = D ^ (k - 2) * ⟪f, h ∣[k] α⁻¹⟫_{α • S}.
This is the change-of-variables step behind the adjoint theory of the Hecke operators
(Diamond–Shurman §5.5, Miyake §4.5), in the shape the change of variables produces. The
classical form uses the main involution α^ι = (det α) · α⁻¹ in place of α⁻¹; the two differ
by the scalar matrix D · I, which slashes as multiplication by D ^ (k - 2), so the two
statements carry the same content and the determinant factor above is exactly the scalar the
involution absorbs. Either way it is the analytic input to the Petersson adjoint
Tₙ* = ⟨n⟩⁻¹Tₙ of the Hecke operators at indices prime to the level.
When the slashed right arguments all coincide — h ∣[k] αᵢ^ι = h' for every i — those
translated pairings reassemble into one pairing over the union ⋃ᵢ αᵢ • S. The translates
are only almost-everywhere disjoint, which is why the reassembly runs through
TauCeti.MeasureTheory.integral_biUnion_finset₀ rather than Mathlib's
MeasureTheory.integral_biUnion_finset. Whether that union is itself a fundamental domain is a
separate question about the family, not settled here; once it is, peterssonInner moves to any
other fundamental domain by UpperHalfPlane.peterssonInner_eq_of_isFundamentalDomain.
The same change of variables identifies the coset sum defining the Petersson product on
S_k(Γ) with a single integral. Each summand
⟪f ∣[k] q⁻¹, g ∣[k] q⁻¹⟫_𝒟 is the integral of the unslashed Petersson integrand over the
translate q⁻¹ • 𝒟; passing to the open domain 𝒟ᵒ, which differs from 𝒟 by a null set,
those translates — one for each coset of Γ·{±I} — become pairwise disjoint. So ⟪f, g⟫ is
the integral of petersson k f g over ⋃_q q⁻¹ • 𝒟ᵒ. This file does not formalize that this
union is itself a fundamental domain for Γ.
Main results #
UpperHalfPlane.peterssonInner_slash_slash_of_det_pos: a simultaneous slash by a positive-determinantαrescales the pairing by(det α) ^ (k - 2)and translates the domain.UpperHalfPlane.peterssonInner_slash_left_of_det_posandUpperHalfPlane.peterssonInner_slash_right_of_det_pos: the adjoint formula, moving a slash from one argument of the pairing to the other.UpperHalfPlane.peterssonInner_slash_left_adjugateGLandUpperHalfPlane.peterssonInner_slash_right_adjugateGL: the same adjoint formulas written with the main involutionα^ιin place ofα⁻¹, where no determinant factor remains.UpperHalfPlane.peterssonInner_sum_slash_left_adjugateGLandUpperHalfPlane.peterssonInner_sum_slash_right_adjugateGL: the same, for a finite family of slashes at once — the shape a Hecke operator presents, being a slash sum over coset representatives.UpperHalfPlane.peterssonInner_sum_slash_left_adjugateGL_biUnionandUpperHalfPlane.peterssonInner_sum_slash_right_adjugateGL_biUnion: when the slashed arguments all coincide, that finite sum is a single pairing over the union of the translated domains.UpperHalfPlane.peterssonInner_slash_slash_SL: the determinant-one case, where the scalar disappears and only the domain moves.CuspForm.peterssonInnerCosets_eq_sum_smul_fd: the coset pairing is a sum of integrals over translates of𝒟.CuspForm.peterssonInnerCosets_eq_peterssonInner: that sum is the single integral ofpetersson k f gover the union of the corresponding translates of𝒟ᵒ— a union whichModularGroup.isFundamentalDomain_iUnion_out_inv_smul_fdo_withCentershows is a fundamental domain for the image ofΓinPSL(2, ℤ).
References #
- F. Diamond and J. Shurman, A first course in modular forms, Sections 5.4 and 5.5.
- Miyake, Modular forms, Section 4.5.
- The AINTLIB
LeanModularFormsproject, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms, commit6d87d596a5372d5b122c47b7082d4c3afa9b7c3b, Apache-2.0 —AdjointTheory.leanfor the single-slash involution form,AdjointTheory/SummandAdjoint.leanfor the finite-family form (peterssonInner_sum_slash_adjoint) and for the reassembly over the union (peterssonInner_sum_slash_adjoint_constantRHS).
Slashing by an element of positive determinant #
A simultaneous slash rescales the Petersson pairing and translates its domain:
⟪f ∣[k] α, h ∣[k] α⟫_S = (det α) ^ (k - 2) · ⟪f, h⟫_{α • S}.
No integrability hypothesis is needed: both sides are the same set integral after the change of
variables, and MeasureTheory.integral is defined (as 0) even where it fails to converge.
The adjoint of a slash, on the left argument:
⟪f ∣[k] α, h⟫_S = (det α) ^ (k - 2) · ⟪f, h ∣[k] α⁻¹⟫_{α • S} for α of positive determinant.
The classical statement uses the main involution α^ι = (det α) · α⁻¹ in place of α⁻¹;
slashing by the scalar matrix (det α) · I is multiplication by (det α) ^ (k - 2), which is
precisely the factor carried here.
The adjoint of a slash, in involution form:
⟪f ∣[k] α, h⟫_S = ⟪f, h ∣[k] α^ι⟫_{α • S}, with no determinant factor.
This is the shape the classical adjoint theory uses (Diamond–Shurman §5.5, Miyake §4.5), and
the shape the Hecke adjoint Tₙ* = ⟨n⟩⁻¹Tₙ is assembled in: the main involution α^ι preserves
the integral matrices, so it acts on the Hecke cosets, where α⁻¹ does not. The determinant
factor of peterssonInner_slash_left_of_det_pos has not gone away — ModularForm.slash_adjugateGL
says it is exactly what the involution contributes over the inverse.
Ported from AINTLIB (github.com/CBirkbeck/AINTLIB @ 6d87d596a537, Apache-2.0),
projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/AdjointTheory.lean:
peterssonInner_slash_adjoint (:412), stated over its peterssonAdj (:322) — which is
TauCeti.adjugateGL specialised to GL (Fin 2) ℝ.
The adjoint of a slash, on the right argument:
⟪f, h ∣[k] α⟫_S = (det α) ^ (k - 2) · ⟪f ∣[k] α⁻¹, h⟫_{α • S}. The mirror of
peterssonInner_slash_left_of_det_pos, with the same proof.
The adjoint of a slash on the right, in involution form:
⟪f, h ∣[k] α⟫_S = ⟪f ∣[k] α^ι, h⟫_{α • S}. The mirror of
peterssonInner_slash_left_adjugateGL, and like it free of the determinant factor.
A finite family of slashes #
The summand-level adjoint, on the left argument: for a finite family αᵢ of
positive-determinant matrices,
⟪∑ᵢ f ∣[k] αᵢ, h⟫_S = ∑ᵢ ⟪f, h ∣[k] αᵢ^ι⟫_{αᵢ • S}.
This is the shape in which the adjoint meets a Hecke operator, which is not a single slash but a
sum of them: HeckeRing.GL2.heckeSlashSum, which underlies the Hecke operator
HeckeRing.GL2.heckeTCuspNat, is ∑ᵥ f ∣[k] aᵥ over representatives of the right cosets in a
double coset. The domains αᵢ • S are left where the change of variables puts
them — reassembling them into one domain is a separate step, and the reason the integrability
hypothesis is stated per summand rather than for the sum.
hint has to be supplied where the family is fixed. The integrability lemmas already here —
UpperHalfPlane.integrableOn_petersson_slash_left and its relatives — do not cover it: they
are stated over 𝒟, for a slash by SL(2, ℤ), and with both arguments slashed, where hint
allows an arbitrary S, a positive-determinant GL(2, ℝ) matrix, and only the left argument
slashed.
Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB @ 6d87d596a5372d5b122c47b7082d4c3afa9b7c3b,
Apache-2.0), projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/AdjointTheory/ SummandAdjoint.lean: peterssonInner_T_p_family_sum_slashes_eq_aggregate_of_integrable (:620).
The split is deliberate. That statement bundles this identity with null-measurability of each
translate, pairwise a.e.-disjointness across the family, and integrability over the union — none
of which the identity needs. Here the domains are left where the change of variables puts them
and reassembling them is a separate step, so the only side condition is integrability of each
summand. The same citation covers peterssonInner_sum_slash_right_adjugateGL below.
The summand-level adjoint, on the right argument: the mirror of
peterssonInner_sum_slash_left_adjugateGL,
⟪f, ∑ᵢ h ∣[k] αᵢ⟫_S = ∑ᵢ ⟪f ∣[k] αᵢ^ι, h⟫_{αᵢ • S}.
Reassembling the translated domains #
The aggregate adjoint identity, on the left argument. When all the translated right
arguments coincide — h ∣[k] αᵢ^ι = h' for every i — the sum produced by
peterssonInner_sum_slash_left_adjugateGL is a single pairing, over the union of the
translated domains:
⟪∑ᵢ f ∣[k] αᵢ, h⟫_S = ⟪f, h'⟫_{⋃ᵢ αᵢ • S}.
The constancy hypothesis hadj is what makes the reassembly possible at all: with a different
integrand on each piece there is nothing to reassemble. It is not a restriction in the Hecke
setting. There the αᵢ are right-coset representatives of a double coset, and their involutions
αᵢ^ι differ from one another by left multiplication by elements of the group h is modular
for, which slashing kills. For Tₚ on Γ₁(N) the representatives are ![![1, b], ![0, p]],
whose involution is ![![1, -b], ![0, 1]] * ![![p, 0], ![0, 1]] with the first factor in
Γ₁(N), so every h ∣[k] αᵢ^ι is h ∣[k] ![![p, 0], ![0, 1]].
The union is not asserted to be a fundamental domain — that is a separate statement about the
family, and once it is available peterssonInner_eq_of_isFundamentalDomain moves the pairing to
any other fundamental domain.
The aggregate adjoint identity, on the right argument: the mirror of
peterssonInner_sum_slash_left_adjugateGL_biUnion,
⟪f, ∑ᵢ h ∣[k] αᵢ⟫_S = ⟪f', h⟫_{⋃ᵢ αᵢ • S} whenever f ∣[k] αᵢ^ι = f' for every i.
Slashing by an element of SL(2, ℤ) #
A simultaneous slash by SL(2, ℤ) only translates the domain of the Petersson pairing:
the determinant is 1, so the scalar of peterssonInner_slash_slash_of_det_pos disappears.
The Petersson product as an integral over a union of translated domains #
The Petersson product of S_k(Γ) is a sum of integrals over translates of 𝒟. Each
coset summand of CuspForm.peterssonInnerCosets slashes both arguments by the same element of
SL(2, ℤ), so UpperHalfPlane.peterssonInner_slash_slash_SL strips the slashes at the cost of
moving the domain.
The Petersson product of S_k(Γ) is a single integral over a union of translates. The
sets q⁻¹ • 𝒟ᵒ, one for each coset of Γ·{±I} in SL(2, ℤ), are open and pairwise disjoint,
and carry an integrable Petersson integrand, so the sum of integrals over them is the integral
over their union.
That union is a fundamental domain for the image of Γ in PSL(2, ℤ):
ModularGroup.isFundamentalDomain_iUnion_out_inv_smul_fdo_withCenter.