The slash sum of a Γ₁-invariant function is Γ₂-invariant

heckeSlashSum is a sum over chosen coset representatives, and HeckeSlash/Basic.lean records that on a general f : ℍ → ℂ the value depends on those choices. This file proves the theorem that repairs it: if f is invariant under the weight-k slash action of Γ₁, then heckeSlashSum k D f is invariant under that of Γ₂.

That is the content of Shimura's Proposition 3.37 — right multiplication by γ ∈ Γ₂ merely permutes the right cosets Γ₁ aᵥ of the decomposition, so the sum is unchanged. Concretely aᵥ γ = δ τᵥ⁻¹ γ = δ (γ⁻¹ τᵥ)⁻¹, so the permutation is v ↦ γ⁻¹ • v for the action of Γ₂ on Γ₂ ⧸ (Γ₂ ∩ δ⁻¹Γ₁δ) — MulAction.toPerm at γ⁻¹ — and the per-summand step is slash_rightCosetRep_of_mem_right from HeckeSlash/Reindex.lean.

⚠ The two groups are different: the hypothesis is invariance under Γ₁ and the conclusion is invariance under Γ₂. They agree on a diagonal triple HeckeCoset Δ Γ Γ, which is where the Hecke operators of Layer 2(b) live, but nothing here needs them to.

Main results

• HeckeRing.GL2.heckeSlashSum_slash_invariant: for γ ∈ Γ₂ and Γ₁-invariant f, heckeSlashSum k D f ∣[k] γ = heckeSlashSum k D f.

Provenance

The statement corresponds to heckeSlash_slash_invariant in the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/HeckeAction.lean, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck), lines 198–246, together with its helper tRep_mul_eq_transpose. No code is transcribed: that proof permutes a left-coset index by transposing, so it holds only where every group in sight is transpose-stable — level one — while the argument below is Shimura's own and quantifies over γ ∈ Γ₂ at an arbitrary triple. As in Reindex.lean, invariance is carried under the rational slash action rather than routed through a real subgroup, so AINTLIB's mem_SL_exists_H bridge is not needed.

References

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

@[instance_reducible]

noncomputable def HeckeRing.GL2.instFintypeDecompQuotientGeneralLinearGroupFinOfNatNatRatInvValMemSubmonoidOutSubtype_1 {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℚ)} (D : HeckeCoset Δ Γ₁ Γ₂) [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] : Fintype (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)

The enumeration the reindexing argument needs, chosen exactly as in HeckeSlash/Basic.lean so that the two ∑s are the same term.

Equations

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

theorem HeckeRing.GL2.heckeSlashSum_slash_invariant (k : ℤ) {Δ : Submonoid (GL (Fin 2) ℚ)} {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℚ)} (D : HeckeCoset Δ Γ₁ Γ₂) [Finite (DoubleCoset.DecompQuotient Γ₂ Γ₁ (↑(Quotient.out D))⁻¹)] (f : UpperHalfPlane → ℂ) (hf : ∀ δ ∈ Γ₁, SlashAction.map k δ f = f) {γ : GL (Fin 2) ℚ} (hγ : γ ∈ Γ₂) : SlashAction.map k γ (heckeSlashSum k D f) = heckeSlashSum k D f

The slash sum of a Γ₁-invariant function is Γ₂-invariant. For f invariant under the weight-k slash action of Γ₁ and γ ∈ Γ₂, heckeSlashSum k D f ∣[k] γ = heckeSlashSum k D f.

The proof is Shimura's — right multiplication by γ permutes the summands — and the permutation is MulAction.toPerm applied to γ⁻¹, acting on the right-coset index Γ₂ ⧸ (Γ₂ ∩ δ⁻¹Γ₁δ).

⚠ This proves invariance of the sum formed from the representatives D.out and v.out that heckeSlashSum fixes. That sums formed from different choices of representatives agree is a separate theorem, heckeSlashSum_eq_sum_of_rightCosets in HeckeSlash/Independence.lean.