Hecke sums on a representation of the monoid Δ

Let D = Γ₁ δ Γ₂ be a double coset in a group G with finitely many right cosets of Γ₁, with chosen representative δ = D.out. Let ρ be a representation of a submonoid Δ' ≤ G containing δ and Γ₂ on an R-module V. For semirings R, S and σ : R →+* S, let q : V →ₛₗ[σ] W be a semilinear map to an S-module W. The decomposition Γ₁ δ Γ₂ = ⊔ᵥ Γ₁ aᵥ into right cosets with representatives aᵥ = rightCosetRep D v defines the Hecke sum

heckeSum D ρ q = ∑ᵥ q ∘ ρ(aᵥ) : V →ₛₗ[σ] W,

the sum over the chosen representatives. Taking S = R and σ = RingHom.id R recovers linear maps over R; allowing a different S also covers maps that extend or twist the coefficients. The two invariance theorems are Shimura's, §3.4, transposed from functions to a representation:

• when q is Γ₁-invariant — q ∘ ρ(γ₁) = q for γ₁ ∈ Γ₁ — the sum is independent of the representatives (heckeSum_eq_sum_of_rightCosets): any family (aᵢ) naming each right coset of Γ₁ δ Γ₂ exactly once gives the same map;
• under the same hypothesis the sum is Γ₂-invariant (heckeSum_comp_of_mem): heckeSum D ρ q ∘ ρ(γ) = heckeSum D ρ q for γ ∈ Γ₂, because right multiplication by γ permutes the right cosets Γ₁ aᵥ.

The second statement is what lets the Hecke sum descend to the Γ₂-coinvariants of V when q is the projection onto the Γ₁-coinvariants: a double coset then induces a map V_{Γ₂} → V_{Γ₁}, the Hecke operator on coinvariants. That descent is carried out where the coinvariants are, for the modular symbols in TauCeti.NumberTheory.ModularForms.ModularSymbols.Hecke.Basic; here q is an arbitrary Γ₁-invariant map so that the two theorems apply to coinvariants formed over any group whose image in G is Γ₁.

The slash sums of TauCeti.NumberTheory.ModularForms.HeckeSlash are the same construction for the right action of GL(2, ℚ) on functions ℍ → ℂ, where invariance under Γ₁ is invariance of the function itself and the sum acts on invariants rather than descending to coinvariants.

Main definitions

• HeckeCoset.heckeSum: the sum ∑ᵥ q ∘ ρ(aᵥ) over the chosen right-coset representatives.

Main results

• Representation.comp_eq_of_rightCoset_eq (in RepresentationTheory/Coset.lean): for Γ₁-invariant q, q ∘ ρ(x) depends only on the right coset Γ₁ x.
• HeckeCoset.heckeSum_zero and HeckeCoset.heckeSum_add: additivity in the target map.
• HeckeCoset.heckeSum_eq_sum_of_rightCosets: the choice-free description of the Hecke sum.
• HeckeCoset.heckeSum_comp_of_mem: the Hecke sum of a Γ₁-invariant map is Γ₂-invariant.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4, (3.4.1) and Proposition 3.37.

@[instance_reducible]

noncomputable def HeckeCoset.instFintypeDecompQuotientInvValMemSubmonoidOutSubtype {G : Type u_1} [Group G] {Δ : Submonoid G} {Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] : Fintype (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)

A chosen finite enumeration of the right-coset index. A Hecke triple supplies the Finite assumption, but the sum needs only finiteness of this index.

Equations

• D.instFintypeDecompQuotientInvValMemSubmonoidOutSubtype = Fintype.ofFinite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)

noncomputable def HeckeCoset.heckeSum {G : Type u_1} [Group G] {Δ Δ' : Submonoid G} {Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) {R : Type u_2} {S : Type u_3} {V : Type u_4} {W : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module S W] {σ : R →+* S} (ρ : Representation R (↥Δ') V) (hD : ↑(Quotient.out D) ∈ Δ') (hΓ₂ : Γ₂.toSubmonoid ≤ Δ') (q : V →ₛₗ[σ] W) [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] : V →ₛₗ[σ] W

The Hecke sum of a double coset on a representation. For Γ₁ δ Γ₂ = ⊔ᵥ Γ₁ aᵥ with aᵥ = rightCosetRep D v, this is ∑ᵥ q ∘ ρ(aᵥ) : V →ₛₗ[σ] W.

⚠ It is a sum over the chosen representatives D.out and v.out, and for an arbitrary q it depends on them. For a Γ₁-invariant q it does not (heckeSum_eq_sum_of_rightCosets), and it is then Γ₂-invariant (heckeSum_comp_of_mem).

The representatives act through ρ because they lie in Δ': only the chosen D.out and Γ₂ are required to (rightCosetRep_mem), not the whole of Δ.

Equations

• D.heckeSum ρ hD hΓ₂ q = ∑ v : DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹, q ∘ₛₗ ρ ⟨DoubleCoset.rightCosetRep D v, ⋯⟩

theorem HeckeCoset.heckeSum_def {G : Type u_1} [Group G] {Δ Δ' : Submonoid G} {Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) {R : Type u_2} {S : Type u_3} {V : Type u_4} {W : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module S W] {σ : R →+* S} (ρ : Representation R (↥Δ') V) (hD : ↑(Quotient.out D) ∈ Δ') (hΓ₂ : Γ₂.toSubmonoid ≤ Δ') (q : V →ₛₗ[σ] W) [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] : D.heckeSum ρ hD hΓ₂ q = ∑ v : DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹, q ∘ₛₗ ρ ⟨DoubleCoset.rightCosetRep D v, ⋯⟩

