Documentation

TauCeti.NumberTheory.HeckeRing.GL2.Basic

The GL₂ Hecke operators T(a, d) and T(m) #

The specialization of the GL_n Hecke ring to n = 2: the basis operators T(a, d) for divisor pairs a ∣ d, the scalar operators T(c, c), and Shimura's summed operator T(m) = ∑_{a ∣ m} T(a, m / a).

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Basic.lean, Chris Birkbeck).

Main definitions #

Main results #

References #

source
noncomputable def HeckeRing.GL2.heckeTDiag (a d : ℕ) :
GLn.IntegralHeckeRing 2

T(a, d): the diagonal Hecke basis element of the pair (a, d), zero unless 0 < a, 0 < d and a ∣ d.

Equations
Instances For
    source
    theorem HeckeRing.GL2.heckeTDiag_def (a d : ℕ) :
    heckeTDiag a d = if 0 < a ∧ 0 < d ∧ a ∣ d then GLn.diagElem ![a, d] else 0

    Defining equation for the sealed heckeTDiag.

    source
    theorem HeckeRing.GL2.heckeTDiag_eq_diagElem {a d : ℕ} (ha : 0 < a) (hd : 0 < d) (h : a ∣ d) :
    heckeTDiag a d = GLn.diagElem ![a, d]

    T(a, d) is the diagonal Hecke element when the divisor-pair conditions hold.

    All three hypotheses are needed. 0 < d does not follow from 0 < a and a ∣ d: in ℕ every number divides 0, so a = 1, d = 0 satisfies both while 0 < d fails — and that is exactly the tuple on which natDiagGL takes its junk value, which the 0 < d branch of heckeTDiag exists to exclude.

    source
    @[simp]
    theorem HeckeRing.GL2.heckeTDiag_eq_zero {a d : ℕ} (h : ¬(0 < a ∧ 0 < d ∧ a ∣ d)) :
    heckeTDiag a d = 0

    T(a, d) is zero when the divisor-pair conditions fail.

    source
    noncomputable def HeckeRing.GL2.heckeTScalar (c : ℕ) :
    GLn.IntegralHeckeRing 2

    T(c, c): the scalar Hecke operator.

    Equations
    Instances For
      source
      theorem HeckeRing.GL2.heckeTScalar_def (c : ℕ) :
      heckeTScalar c = heckeTDiag c c

      The defining equation of heckeTScalar.

      source
      @[simp]
      theorem HeckeRing.GL2.heckeTScalar_zero :
      heckeTScalar 0 = 0

      T(0, 0) = 0: the scalar operator of 0 is zero, since the divisor-pair conditions fail.

      Together with heckeTScalar_of_pos this covers the whole ℕ-valued interface, so consumers never need to unfold through heckeTScalar_def.

      source
      theorem HeckeRing.GL2.heckeTScalar_of_pos {c : ℕ} (hc : 0 < c) :
      heckeTScalar c = GLn.diagElem fun (x : Fin 2) => c

      The scalar operator of a positive c is the constant diagonal element.

      source
      @[simp]
      theorem HeckeRing.GL2.heckeTDiag_one_one :
      heckeTDiag 1 1 = 1

      T(1, 1) is the identity.

      source
      @[simp]
      theorem HeckeRing.GL2.heckeTScalar_one :
      heckeTScalar 1 = 1

      T(1, 1) = 1 in scalar form: the scalar operator of 1 is the identity. Together with heckeTScalar_zero and heckeTScalar_of_pos this closes the ℕ-valued interface at its canonical input.

      source
      noncomputable def HeckeRing.GL2.heckeT (m : ℕ+) :
      GLn.IntegralHeckeRing 2

      Shimura's summed Hecke operator: T(m) = ∑_{a ∣ m} T(a, m / a).

      Equations
      Instances For
        source
        theorem HeckeRing.GL2.heckeT_def (m : ℕ+) :
        heckeT m = ∑ a ∈ (↑m).divisors, heckeTDiag a (↑m / a)

        The defining equation of heckeT.

        source
        @[simp]
        theorem HeckeRing.GL2.heckeT_one :
        heckeT 1 = 1

        T(1) = 1: the only divisor pair of 1 is (1,1).

        source
        @[simp]
        theorem HeckeRing.GL2.heckeT_prime (p : ℕ) (hp : Nat.Prime p) :
        heckeT ⟨p, ⋯⟩ = heckeTDiag 1 p

        For a prime p, the summed operator collapses: T(p) = T(1, p).

        source
        theorem HeckeRing.GL2.heckeTScalar_pow (p : ℕ) (hp : 0 < p) (i : ℕ) :
        heckeTScalar p ^ i = GLn.diagElem fun (x : Fin 2) => p ^ i

        Powers of the scalar operator: T(p,p) ^ i = T(pⁱ,...,pⁱ).

        source
        theorem HeckeRing.GL2.heckeT_prime_pow_expansion (p : ℕ) (hp : Nat.Prime p) (k : ℕ) :
        heckeT ⟨p ^ k, ⋯⟩ = ∑ i ∈ Finset.range (k / 2 + 1), heckeTDiag (p ^ i) (p ^ (k - i))

        Expansion of T(pᵏ): only the divisor pairs (pⁱ, p^(k-i)) with i ≤ k - i contribute.

        source
        theorem HeckeRing.GL2.heckeTDiag_mul_of_coprime (a b da db : ℕ) (hcop : (a * da).Coprime (b * db)) :
        heckeTDiag a da * heckeTDiag b db = heckeTDiag (a * b) (da * db)

        Coprime multiplicativity (Shimura, Proposition 3.16 in the GL₂ notation): T(a, da) · T(b, db) = T(ab, da·db) when the determinants a·da and b·db are coprime.

        Coprimality is the only hypothesis. No positivity or divisor-pair condition is needed, because heckeTDiag is zero-extended and coprimality propagates that zero: if T(a, da) fails to be a basis element then so does T(ab, da·db), since a is coprime to db, so a ∣ ab ∣ da·db would force a ∣ da. Both sides are then 0.

        source
        theorem HeckeRing.GL2.heckeT_mul_of_coprime (m n : ℕ+) (hcop : (↑m).Coprime ↑n) :
        heckeT m * heckeT n = heckeT (m * n)

        Shimura, Theorem 3.24(3a) — coprime multiplicativity: T(m) · T(n) = T(mn) when m and n are coprime.