Hecke slash sums as traces

A double-coset operator is the trace of a translate. The rational cosets used by HeckeRing.GL2.heckeSlashSum and the real cosets used by Mathlib's trace correspond under extension of scalars. Consequently the two constructions agree, with no extra determinant factor: both use the arithmetic slash action.

This comparison allows the Petersson adjunction for traces of translates to be applied to Hecke operators already constructed from rational double cosets.

The trace of a form depends only on its underlying function and its level, not on the type the form is packaged in (TauCeti.SlashInvariantForm.trace_eq_of_eq_of_coe_eq). This is what lets a trace of a translate be compared with another one whose level is equal but not syntactically so, as happens when the translating matrix is changed by an element normalizing the level. When that element multiplies on the right, it comes out of the trace as a slash (TauCeti.SlashInvariantForm.coe_trace_translate_mul_of_mem_normalizer). The lemma TauCeti.trace_coe_cuspForm records the compatibility of the cusp-form and modular-form trace constructions.

References

• F. Diamond and J. Shurman, A first course in modular forms, Sections 5.1 and 5.5.
• David Loeffler, Mathlib's trace construction in NormTrace.lean.

@[simp]

theorem TauCeti.trace_coe_cuspForm {k : ℤ} {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F 𝒢 k] [𝒢.IsFiniteRelIndex ℋ] (f : F) : ModularFormClass.modularForm (CuspForm.trace ℋ f) = ModularForm.trace ℋ f

Coercing a cusp-form trace to a modular form agrees with the modular-form trace. This is class-polymorphic in the source form, just as Mathlib's two trace constructions are.

theorem TauCeti.SlashInvariantForm.trace_eq_of_eq_of_coe_eq {k : ℤ} {𝒢₁ 𝒢₂ ℋ : Subgroup (GL (Fin 2) ℝ)} (h : 𝒢₁ = 𝒢₂) [𝒢₁.IsFiniteRelIndex ℋ] [𝒢₂.IsFiniteRelIndex ℋ] {F₁ : Type u_1} {F₂ : Type u_2} [FunLike F₁ UpperHalfPlane ℂ] [SlashInvariantFormClass F₁ 𝒢₁ k] [FunLike F₂ UpperHalfPlane ℂ] [SlashInvariantFormClass F₂ 𝒢₂ k] {f₁ : F₁} {f₂ : F₂} (hf : ⇑f₁ = ⇑f₂) : SlashInvariantForm.trace ℋ f₁ = SlashInvariantForm.trace ℋ f₂

The trace sees only the underlying function and the level. Two slash-invariant forms with the same underlying function, for levels that are equal (though perhaps not syntactically), have the same trace.

theorem TauCeti.SlashInvariantForm.coe_trace_translate_mul_of_mem_normalizer {k : ℤ} {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F 𝒢 k] (f : F) (x : GL (Fin 2) ℝ) {a : GL (Fin 2) ℝ} (ha : a ∈ Subgroup.normalizer ↑ℋ) [(ConjAct.toConjAct x⁻¹ • 𝒢).IsFiniteRelIndex ℋ] [(ConjAct.toConjAct (x * a)⁻¹ • 𝒢).IsFiniteRelIndex ℋ] : ⇑(SlashInvariantForm.trace ℋ (SlashInvariantForm.translate f (x * a))) = SlashAction.map k a ⇑(SlashInvariantForm.trace ℋ (SlashInvariantForm.translate f x))

Translating by a normalizing element commutes with the trace. If a normalizes the level ℋ, the trace of the translate of f by x a is the slash by a of the trace of the translate by x. The cosets of the two traces correspond under conjugation by a.

@[simp]

theorem TauCeti.trace_translate_coe_cuspForm {k : ℤ} {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F 𝒢 k] (f : F) (x : GL (Fin 2) ℝ) [(ConjAct.toConjAct x⁻¹ • 𝒢).IsFiniteRelIndex ℋ] : ModularFormClass.modularForm (CuspForm.trace ℋ (CuspForm.translate f x)) = ModularForm.trace ℋ (ModularForm.translate f x)

Coercing the cusp-form trace of a translate agrees with tracing the corresponding translated modular form. Like trace_coe_cuspForm, this is class-polymorphic in the source form.

theorem TauCeti.isFiniteRelIndex_ratCast_conj {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℚ)} {δ : GL (Fin 2) ℚ} [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ δ⁻¹)] : (ConjAct.toConjAct ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) δ)⁻¹ • Subgroup.map (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) Γ₁).IsFiniteRelIndex (Subgroup.map (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) Γ₂)

A finite rational double-coset decomposition gives the finite relative index needed to trace a translate after extension of scalars to ℝ.

theorem TauCeti.heckeSlashSum_eq_coe_trace_translate {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℚ)} {δ : GL (Fin 2) ℚ} {Δ : Submonoid (GL (Fin 2) ℚ)} (k : ℤ) (D : HeckeCoset Δ Γ₁ Γ₂) [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] (hδ : δ ∈ DoubleCoset.doubleCoset ↑(Quotient.out D) ↑Γ₁ ↑Γ₂) {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} (hΓ₁ : Subgroup.map (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) Γ₁ = 𝒢) (hΓ₂ : Subgroup.map (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) Γ₂ = ℋ) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F 𝒢 k] (f : F) : have this := ⋯; HeckeRing.GL2.heckeSlashSum k D ⇑f = ⇑(SlashInvariantForm.trace ℋ (SlashInvariantForm.translate f ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) δ)))

The rational slash sum equals the trace of the translate by any representative of the same double coset. This statement needs only slash invariance, and allows different source and target groups.

instance TauCeti.isFiniteRelIndex_conj_mapGL {δ : GL (Fin 2) ℚ} {G H : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Finite (DoubleCoset.DecompQuotient (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) H) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G) δ⁻¹)] : (ConjAct.toConjAct ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) δ)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) G).IsFiniteRelIndex (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) H)

The real conjugate of an integral level has finite relative index whenever its rational right-coset decomposition is finite. This supplies the instance required by Mathlib's trace.

theorem TauCeti.heckeSlashCuspFormEnd_eq_trace_translate {δ : GL (Fin 2) ℚ} {G : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) G).IsArithmetic] {Δ : Submonoid (GL (Fin 2) ℚ)} (k : ℤ) (D : HeckeCoset Δ (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G)) [Finite (DoubleCoset.DecompQuotient (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G) (↑(Quotient.out D))⁻¹)] (hD : ↑(Quotient.out D) ∈ Matrix.GLPos (Fin 2) ℚ) (hδ : δ ∈ DoubleCoset.doubleCoset ↑(Quotient.out D) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) G)) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) G) k) : have this := ⋯; (HeckeRing.GL2.heckeSlashCuspFormEnd k D hD) f = CuspForm.trace (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) G) (CuspForm.translate f ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) δ))

The rational double-coset operator on cusp forms is Mathlib's trace of a translate. The representative δ may be chosen anywhere in the double coset.

theorem TauCeti.heckeTCuspNat_eq_trace_translate (N : ℕ) [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (HeckeRing.GL2.heckeTCuspNat k n) f = CuspForm.trace (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) (CuspForm.translate f ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (HeckeRing.GLn.natDiagGL 2 ![1, n])))

The operator attached to Γ₁(N) diag(1,n) Γ₁(N) is the trace of the translate by diag(1,n), with no additional normalization factor. The formula holds for every positive index, including indices divisible by primes in the level.