The upper-triangular Hecke operator on M_k(Γ₁(N)) and S_k(Γ₁(N))

The three analytic inputs for heckeSlashUpperTri are in place — holomorphy (UpperTri/Holomorphic.lean), boundedness and vanishing at every cusp (UpperTri/Cusps.lean), and UpperTri/Invariance.lean supplies the missing algebraic one: at p ∣ N the sum preserves Γ₁(N)-invariance. This file assembles them into the operator itself, a ℂ-linear endomorphism of ModularForm ((Gamma1 N).map (mapGL ℝ)) k and of CuspForm ((Gamma1 N).map (mapGL ℝ)) k. Nebentypus preservation and the q-expansion recurrence for the canonical heckeTNat operator are recorded at every level-supported index in HeckeSlash/LevelSupported.lean.

This is Layer 2(b) of the ModularForms roadmap at a level divisible by p. When p is prime, the classical Tₚ for p ∤ N needs one further coset representative and is not built here; at p ∣ N the classical Tₚ is this operator, which is why the corresponding prime Hecke recurrence carries no χ(p) p^{k-1} term. Following Miyake, Diamond–Shurman and Shimura, no separate Uₚ is introduced.

Where the level enters

HeckeSlash/ModularForm.lean already descends the general double-coset sum to forms, but only at level 𝒮ℒ, where invariance is Shimura's Proposition 3.37 and no congruence condition is involved. Neither file implies the other: that one has an arbitrary double coset and the full modular group, this one has a fixed family of representatives and a congruence subgroup, and it is the congruence condition p ∣ N that makes the upper-triangular representatives suffice.

The cusp conditions ask for Subgroup.IsArithmetic on the level, which (Gamma1 N).map (mapGL ℝ) carries through CongruenceSubgroup.instFiniteIndexGamma1 once N ≠ 0. Invariance is carried rationally throughout UpperTri/Invariance.lean, so the one place the ℚ/ℝ bridge is needed is ModularForm.rat_slash_mapGL, from ModularForms/SlashActionRat.lean.

Main definitions

• HeckeRing.GL2.heckeSlashUpperTriModularFormEnd: the operator on M_k(Γ₁(N)), bundled as a Module.End ℂ.
• HeckeRing.GL2.heckeSlashUpperTriCuspFormEnd: the operator on S_k(Γ₁(N)) — the statement that it preserves cuspidality.

Main results

• HeckeRing.GL2.coe_heckeSlashUpperTriModularFormEnd, HeckeRing.GL2.coe_heckeSlashUpperTriCuspFormEnd: both are heckeSlashUpperTri on underlying functions.

References

• F. Diamond and J. Shurman, A first course in modular forms, §5.2–5.3.
• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.5.

noncomputable def HeckeRing.GL2.heckeSlashUpperTriModularFormEnd {N p : ℕ} (k : ℤ) [NeZero N] (hpN : p ∣ N) : Module.End ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The upper-triangular Hecke operator on M_k(Γ₁(N)), for p ∣ N, as a ℂ-linear endomorphism. Bundling is what lets Hecke operators compose and later carry a ring structure.

Equations

• HeckeRing.GL2.heckeSlashUpperTriModularFormEnd k hpN = { toFun := HeckeRing.GL2.heckeSlashUpperTriModularForm✝ k hpN, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def HeckeRing.GL2.heckeSlashUpperTriCuspFormEnd {N p : ℕ} (k : ℤ) [NeZero N] (hpN : p ∣ N) : Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The upper-triangular Hecke operator on S_k(Γ₁(N)), for p ∣ N.

Equations

• HeckeRing.GL2.heckeSlashUpperTriCuspFormEnd k hpN = { toFun := HeckeRing.GL2.heckeSlashUpperTriCuspForm✝ k hpN, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HeckeRing.GL2.coe_heckeSlashUpperTriModularFormEnd {N p : ℕ} (k : ℤ) [NeZero N] (hpN : p ∣ N) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((heckeSlashUpperTriModularFormEnd k hpN) f) = heckeSlashUpperTri k p ⇑f

The operator is heckeSlashUpperTri on underlying functions.

@[simp]

theorem HeckeRing.GL2.coe_heckeSlashUpperTriCuspFormEnd {N p : ℕ} (k : ℤ) [NeZero N] (hpN : p ∣ N) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((heckeSlashUpperTriCuspFormEnd k hpN) f) = heckeSlashUpperTri k p ⇑f

The operator is heckeSlashUpperTri on underlying functions.