The Hecke operators at an index supported on the level

Call a positive integer n supported on the level N when every prime factor of n divides N, that is n.primeFactors ⊆ N.primeFactors. These are the indices at which the decomposition of HeckeRing/GL2/Gamma1/UpperTriCosets.lean writes the double coset Γ₁(N) · diag(1, n) · Γ₁(N) as n upper-triangular right cosets Γ₁(N) · !![1, b; 0, n] — no further coset appears, as it does at a prime p ∤ N. The prime powers p ^ r with p ∣ N are supported on the level whether or not they divide it, and they are the reason this regime is worth naming: p ∣ N alone does not reach T_{p²}.

Consequently T_n is the plain upper-triangular sum there, and — this is the point — these operators multiply: composing the m-term and the n-term sums enumerates the (n·m)-term sum exactly once each, so

T_n T_m = T_{n m} for n and m supported on the level,

with T_{p^r} = T_p ^ r at p ∣ N as the special case the ModularForms roadmap names. In the vocabulary of modern papers the operator at p ∣ N is U_p (heckeUNat, an alias of T_p by heckeUNat_eq_heckeTNat), so the same statement reads T_{p^r} = U_p ^ r; no second operator is introduced.

⚠ This does not supply multiplicativity for arbitrary coprime indices: it applies when each index is supported on the level, whether or not the two indices are coprime. An index with a prime factor outside the level needs the whole coset decomposition of Gamma1/CoprimeCosets.lean. In the level-supported case the identity degenerates the prime-power recurrence T_{p^{r+2}} = T_p T_{p^{r+1}} − p^{k−1}⟨p⟩ T_{p^r} to T_{p^r} = T_p ^ r, the zero-extended diamond ⟨p⟩ vanishing at p ∣ N.

Two consequences are recorded alongside: T_n preserves each nebentypus space M_k(N, χ) and S_k(N, χ) there, and its effect on q-expansions is aₘ(T_n f) = a_{n m}(f), proved from the function-level recurrence in UpperTri/QExpansion.lean.

Main results

• HeckeRing.GL2.coe_heckeTNat_of_primeFactors_subset and HeckeRing.GL2.coe_heckeTCuspNat_of_primeFactors_subset: at an index supported on the level, T_n is the upper-triangular sum.
• HeckeRing.GL2.heckeTNat_mul_of_primeFactors_subset and its cusp-form counterpart: T_{n m} = T_n ∘ T_m for two indices supported on the level, with HeckeRing.GL2.commute_heckeTNat_of_primeFactors_subset recording that such operators commute.
• HeckeRing.GL2.heckeTNat_pow_of_primeFactors_subset: T_{n^r} = T_n ^ r at every level-supported index, with its cusp-form counterpart.
• HeckeRing.GL2.heckeTNat_pow_of_dvd: T_{p^r} = T_p ^ r at p ∣ N, with its cusp-form counterpart.
• HeckeRing.GL2.heckeTNat_mem_modFormCharSpace_of_primeFactors_subset with its cusp-form counterpart: the operator preserves M_k(N, χ) and S_k(N, χ).
• HeckeRing.GL2.qExpansion_coeff_heckeTNat_of_primeFactors_subset and its cusp-form counterpart: aₘ(T_n f) = a_{n m}(f).
• HeckeRing.GL2.heckeTNat_eq_smul_iff_forall_qExpansion_coeff_mul_of_primeFactors_subset and its cusp-form counterpart characterize the eigen-relation by a_{nm}(f) = c a_m(f).

Provenance

No code is transcribed. The prime-power statement is the ModularForms roadmap's Layer 2(b) milestone, carried in the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0) as heckeT_ppow_eq_pow_of_not_coprime (LeanModularForms/HeckeRIngs/GL2/MultiplicationTable.lean); there it is a statement about a family of operators assembled prime by prime, while here it falls out of the composition law for the coset representatives, which holds at every pair of level-supported indices and not only at powers of one prime.

