The bad-prime operator U_p

For a prime p dividing the level N, the classical operator often denoted U_p is not a second Hecke operator: it is the bad-prime specialization of the uniform operator T_p. This file introduces heckeUNat and heckeUCuspNat as aliases of heckeTNat and heckeTCuspNat, with the hypotheses p.Prime and p ∣ N making the bad-prime convention explicit in their types.

The theorem heckeUNat_eq_heckeTNat records the normalization promised by the ModularForms roadmap. All operational properties of U_p are inherited directly from the existing T_p API through this equality.

Main definitions

• HeckeRing.GL2.heckeUNat: the bad-prime alias of T_p on modular forms.
• HeckeRing.GL2.heckeUCuspNat: the corresponding alias on cusp forms.

Main results

• HeckeRing.GL2.heckeUNat_eq_heckeTNat and HeckeRing.GL2.heckeUCuspNat_eq_heckeTCuspNat: U_p = T_p.

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.12.

@[reducible, inline]

noncomputable abbrev HeckeRing.GL2.heckeUNat {N : ℕ} [NeZero N] (k : ℤ) (p : ℕ) (hp : Nat.Prime p) (_hpN : p ∣ N) : Module.End ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The bad-prime operator U_p on M_k(Γ₁(N)). For a prime p ∣ N, this is an alias of the uniform Hecke operator T_p, not an independently defined operator.

Equations

• HeckeRing.GL2.heckeUNat k p hp _hpN = HeckeRing.GL2.heckeTNat k p

@[reducible, inline]

noncomputable abbrev HeckeRing.GL2.heckeUCuspNat {N : ℕ} [NeZero N] (k : ℤ) (p : ℕ) (hp : Nat.Prime p) (_hpN : p ∣ N) : Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The bad-prime operator U_p on S_k(Γ₁(N)). It is the cusp-form alias of the uniform operator T_p.

Equations

• HeckeRing.GL2.heckeUCuspNat k p hp _hpN = HeckeRing.GL2.heckeTCuspNat k p

theorem HeckeRing.GL2.heckeUNat_eq_heckeTNat {N p : ℕ} [NeZero N] (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) : heckeUNat k p hp hpN = heckeTNat k p

At a prime dividing the level, U_p = T_p on modular forms.

theorem HeckeRing.GL2.heckeUCuspNat_eq_heckeTCuspNat {N p : ℕ} [NeZero N] (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) : heckeUCuspNat k p hp hpN = heckeTCuspNat k p

At a prime dividing the level, U_p = T_p on cusp forms.