The diagonal generators of the Γ₀(N) Hecke ring

This file builds the two generating classes of the Hecke ring R(Γ₀(N), Δ₀(N)) on top of the general diagonal element diagElemGamma0 from Diagonal/Elem.lean, together with the family the Diamond–Shurman recurrence assembles.

The two generators specialise that element: heckeTGeneratorGamma0 p at ![1, p] and heckeTScalarGamma0 p at ![p, p]. The iterated family heckeTGeneratorRecGamma0 p r satisfies T₀ = 1, T₁ = T_p and

T_{r+2} = T_p · T_{r+1} − (p · S_p) · T_r,

which when p shares a factor with the level degenerates to T_r = T_p^r, the scalar term having vanished.

Every declaration here is stated for an arbitrary natural p, and the names say so: they follow heckeTDiag/heckeTScalar/heckeT at level one (GL2/Basic.lean), none of which asks Nat.Prime either. The elements are the classical T_p and T_{p^r} of Γ₀(N) exactly when p is prime — that is the intended reading, and the recurrence is chosen to match it — but nothing below assumes it, so nothing below is named for it.

The composite element assembled over a prime factorisation is not built here; this file supplies the generators it needs, and the per-prime product formula they satisfy.

Main definitions

• HeckeRing.GL2.heckeTGeneratorGamma0: the generator Γ₀(N)·diag(1, p)·Γ₀(N).
• HeckeRing.GL2.heckeTScalarGamma0: the scalar generator Γ₀(N)·diag(p, p)·Γ₀(N), or 0.
• HeckeRing.GL2.heckeTGeneratorRecGamma0: the family the recurrence generates.

Main results

• HeckeRing.GL2.heckeTGeneratorRecGamma0_succ_succ: the recurrence, as a rewriting rule.
• HeckeRing.GL2.heckeTGeneratorRecGamma0_eq_generator_pow_of_not_coprime: when p shares a factor with the level, the recurrence degenerates to a power of the generator.
• HeckeRing.GL2.heckeTGeneratorRecGamma0_mul: Shimura, Theorem 3.24(3) at level Γ₀(N), the per-prime product formula T_{p^r} · T_{p^s} = ∑_{i ≤ r} pⁱ · S_pⁱ · T_{p^{r+s−2i}} for r ≤ s.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.3.
• Diamond–Shurman, A first course in modular forms, §5.3 — the prime-power recurrence T_{p^{r+1}} = T_p T_{p^r} − p^{k−1}⟨p⟩ T_{p^{r−1}} this file's heckeTGeneratorRecGamma0 transcribes to the ring.
• Ported from AINTLIB commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck, LeanModularForms/HeckeRIngs/GL2/Unified/Gamma0RingDn.lean, declarations heckeRingDp, heckeRingSpp, heckeRingSpp_of_not_coprime, heckeRingDppow, heckeRingDppow_zero, heckeRingDppow_one, heckeRingDppow_succ_succ, heckeRingDppow_eq_pow_of_not_coprime and heckeRingDppow_mul. Four hypotheses of the source are dropped here: the generator no longer asks 0 < p, and none of the scalar generator, the iterated family and the product formula asks Nat.Prime p — none is needed to define the elements, to prove the recurrence, or to derive the product formula from it, and carrying them would force every consumer to supply a primality proof for a statement that does not use it. The names follow this namespace's heckeT* family rather than the source's heckeRing*, and drop the source's p/prime vocabulary along with the hypothesis it stood for.

noncomputable def HeckeRing.GL2.heckeTGeneratorGamma0 (N p : ℕ) : HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ

The diagonal generator of the Γ₀(N) Hecke ring: for 0 < p the class of Γ₀(N)·diag(1, p)·Γ₀(N), including when p shares a factor with the level, and 0 at p = 0. At a prime p this is the classical T_p.

No coprimality is asked of p: the head entry of ![1, p] is 1, which is coprime to every level, so only positivity can send this to the junk branch, and it does exactly at p = 0 (heckeTGeneratorGamma0_zero). No consumer needs 0 < p as a hypothesis, so it is not imposed on the definition.

Equations

• HeckeRing.GL2.heckeTGeneratorGamma0 N p = HeckeRing.GL2.diagElemGamma0 N ![1, p]