References

• F. Diamond and J. Shurman, A first course in modular forms, Propositions 5.2.1--5.2.2 and equations (5.3)--(5.4).
• T. Miyake, Modular forms, §4.5, Lemma 4.5.7.
• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.5.

theorem HeckeRing.GL2.coe_heckeTNat_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((heckeTNat k n) f) = heckeSlashUpperTri k n ⇑f

At an index supported on the level, T_n is the upper-triangular sum ∑_{b < n} f ∣[k] !![1, b; 0, n]. This is the normalisation lemma of UpperTri/DoubleCoset.lean at every such index, not only at the divisors of N.

theorem HeckeRing.GL2.coe_heckeTCuspNat_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((heckeTCuspNat k n) f) = heckeSlashUpperTri k n ⇑f

At an index supported on the level, the cusp-form T_n is the upper-triangular sum.

theorem HeckeRing.GL2.heckeTNat_mul_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) {n m : ℕ} [NeZero n] [NeZero m] (hn : n.primeFactors ⊆ N.primeFactors) (hm : m.primeFactors ⊆ N.primeFactors) : heckeTNat k (n * m) = heckeTNat k n * heckeTNat k m

The Hecke operators at indices supported on the level multiply: T_{n m} = T_n ∘ T_m on M_k(Γ₁(N)).

Both sides are upper-triangular sums, and upperTriRep_mul_upperTriRep matches the pairs of representatives with the representatives at index n · m bijectively. Nothing here is a coprimality statement: each of n and m is supported on the level, and the identity holds whether or not they are coprime (in particular, for n = m).

theorem HeckeRing.GL2.heckeTCuspNat_mul_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) {n m : ℕ} [NeZero n] [NeZero m] (hn : n.primeFactors ⊆ N.primeFactors) (hm : m.primeFactors ⊆ N.primeFactors) : heckeTCuspNat k (n * m) = heckeTCuspNat k n * heckeTCuspNat k m

The cusp-form Hecke operators at indices supported on the level multiply: T_{n m} = T_n ∘ T_m on S_k(Γ₁(N)).

theorem HeckeRing.GL2.commute_heckeTNat_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) {n m : ℕ} [NeZero n] [NeZero m] (hn : n.primeFactors ⊆ N.primeFactors) (hm : m.primeFactors ⊆ N.primeFactors) : Commute (heckeTNat k n) (heckeTNat k m)

The Hecke operators at indices supported on the level commute. Both orders compute the operator at the product index, and the product of indices is commutative. This is the commuting family the simultaneous-diagonalisation arguments consume at the bad primes.

theorem HeckeRing.GL2.commute_heckeTCuspNat_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) {n m : ℕ} [NeZero n] [NeZero m] (hn : n.primeFactors ⊆ N.primeFactors) (hm : m.primeFactors ⊆ N.primeFactors) : Commute (heckeTCuspNat k n) (heckeTCuspNat k m)

The cusp-form Hecke operators at indices supported on the level commute.

theorem HeckeRing.GL2.heckeTNat_pow_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) {n : ℕ} [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) (r : ℕ) : heckeTNat k (n ^ r) = heckeTNat k n ^ r

T_{n^r} = T_n ^ r at an index supported on the level.

theorem HeckeRing.GL2.heckeTCuspNat_pow_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) {n : ℕ} [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) (r : ℕ) : heckeTCuspNat k (n ^ r) = heckeTCuspNat k n ^ r

T_{n^r} = T_n ^ r on cusp forms, at an index supported on the level.

theorem HeckeRing.GL2.heckeTNat_pow_of_dvd {N p : ℕ} [NeZero N] (k : ℤ) (hpN : p ∣ N) (r : ℕ) : heckeTNat k (p ^ r) = heckeTNat k p ^ r

T_{p^r} = T_p ^ r at a divisor p ∣ N, on M_k(Γ₁(N)).

