The adjugates of the Hecke coset representatives

HeckeRing.GL2.heckeSlashSum sums f ∣[k] aᵥ over aᵥ = rightCosetRep D v = δ τᵥ⁻¹, where δ represents the double coset and τᵥ runs over Γ₂ ⧸ (Γ₂ ∩ δ⁻¹Γ₁δ). Moving that sum across the Petersson pairing replaces each aᵥ by its main involution aᵥ^ι = adjugateGL aᵥ (UpperHalfPlane.peterssonInner_sum_slash_left_adjugateGL), and the resulting pairing is an integral of g ∣[k] aᵥ^ι over a translate of a fundamental domain — one integrand per v.

This file records the fact that collapses those integrands to one. The adjugate is anti-multiplicative, so

aᵥ^ι = (δ τᵥ⁻¹)^ι = (τᵥ⁻¹)^ι δ^ι = τᵥ δ^ι

as soon as τᵥ has determinant one, and the left factor lies in Γ₂. A function invariant under the weight-k slash action of that factor therefore does not see it: g ∣[k] aᵥ^ι = g ∣[k] δ^ι for every v. That is exactly the constancy hypothesis of UpperHalfPlane.peterssonInner_sum_slash_left_adjugateGL_biUnion, which is what lets the translated pairings reassemble into a single one.

Main results

• HeckeRing.GL2.adjugateGL_rightCosetRep: aᵥ^ι = τᵥ δ^ι, the adjugate of a right-coset representative split off from the adjugate of the double-coset representative.
• HeckeRing.GL2.slash_adjugateGL_rightCosetRep: consequently g ∣[k] aᵥ^ι = g ∣[k] δ^ι for a g invariant under τᵥ, independent of v.

Both are stated at a single v, with the determinant and invariance hypotheses asked of τᵥ alone. A caller quantifying over v — which is what the aggregate identity needs — supplies them from whatever it knows about Γ₂, and HeckeCoset itself puts no condition on its subgroups.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Chapter 3.
• The AINTLIB LeanModularForms project, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms, commit 6d87d596a5372d5b122c47b7082d4c3afa9b7c3b, Apache-2.0 — HeckeRIngs/GL2/AdjointTheory/SummandAdjoint.lean proves the corresponding statements (slash_peterssonAdj_glMap_T_p_upper_eq_slash_T_p_lower, :716, and its M_∞ companion) for the concrete Tₚ family on Γ₁(N), one matrix at a time. Here the double coset is abstract, so the anti-multiplicativity of the adjugate does the work that explicit matrices do there.

theorem HeckeRing.GL2.adjugateGL_rightCosetRep {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℚ)} (D : HeckeCoset Δ Γ₁ Γ₂) (v : DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹) (hdet : (↑↑(Quotient.out v)).det = 1) : TauCeti.adjugateGL (DoubleCoset.rightCosetRep D v) = ↑(Quotient.out v) * TauCeti.adjugateGL ↑(Quotient.out D)

The adjugate of a right-coset representative peels off a Γ₂-element on the left. The adjugate is anti-multiplicative and inverts a determinant-one matrix, so (δ τᵥ⁻¹)^ι = τᵥ · δ^ι.

The determinant hypothesis is asked of τᵥ alone, not of Γ₂: the statement is about one v, and HeckeCoset puts no condition on its subgroups. A caller quantifying over v supplies it from whatever it knows about Γ₂.

theorem HeckeRing.GL2.slash_adjugateGL_rightCosetRep (k : ℤ) {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℚ)} (D : HeckeCoset Δ Γ₁ Γ₂) (v : DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹) (hdet : (↑↑(Quotient.out v)).det = 1) {g : UpperHalfPlane → ℂ} (hg : SlashAction.map k (↑(Quotient.out v)) g = g) : SlashAction.map k (TauCeti.adjugateGL (DoubleCoset.rightCosetRep D v)) g = SlashAction.map k (TauCeti.adjugateGL ↑(Quotient.out D)) g

A Γ₂-invariant function does not see which right-coset representative it is slashed by, once the adjugate is taken: g ∣[k] aᵥ^ι = g ∣[k] δ^ι for every v.

This is the constancy that UpperHalfPlane.peterssonInner_sum_slash_left_adjugateGL_biUnion asks for, and the reason a Hecke operator's translated pairings reassemble into one.