2. Eigenforms and eigenvalue systems🔗

Definition2.1

Statement uses 2

Statement dependency previews

Preview

Definition 1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 7

Reverse dependency previews

Preview

Theorem 2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

An eigenform of level \Gamma_1(N) and weight k is a cusp form f carrying a Nebentypus character \chi (so f \in S_k(N, \chi), Definition 1.2) that is a simultaneous eigenvector of all Hecke operators T_n with \gcd(n, N) = 1 (Definition 1.4). Its eigenvalue \lambda_n is recorded by T_n f = \lambda_n f. In LeanModularForms this is the structure \texttt{Eigenform} with \texttt{Eigenform.eigenvalue}. Following Miyake §4.5.

Lean code for Definition2.1●2 definitions

structure(extends 2, 9 fields)defined in LeanModularForms/HeckeRIngs/GL2/Newforms/Basic.lean

complete

structure HeckeRing.GL2.Eigenform (N : ℕ) [NeZero N] (k : ℤ) : Type

structure HeckeRing.GL2.Eigenform (N : ℕ) [NeZero N]
  (k : ℤ) : Type

An **eigenform** of level Γ₁(N) and weight k: a cusp form `f` carrying a Nebentypus
character `χ` (so `↑f ∈ modFormCharSpace k χ`) that is a simultaneous eigenvector of the
canonical `Γ₀(N)` Hecke **ring** action `heckeRingHomCharSpace`.  The classical eigenvalue
`T_n f = (eigenvalue n) • f` is a *derived* fact (`Eigenform.eigenvalue`, `Eigenform.isEigen`),
differing from the ring eigenvalue by the diamond normalisation `χ(n)`.
DS Definition 5.5.4 / Miyake §4.5.

Extends

CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k

Fields

toFun : UpperHalfPlane → ℂ

Inherited from

CuspForm
SlashInvariantForm

slash_action_eq' : ∀ γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N),
  SlashAction.map k γ self.toFun = self.toFun

Inherited from

CuspForm
SlashInvariantForm

holo' : MDiff ⇑self.toSlashInvariantForm

Inherited from

CuspForm

zero_at_cusps' : ∀ {c : OnePoint ℝ},
  IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) → c.IsZeroAt self.toFun k

Inherited from

CuspForm

χ : (ZMod N)ˣ →* ℂˣ

The Nebentypus character of the eigenform.

mem_charSpace : self.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k self.χ

The coercion of the cusp form lies in the `χ`-eigenspace `modFormCharSpace k χ`.

ringEigenvalue : ℕ+ → ℂ

The eigenvalues for the canonical `Γ₀(N)` Hecke **ring** action.

isRingEigen : ∀ (n : ℕ+),
  (↑n).Coprime N →
    (HeckeRing.GL2.Unified.heckeRingHomCharSpace (HeckeRing.GL2.Unified.heckeRingDn ↑n)) ⟨self.toModularForm', ⋯⟩ =
      self.ringEigenvalue n • ⟨self.toModularForm', ⋯⟩

For `n` coprime to `N`, the explicit ring element `heckeRingDn n` acts on the
coercion `↑f ∈ modFormCharSpace k χ` by the scalar `ringEigenvalue n`.

ringEigen_bad : ∀ (n : ℕ+), ¬(↑n).Coprime N → self.ringEigenvalue n = 0

At indices **not** coprime to `N` the ring action `heckeRingDn` is not packaged here
(the bad-prime element lies in a disjoint double-coset class), so the ring eigenvalue is
pinned to the canonical constant `0`.  This removes a latent over-specification: without it,
the bad-prime values of `ringEigenvalue` would be free, giving infinitely many `Eigenform`
terms over a single underlying `toCuspForm`.  With it, an `Eigenform` is determined by its
underlying form together with `χ` (see `Eigenform.ext_of_toCuspForm`).

defdefined in LeanModularForms/HeckeRIngs/GL2/Newforms/Basic.lean

complete

def HeckeRing.GL2.Eigenform.eigenvalue {N : ℕ} [NeZero N] {k : ℤ}
  (f : HeckeRing.GL2.Eigenform N k) (n : ℕ+) : ℂ

def HeckeRing.GL2.Eigenform.eigenvalue {N : ℕ}
  [NeZero N] {k : ℤ}
  (f : HeckeRing.GL2.Eigenform N k)
  (n : ℕ+) : ℂ

The classical Hecke eigenvalue of an eigenform: the ring eigenvalue rescaled by the
diamond factor `χ(n)`, so that `T_n f = (eigenvalue n) • f` (`Eigenform.isEigen`).  For
`n` not coprime to `N` the value is `0` (the classical `T_n` is not packaged here).

Theorem2.2

Statement uses 2

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Any cusp form in the new subspace lying in a Nebentypus space S_k(N, \chi) is a finite sum of common Hecke eigenforms, each again new and of Nebentypus \chi (Definition 2.1, Definition 4.3). This is the simultaneous diagonalisation underlying the whole theory.

Lean code for Theorem2.2●1 theorem

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew {N : ℕ}
  [NeZero N] {k : ℤ} (χ : (ZMod N)ˣ →* ℂˣ)
  (g :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)
  (hg_new : g ∈ HeckeRing.GL2.cuspFormsNew N k)
  (hgχ : g.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) :
  ∃ ι x h,
    (∀ (i : ι), h i ∈ HeckeRing.GL2.cuspFormsNew N k) ∧
      (∀ (i : ι), h i ∈ HeckeRing.GL2.cuspFormCharSpace k χ) ∧
        (∀ (i : ι), HeckeRing.GL2.IsEigenform (h i)) ∧ g = ∑ i, h i