The roadmap's prime case is the degenerate case of the prime-power recurrence T_{p^{r+2}} = T_p T_{p^{r+1}} − p^{k−1} ⟨p⟩ T_{p^r}: the zero-extended diamond ⟨p⟩ vanishes at a prime p ∣ N, leaving T_{p^{r+1}} = T_p T_{p^r}. In that case, read through heckeUNat_eq_heckeTNat, the statement is T_{p^r} = U_p ^ r; there is no second operator.

theorem HeckeRing.GL2.heckeTCuspNat_pow_of_dvd {N p : ℕ} [NeZero N] (k : ℤ) (hpN : p ∣ N) (r : ℕ) : heckeTCuspNat k (p ^ r) = heckeTCuspNat k p ^ r

T_{p^r} = T_p ^ r at a divisor p ∣ N, on S_k(Γ₁(N)).

theorem HeckeRing.GL2.heckeTNat_mem_modFormCharSpace_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (n : ℕ) [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k χ) : (heckeTNat k n) f ∈ modFormCharSpace k χ

T_n preserves the nebentypus at every index supported on the level: it maps M_k(N, χ) into itself. Not an assumption but a theorem, as the ModularForms roadmap asks of the Hecke action.

theorem HeckeRing.GL2.heckeTCuspNat_mem_cuspFormCharSpace_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (n : ℕ) [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) : (heckeTCuspNat k n) f ∈ cuspFormCharSpace k χ

T_n preserves the nebentypus on cusp forms: it maps S_k(N, χ) into itself, at every index supported on the level.

theorem HeckeRing.GL2.qExpansion_coeff_heckeTNat_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑((heckeTNat k n) f)) = (PowerSeries.coeff (n * m)) (UpperHalfPlane.qExpansion 1 ⇑f)

The q-expansion recurrence at an index supported on the level: aₘ(T_n f) = a_{n m}(f). When f lies in a nebentypus-χ space, at a prime p ∣ N this is the Diamond–Shurman recurrence aₘ(Tₚ f) = a_{m p}(f) + χ(p) p^{k-1} a_{m/p}(f) with its second term killed by χ(p) = 0; at n = p ^ r it is the r-fold iterate of that.

theorem HeckeRing.GL2.qExpansion_coeff_heckeTCuspNat_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑((heckeTCuspNat k n) f)) = (PowerSeries.coeff (n * m)) (UpperHalfPlane.qExpansion 1 ⇑f)

The q-expansion recurrence on cusp forms: aₘ(T_n f) = a_{n m}(f) at an index supported on the level.

theorem HeckeRing.GL2.heckeTNat_eq_smul_iff_forall_qExpansion_coeff_mul_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) {n : ℕ} [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) {F : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (c : ℂ) : (heckeTNat k n) F = c • F ↔ ∀ (m : ℕ), (PowerSeries.coeff (n * m)) (UpperHalfPlane.qExpansion 1 ⇑F) = c * (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑F)

The coefficient characterization of an eigen-relation at a level-supported index, on modular forms. If every prime factor of n divides N, then T_n F = c • F if and only if a_{nm}(F) = c a_m(F) for every m.

No nonvanishing hypothesis on F is needed: this characterizes an equation rather than the property of being an eigenvector.

theorem HeckeRing.GL2.heckeTCuspNat_eq_smul_iff_forall_qExpansion_coeff_mul_of_primeFactors_subset {N : ℕ} [NeZero N] (k : ℤ) {n : ℕ} [NeZero n] (hn : n.primeFactors ⊆ N.primeFactors) {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (c : ℂ) : (heckeTCuspNat k n) F = c • F ↔ ∀ (m : ℕ), (PowerSeries.coeff (n * m)) (UpperHalfPlane.qExpansion 1 ⇑F) = c * (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑F)

The coefficient characterization of an eigen-relation at a level-supported index, on cusp forms. If every prime factor of n divides N, then T_n F = c • F if and only if a_{nm}(F) = c a_m(F) for every m.