The defining equation of heckeSum. Since heckeSum is not @[expose], a downstream module rewrites with this instead of unfolding the body.

theorem HeckeCoset.heckeSum_apply {G : Type u_1} [Group G] {Δ Δ' : Submonoid G} {Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) {R : Type u_2} {S : Type u_3} {V : Type u_4} {W : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module S W] {σ : R →+* S} (ρ : Representation R (↥Δ') V) (hD : ↑(Quotient.out D) ∈ Δ') (hΓ₂ : Γ₂.toSubmonoid ≤ Δ') (q : V →ₛₗ[σ] W) [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] (x : V) : (D.heckeSum ρ hD hΓ₂ q) x = ∑ v : DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹, q ((ρ ⟨DoubleCoset.rightCosetRep D v, ⋯⟩) x)

The Hecke sum, evaluated: heckeSum D ρ q x = ∑ᵥ q (ρ(aᵥ) x).

@[simp]

theorem HeckeCoset.heckeSum_zero {G : Type u_1} [Group G] {Δ Δ' : Submonoid G} {Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) {R : Type u_2} {S : Type u_3} {V : Type u_4} {W : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module S W] {σ : R →+* S} (ρ : Representation R (↥Δ') V) (hD : ↑(Quotient.out D) ∈ Δ') (hΓ₂ : Γ₂.toSubmonoid ≤ Δ') [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] : D.heckeSum ρ hD hΓ₂ 0 = 0

The Hecke sum of the zero map is zero.

@[simp]

theorem HeckeCoset.heckeSum_add {G : Type u_1} [Group G] {Δ Δ' : Submonoid G} {Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) {R : Type u_2} {S : Type u_3} {V : Type u_4} {W : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module S W] {σ : R →+* S} (ρ : Representation R (↥Δ') V) (hD : ↑(Quotient.out D) ∈ Δ') (hΓ₂ : Γ₂.toSubmonoid ≤ Δ') [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] (q₁ q₂ : V →ₛₗ[σ] W) : D.heckeSum ρ hD hΓ₂ (q₁ + q₂) = D.heckeSum ρ hD hΓ₂ q₁ + D.heckeSum ρ hD hΓ₂ q₂

The Hecke sum is additive in the target map.

theorem HeckeCoset.heckeSum_eq_sum_of_rightCosets {G : Type u_1} [Group G] {Δ Δ' : Submonoid G} {Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) {R : Type u_2} {S : Type u_3} {V : Type u_4} {W : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module S W] {σ : R →+* S} (ρ : Representation R (↥Δ') V) (hD : ↑(Quotient.out D) ∈ Δ') (hΓ₂ : Γ₂.toSubmonoid ≤ Δ') {q : V →ₛₗ[σ] W} [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] (hΓ₁ : Γ₁.toSubmonoid ≤ Δ') (hq : ∀ (γ : G) (hγ : γ ∈ Γ₁), q ∘ₛₗ ρ ⟨γ, ⋯⟩ = q) {ι : Type u_6} [Fintype ι] (a : ι → G) (ha : ∀ (i : ι), a i ∈ Δ') (hcover : DoubleCoset.doubleCoset ↑(Quotient.out D) ↑Γ₁ ↑Γ₂ = ⋃ (i : ι), MulOpposite.op (a i) • ↑Γ₁) (hinj : Function.Injective fun (i : ι) => MulOpposite.op (a i) • ↑Γ₁) : D.heckeSum ρ hD hΓ₂ q = ∑ i : ι, q ∘ₛₗ ρ ⟨a i, ⋯⟩

The Hecke sum of a Γ₁-invariant map is the sum over any decomposition of the double coset into right cosets. If the right cosets Γ₁ aᵢ are pairwise distinct and cover Γ₁ D.out Γ₂, then heckeSum D ρ q = ∑ᵢ q ∘ ρ(aᵢ).

So the map is attached to the double coset itself: the representatives D.out and v.out that heckeSum happens to pick are one such family, and every other family gives the same map. The hypothesis ha records that the family lies in the monoid ρ acts through; it is automatic when the family lies in the double coset and Γ₁ ≤ Δ'.

theorem HeckeCoset.heckeSum_comp_of_mem {G : Type u_1} [Group G] {Δ Δ' : Submonoid G} {Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) {R : Type u_2} {S : Type u_3} {V : Type u_4} {W : Type u_5} [Semiring R] [Semiring S] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module S W] {σ : R →+* S} (ρ : Representation R (↥Δ') V) (hD : ↑(Quotient.out D) ∈ Δ') (hΓ₂ : Γ₂.toSubmonoid ≤ Δ') {q : V →ₛₗ[σ] W} [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] (hΓ₁ : Γ₁.toSubmonoid ≤ Δ') (hq : ∀ (γ : G) (hγ : γ ∈ Γ₁), q ∘ₛₗ ρ ⟨γ, ⋯⟩ = q) {γ : G} (hγ : γ ∈ Γ₂) : D.heckeSum ρ hD hΓ₂ q ∘ₛₗ ρ ⟨γ, ⋯⟩ = D.heckeSum ρ hD hΓ₂ q

The Hecke sum of a Γ₁-invariant map is Γ₂-invariant. For γ ∈ Γ₂, heckeSum D ρ q ∘ ρ(γ) = heckeSum D ρ q.

This is the invariance needed to descend the sum to the Γ₂-coinvariants of V.