The upper-triangular part of the Hecke operator

The classical T_p contains a sum of slashes by the representatives !![1, b; 0, p] for b < p, together with one further, diamond-twisted term when p ∤ N. This file defines the triangular sum heckeSlashUpperTri and records its ℂ-linearity in f: zero, addition and scalar multiplication are preserved. (Linearity in f only; it is not yet bundled as a LinearMap.)

Why these representatives: mathlib's IsBoundedAtImInfty.slash requires g 1 0 = 0, so it applies when g is upper triangular. (Sufficient, not necessary — the zero function stays bounded after slashing by any matrix.) Having that hypothesis to hand is why the classical arguments are organised around !![1, b; 0, p]. It is discharged by upperTriRep_apply_one_zero in HeckeRing/GL2/CosetDecomposition.lean, the (1, 0) case of upperTriGL_apply_eq_zero_of_lt — the entrywise description of the representatives is not restated.

Main definitions

• HeckeRing.GL2.heckeSlashUpperTri: the sum ∑ b < p, f ∣[k] !![1, b; 0, p].

Main results

• HeckeRing.GL2.heckeSlashUpperTri_def and heckeSlashUpperTri_apply: the characteristic equation and its pointwise form, the convenient rewrites for turning the operator back into its sum.
• HeckeRing.GL2.heckeSlashUpperTri_zero, heckeSlashUpperTri_add, heckeSlashUpperTri_smul: linearity in f.
• HeckeRing.GL2.heckeSlashUpperTri_heckeSlashUpperTri: the sums compose, the p-term sum of the n-term sum being the (n · p)-term sum. The representatives themselves, and their upper-triangularity and positive determinant, live in HeckeRing/GL2/CosetDecomposition.lean; this file is only the slash sum built from them.

Provenance

The shape is AINTLIB's heckeT_p_ut (LeanModularForms/HeckeRIngs/GL2/HeckeT_p.lean, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck): ∑ b ∈ Finset.range p, f ∣[k] T_p_upper p hp b. Restated over this repository's own representatives — T_p_upper p _ b is upperTriGL at n = 2, a = ![1, p] — so AINTLIB's T_p_upper is not reproduced.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4.
• [DS] Diamond–Shurman, A first course in modular forms, Proposition 5.2.1.

noncomputable def HeckeRing.GL2.heckeSlashUpperTri (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ) : UpperHalfPlane → ℂ

The upper-triangular part of the Hecke operator: ∑ b < p, f ∣[k] !![1, b; 0, p].

Equations

• HeckeRing.GL2.heckeSlashUpperTri k p f = ∑ b : Fin p, SlashAction.map k (HeckeRing.GL2.upperTriRep p b) f

theorem HeckeRing.GL2.heckeSlashUpperTri_def (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ) : heckeSlashUpperTri k p f = ∑ b : Fin p, SlashAction.map k (upperTriRep p b) f

The defining equation of heckeSlashUpperTri: the convenient rewrite for turning the operator back into its sum.

theorem HeckeRing.GL2.heckeSlashUpperTri_apply (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane) : heckeSlashUpperTri k p f τ = ∑ b : Fin p, SlashAction.map k (upperTriRep p b) f τ

The pointwise form of the defining equation: consumers working at a point of ℍ — cusp and q-expansion arguments in particular — need the value, not the function.

@[simp]

theorem HeckeRing.GL2.heckeSlashUpperTri_one (k : ℤ) (f : UpperHalfPlane → ℂ) : heckeSlashUpperTri k 1 f = f

At index one the upper-triangular sum is the identity: its unique representative is the identity matrix.

@[simp]

theorem HeckeRing.GL2.heckeSlashUpperTri_zero (k : ℤ) (p : ℕ) : heckeSlashUpperTri k p 0 = 0

The sum sends the zero function to zero.

@[simp]

theorem HeckeRing.GL2.heckeSlashUpperTri_add (k : ℤ) (p : ℕ) (f g : UpperHalfPlane → ℂ) : heckeSlashUpperTri k p (f + g) = heckeSlashUpperTri k p f + heckeSlashUpperTri k p g

The sum is additive in f, since each slash is.

@[simp]

theorem HeckeRing.GL2.heckeSlashUpperTri_smul (k : ℤ) (p : ℕ) {α : Type u_1} [DistribSMul α ℂ] [IsScalarTower α ℂ ℂ] (c : α) (f : UpperHalfPlane → ℂ) : heckeSlashUpperTri k p (c • f) = c • heckeSlashUpperTri k p f

Scalars pass through the sum. With heckeSlashUpperTri_add and heckeSlashUpperTri_zero this is the ℂ-linearity of f ↦ heckeSlashUpperTri k p f. The scalar generality matches ModularForm.rat_smul_slash_of_det_pos.

@[simp]

theorem HeckeRing.GL2.heckeSlashUpperTri_heckeSlashUpperTri (k : ℤ) (p n : ℕ) (f : UpperHalfPlane → ℂ) : heckeSlashUpperTri k p (heckeSlashUpperTri k n f) = heckeSlashUpperTri k (n * p) f

The upper-triangular sums compose: the p-term sum of the n-term sum is the (n · p)-term sum,

∑_{b < p} (∑_{b' < n} f ∣[k] !![1, b'; 0, n]) ∣[k] !![1, b; 0, p] = ∑_{c < n·p} f ∣[k] !![1, c; 0, n·p].

Both sides are sums of slashes of f by representatives, and upperTriRep_mul_upperTriRep matches the index pair (b', b) with the offset finProdFinEquiv (b', b) of the composite family; that map is a bijection, so each composite representative occurs exactly once.

No divisibility, primality or level hypothesis enters: this is an identity of finite sums of slashes, valid for every f : ℍ → ℂ.