noncomputable def HeckeRing.GL2.heckeTScalarGamma0 (N p : ℕ) : HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ

The scalar generator of the Γ₀(N) Hecke ring: the class of Γ₀(N)·diag(p, p)·Γ₀(N) when 0 < p and p is coprime to the level, and 0 otherwise. Both halves of the guard bite: heckeTScalarGamma0 1 0 is 0 even though 0 is coprime to the level 1.

Unlike heckeTGeneratorGamma0 the coprimality here has content, because the head entry of ![p, p] is p. For 0 < p sharing a factor with N the vanishing is a membership fact — diag(p, p) ∉ Δ₀(N) — and mirrors ⟨p⟩ = 0. At p = 0 it is instead a junk-value convention: natDiagGL 2 ![0, 0] is the identity and so does lie in Δ₀(N), but the positivity guard sends the element to 0 at every level, coprime or not.

Equations

• HeckeRing.GL2.heckeTScalarGamma0 N p = HeckeRing.GL2.diagElemGamma0 N ![p, p]

theorem HeckeRing.GL2.heckeTGeneratorGamma0_eq_single (N : ℕ) {p : ℕ} (hp : 0 < p) : heckeTGeneratorGamma0 N p = HeckeCosetModule.single ℤ (diagCosetGamma0 N ![1, p] ⋯) 1

The diagonal generator as a single. The guard has two halves: coprimality is discharged outright by Nat.coprime_one_left, since the head entry of ![1, p] is 1, and the supplied 0 < p discharges positivity — so past that hypothesis this is the class of the double coset. Named _eq_single rather than _def because it states the two-level unfolding, not the definition; heckeTGeneratorGamma0_def below is the actual defining equation.

theorem HeckeRing.GL2.heckeTGeneratorGamma0_def (N p : ℕ) : heckeTGeneratorGamma0 N p = diagElemGamma0 N ![1, p]

The defining equation of the diagonal generator: it is diagElemGamma0 at ![1, p]. Both generator bodies are sealed, so without this the diagElemGamma0_* API is unreachable for them.

theorem HeckeRing.GL2.heckeTScalarGamma0_def (N p : ℕ) : heckeTScalarGamma0 N p = diagElemGamma0 N ![p, p]

The defining equation of the scalar generator, the companion of heckeTGeneratorGamma0_def.

theorem HeckeRing.GL2.heckeTScalarGamma0_of_coprime (N : ℕ) {p : ℕ} (hp : 0 < p) (hpN : p.Coprime N) : heckeTScalarGamma0 N p = HeckeCosetModule.single ℤ (diagCosetGamma0 N ![p, p] ⋯) 1

The scalar generator in the coprime branch, where it is nonzero.

@[simp]

theorem HeckeRing.GL2.heckeTScalarGamma0_of_not_coprime (N : ℕ) {p : ℕ} (hpN : ¬p.Coprime N) : heckeTScalarGamma0 N p = 0

The scalar generator vanishes when p shares a factor with the level. This is the case that lets the recurrence below be stated without splitting on whether p divides N.

@[simp]

theorem HeckeRing.GL2.heckeTScalarGamma0_one (N : ℕ) : heckeTScalarGamma0 N 1 = 1

At p = 1 the scalar generator is the identity: diag(1, 1) is the identity matrix.

@[simp]

theorem HeckeRing.GL2.heckeTGeneratorGamma0_zero (N : ℕ) : heckeTGeneratorGamma0 N 0 = 0

At p = 0 the generator vanishes: ![1, 0] is not everywhere positive.

@[simp]

theorem HeckeRing.GL2.heckeTScalarGamma0_zero (N : ℕ) : heckeTScalarGamma0 N 0 = 0

At p = 0 the scalar generator vanishes too, for the same reason and at every level. The two generators agreeing here is what the shared positivity guard buys: before it, this one vanished only because 0 is not coprime to N > 1, and so had no unconditional normal form.

@[simp]

theorem HeckeRing.GL2.heckeTGeneratorGamma0_one (N : ℕ) : heckeTGeneratorGamma0 N 1 = 1

At p = 1 the generator is the identity for the other reason: diag(1, 1) is the identity matrix, so this is diagElemGamma0_one rather than the degeneracy case above.

