The Petersson adjoint of the trace and of the double coset operators

For a subgroup Γ' ≤ Γ of finite index in SL₂(ℤ), Mathlib's CuspForm.trace sends a cusp form h for Γ' to the cusp form ∑ᵢ h ∣[k] γᵢ for Γ, the sum running over representatives γᵢ of the right cosets Γ' \ Γ. For the un-normalised Petersson products CuspForm.peterssonInnerCosets of the two levels, the trace is adjoint to restriction:

⟪tr h, g⟫_Γ = ⟪h, g⟫_Γ'        (g a cusp form for Γ).

Unfolded, ⟪h, g⟫_Γ' is an integral over a fundamental domain for Γ', which the translates γᵢ • D of a fundamental domain D for Γ tile; moving each piece back to D turns h into h ∣[k] γᵢ and leaves g unchanged. Here the argument is run on the defining coset sums, where it becomes a reindexing: the cosets of Γ'·{±I} in SL₂(ℤ) are in bijection with pairs of a coset of Γ·{±I} and a coset of Γ' in Γ. That bijection needs the hypothesis -I ∈ Γ → -I ∈ Γ', and the identity needs it too: if -I lies in Γ but not in Γ', then the trace counts every translate twice, and in even weight the left side is twice the right.

Combined with the conjugation law TauCeti.CuspForm.peterssonInnerCosets_slash_of_inv_conjAct_eq, this gives the adjoint of the double coset operator. For α ∈ GL₂(ℝ) of positive determinant, f ↦ tr (f ∣[k] α) — the trace, from α⁻¹ Γ₁ α ∩ Γ₂ to Γ₂, of the translate of f by α — is the operator f ↦ f[Γ₁ α Γ₂]_k of Diamond–Shurman §5.1, from S_k(Γ₁) to S_k(Γ₂), and its Petersson adjoint is the double coset operator of the main involution α^ι = (det α) · α⁻¹:

⟪f[Γ₁ α Γ₂]_k, g⟫_Γ₂ = ⟪f, g[Γ₂ α^ι Γ₁]_k⟫_Γ₁.

The Hecke operators Tₙ are double coset operators of this kind, so this is the analytic core of the adjoint formula Tₙ* = ⟨n⟩⁻¹ Tₙ at indices prime to the level.

The Petersson products here are not normalised by the volume of the fundamental domain. When Γ₁ = Γ₂ that makes no difference to the identity, and it is Diamond–Shurman's Proposition 5.5.2(b). When Γ₁ ≠ Γ₂ it is the un-normalised products that match with no volume factor.

Main results

• CuspForm.peterssonInnerCosets_sum_slash_left: the adjunction for the trace written with an arbitrary family of coset representatives.
• CuspForm.peterssonInnerCosets_trace_left: the same for Mathlib's CuspForm.trace.
• CuspForm.peterssonInnerCosets_trace_translate: the Petersson adjoint of the double coset operator f ↦ tr (f ∣[k] α) is g ↦ tr (g ∣[k] α^ι).

References

• F. Diamond and J. Shurman, A first course in modular forms, Sections 5.1 and 5.5.

The trace is adjoint to restriction