theorem HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew
  {N : ℕ} [NeZero N] {k : ℤ}
  (χ : (ZMod N)ˣ →* ℂˣ)
  (g :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)
  (hg_new :
    g ∈ HeckeRing.GL2.cuspFormsNew N k)
  (hgχ :
    g.toModularForm' ∈
      HeckeRing.GL2.modFormCharSpace k
        χ) :
  ∃ ι x h,
    (∀ (i : ι),
        h i ∈
          HeckeRing.GL2.cuspFormsNew N
            k) ∧
      (∀ (i : ι),
          h i ∈
            HeckeRing.GL2.cuspFormCharSpace
              k χ) ∧
        (∀ (i : ι),
            HeckeRing.GL2.IsEigenform
              (h i)) ∧
          g = ∑ i, h i

**New eigenbasis decomposition.**  A new cusp form `g ∈ S_k^♯(N)` whose underlying
modular form lies in the Nebentypus space `M_k(Γ₁(N),χ)` is a finite sum of common Hecke
eigenforms, each of which is again **new** (lies in `S_k^♯(N)`).

Proof: the new subspace is `T_n`-invariant (`heckeT_n_preserves_cuspFormsNew`), so the
simultaneous Hecke diagonalisation of `S_k(Γ₁(N),χ)`
(`exists_eigenform_decomposition_of_invariant`) restricts to it, yielding eigenform
summands that remain new.

Proof for Theorem 2.2

Proof uses 2

Proof dependency previews

Preview

Theorem 1.5

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

The new subspace and the Nebentypus space are stable under every T_n (Theorem 1.6). The \{T_n\}_{\gcd(n,N)=1} form a commuting family of diagonalisable operators on the finite-dimensional space S_k(N, \chi) (Theorem 1.5), so the joint spectral decomposition restricts to the invariant new subspace, exhibiting the form in a joint eigenbasis.

Theorem2.3

uses 1used by 1✓L∃∀N

For a normalised eigenform the eigenvalue system is multiplicative: the Fourier coefficients satisfy a_m a_n = \sum_{d \mid (m,n)} d^{k-1}\,\chi(d)\, a_{mn/d^2}, so a_{mn} = a_m a_n whenever \gcd(m, n) = 1 (Definition 2.1). Following Miyake Theorem 4.5.4(3).

Lean code for Theorem2.3●1 theorem

theoremdefined in LeanModularForms/HeckeRIngs/GL2/FourierHecke.lean

complete

theorem HeckeRing.GL2.eigenform_coeff_multiplicative_one {N : ℕ} [NeZero N]
  (k : ℤ) (m n : ℕ+) (hm : (↑m).Coprime N) :
  (↑n).Coprime N →
    ∀ (χ : (ZMod N)ˣ →* ℂˣ)
      {f :
        ModularForm
          (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
            (CongruenceSubgroup.Gamma1 N))
          k}
      (hf_char : f ∈ HeckeRing.GL2.modFormCharSpace k χ)
      (hf_eigen : HeckeRing.GL2.IsNormalisedEigenform_one k f),
      (PowerSeries.coeff ↑m) (UpperHalfPlane.qExpansion 1 ⇑f) *
          (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑f) =
        ∑ d ∈ ((↑m).gcd ↑n).divisors,
          if h : d.Coprime N then
            ↑d ^ (k - 1) * ↑(χ (ZMod.unitOfCoprime d h)) *
              (PowerSeries.coeff (↑m * ↑n / (d * d)))
                (UpperHalfPlane.qExpansion 1 ⇑f)
          else 0

theorem HeckeRing.GL2.eigenform_coeff_multiplicative_one
  {N : ℕ} [NeZero N] (k : ℤ) (m n : ℕ+)
  (hm : (↑m).Coprime N) :
  (↑n).Coprime N →
    ∀ (χ : (ZMod N)ˣ →* ℂˣ)
      {f :
        ModularForm
          (Subgroup.map
            (Matrix.SpecialLinearGroup.mapGL
              ℝ)
            (CongruenceSubgroup.Gamma1 N))
          k}
      (hf_char :
        f ∈
          HeckeRing.GL2.modFormCharSpace k
            χ)
      (hf_eigen :
        HeckeRing.GL2.IsNormalisedEigenform_one
          k f),
      (PowerSeries.coeff ↑m)
            (UpperHalfPlane.qExpansion 1
              ⇑f) *
          (PowerSeries.coeff ↑n)
            (UpperHalfPlane.qExpansion 1
              ⇑f) =
        ∑ d ∈ ((↑m).gcd ↑n).divisors,
          if h : d.Coprime N then
            ↑d ^ (k - 1) *
                ↑(χ
                    (ZMod.unitOfCoprime d
                      h)) *
              (PowerSeries.coeff
                  (↑m * ↑n / (d * d)))
                (UpperHalfPlane.qExpansion
                  1 ⇑f)
          else 0

**Period-1 Hecke multiplicativity relations** for Fourier coefficients of a normalised
eigenform: `a_m · a_n = Σ_{d | gcd(m, n)} d^{k-1} · χ(d) · a_{mn/d²}`. In particular
`a_m · a_n = a_{mn}` when `gcd(m, n) = 1`. Period-1 analog of
`eigenform_coeff_multiplicative`.

Proof for Theorem 2.3

Proof uses 2

Proof dependency previews

Preview

Theorem 1.5

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Apply the divisor-sum Fourier formula for T_m T_n (Theorem 3.1) to a normalised eigenform and read off the first coefficient; the multiplicativity of the T_n (Theorem 1.5) turns the operator identity into the stated relation on coefficients.