noncomputable def HeckeRing.GL2.heckeTGeneratorRecGamma0 (N : ℕ) [NeZero N] (p : ℕ) : ℕ → HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ

The family generated from heckeTGeneratorGamma0 by the Diamond–Shurman recurrence T₀ = 1, T₁ = T_p and T_{r+2} = T_p · T_{r+1} − (p · S_p) · T_r.

The recurrence is chosen so that at a prime p the r-th term is the classical T_{p^r}, but it is defined for every natural p and nothing here assumes primality.

Equations

• One or more equations did not get rendered due to their size.
• HeckeRing.GL2.heckeTGeneratorRecGamma0 N p 0 = 1
• HeckeRing.GL2.heckeTGeneratorRecGamma0 N p 1 = HeckeRing.GL2.heckeTGeneratorGamma0 N p

@[simp]

theorem HeckeRing.GL2.heckeTGeneratorRecGamma0_zero (N : ℕ) [NeZero N] (p : ℕ) : heckeTGeneratorRecGamma0 N p 0 = 1

The empty product: T₀ = 1.

@[simp]

theorem HeckeRing.GL2.heckeTGeneratorRecGamma0_one (N : ℕ) [NeZero N] (p : ℕ) : heckeTGeneratorRecGamma0 N p 1 = heckeTGeneratorGamma0 N p

The first term is the generator itself: T₁ = T_p.

theorem HeckeRing.GL2.heckeTGeneratorRecGamma0_succ_succ (N : ℕ) [NeZero N] (p r : ℕ) : heckeTGeneratorRecGamma0 N p (r + 2) = heckeTGeneratorGamma0 N p * heckeTGeneratorRecGamma0 N p (r + 1) - ↑p • heckeTScalarGamma0 N p * heckeTGeneratorRecGamma0 N p r

The r + 2 case of the recurrence, as a rewriting rule. Not a simp lemma: the right-hand side mentions heckeTGeneratorRecGamma0 at two smaller arguments, so it is a recursion to unfold deliberately rather than a normal form to rewrite towards.

@[simp]

theorem HeckeRing.GL2.heckeTGeneratorRecGamma0_eq_generator_pow_of_not_coprime (N : ℕ) [NeZero N] {p : ℕ} (hpN : ¬p.Coprime N) (r : ℕ) : heckeTGeneratorRecGamma0 N p r = heckeTGeneratorGamma0 N p ^ r

When p shares a factor with the level the scalar term vanishes and the recurrence degenerates to a power of the generator: T_r = T_p^r.

@[simp] because this is the normal form once the coprimality hypothesis is in context: it is conditional, so it fires only where ¬ Nat.Coprime p N can be discharged, and leaves the unconditional heckeTGeneratorRecGamma0_zero/_one normal forms alone elsewhere.

The product formula

heckeTGeneratorRecGamma0 is a two-term linear recurrence with D = T_p and S = p · S_p, so a product of two of its terms is an instance of TauCeti.linearRec₂_mul_eq_sum_pow_mul. That is the route heckeT_prime_pow_mul already takes at level one (GL2/Recurrence.lean); the only input beyond the recurrence is that D and S commute.

theorem HeckeRing.GL2.heckeTGeneratorRecGamma0_mul (N : ℕ) [NeZero N] (p : ℕ) {r s : ℕ} (hrs : r ≤ s) : heckeTGeneratorRecGamma0 N p r * heckeTGeneratorRecGamma0 N p s = ∑ i ∈ Finset.range (r + 1), ↑p ^ i • (heckeTScalarGamma0 N p ^ i * heckeTGeneratorRecGamma0 N p (r + s - 2 * i))

Shimura, Theorem 3.24(3) at level Γ₀(N) — the per-prime product formula: T_{p^r} · T_{p^s} = ∑_{i ≤ r} pⁱ · S_pⁱ · T_{p^{r+s−2i}} for r ≤ s, so that no product of two T-values survives on the right.

No primality is asked of p, for the same reason the recurrence does not ask it. When p shares a factor with the level S_p = 0, every summand but i = 0 drops and the identity degenerates to T_p^r · T_p^s = T_p^{r+s}.