theorem CuspForm.peterssonInnerCosets_sum_slash_left {k : ℤ} {Γ Γ' : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] [Γ'.FiniteIndex] (hle : Γ' ≤ Γ) (hneg : -1 ∈ Γ → -1 ∈ Γ') {ι : Type u_1} [Fintype ι] (γ : ι → ↥Γ) (hγ : Function.Bijective fun (i : ι) => ↑(γ i)) (h : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ') k) (g F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (hF : ⇑F = ∑ i : ι, SlashAction.map k (↑(γ i))⁻¹ ⇑h) : F.peterssonInnerCosets g = h.peterssonInnerCosets (ofLe ⋯ g)

The trace is adjoint to restriction, for a chosen family of coset representatives. Let Γ' ≤ Γ be of finite index in SL₂(ℤ) with -I ∈ Γ → -I ∈ Γ', and let γ enumerate Γ / Γ', so that the (γ i)⁻¹ represent the right cosets Γ' \ Γ. If F is the trace ∑ᵢ h ∣[k] (γ i)⁻¹ of a cusp form h for Γ', then for every cusp form g for Γ

⟪F, g⟫_Γ = ⟪h, g⟫_Γ'.

The trace is taken as data F with its defining equation, so that a caller holding its own coset representatives — the Hecke operators come with theirs — need not pass through the quotient. For Mathlib's CuspForm.trace see peterssonInnerCosets_trace_left.

theorem CuspForm.peterssonInnerCosets_trace_left {k : ℤ} {𝒢 : Subgroup (GL (Fin 2) ℝ)} {Γ Γ' : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] [Γ'.FiniteIndex] [𝒢.IsFiniteRelIndex (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ)] (hΓ' : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ' = 𝒢 ⊓ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) (hneg : -1 ∈ Γ → -1 ∈ Γ') (h : CuspForm 𝒢 k) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : (CuspForm.trace (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) h).peterssonInnerCosets g = (ofLe ⋯ h).peterssonInnerCosets (ofLe ⋯ g)

The trace is adjoint to restriction. Let 𝒢 ≤ GL₂(ℝ) meet the image of a finite-index Γ ≤ SL₂(ℤ) in the image of Γ' ≤ Γ, with -I ∈ Γ → -I ∈ Γ'. For a cusp form h for 𝒢 and a cusp form g for Γ, the Petersson product of Mathlib's trace CuspForm.trace of h down to Γ against g is the product at level Γ' of h and g, both read as forms for Γ':

⟪tr h, g⟫_Γ = ⟪h, g⟫_Γ'.

The group 𝒢 is general because that is how the trace arises: for the double coset operators h is a translate f ∣[k] α, modular for the conjugate α⁻¹ Γ₁ α, which is not contained in Γ. The hypothesis on -I is needed: when -I ∈ Γ but -I ∉ Γ', the trace counts each coset of Γ'·{±I} twice.

The adjoint of a double coset operator

theorem CuspForm.peterssonInnerCosets_trace_translate {k : ℤ} {Γ₁ Γ₂ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ₁.FiniteIndex] [Γ₂.FiniteIndex] {α : GL (Fin 2) ℝ} (hα : 0 < (↑α).det) [(ConjAct.toConjAct α⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ₁).IsFiniteRelIndex (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ₂)] [(ConjAct.toConjAct (TauCeti.adjugateGL α)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ₂).IsFiniteRelIndex (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ₁)] (hneg : -1 ∈ Γ₁ ↔ -1 ∈ Γ₂) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ₁) k) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ₂) k) : (CuspForm.trace (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ₂) (translate f α)).peterssonInnerCosets g = f.peterssonInnerCosets (CuspForm.trace (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ₁) (translate g (TauCeti.adjugateGL α)))

The Petersson adjoint of a double coset operator. Let Γ₁, Γ₂ be of finite index in SL₂(ℤ), with -I ∈ Γ₁ ↔ -I ∈ Γ₂, and let α ∈ GL₂(ℝ) have positive determinant, with α⁻¹ Γ₁ α ∩ Γ₂ of finite index in Γ₂ and α Γ₂ α⁻¹ ∩ Γ₁ of finite index in Γ₁. The operator f ↦ tr (f ∣[k] α) from S_k(Γ₁) to S_k(Γ₂) — Mathlib's CuspForm.trace of the translate CuspForm.translate f α, which is the double coset operator f[Γ₁ α Γ₂]_k — has Petersson adjoint g ↦ tr (g ∣[k] α^ι), the double coset operator of the main involution α^ι = TauCeti.adjugateGL α:

⟪f[Γ₁ α Γ₂]_k, g⟫_Γ₂ = ⟪f, g[Γ₂ α^ι Γ₁]_k⟫_Γ₁.

Both sides are computed at the intermediate level: the trace on either side is adjoint to restriction (peterssonInnerCosets_trace_left), and α conjugates α⁻¹ Γ₁ α ∩ Γ₂ onto Γ₁ ∩ α Γ₂ α⁻¹, carrying one intermediate product to the other (TauCeti.CuspForm.peterssonInnerCosets_slash_of_inv_conjAct_eq). The main involution rather than α⁻¹ appears because α^ι α = (det α) · 1, whose slash is multiplication by (det α) ^ (k - 2): exactly the factor the conjugation produces.

The two finite-index hypotheses are instance arguments because CuspForm.trace requires them. For α with rational entries both hold, since Γ₁ and Γ₂ are commensurable with all their rational conjugates; that is not proved here.