Strong Multiplicity One — Lean blueprint

5. Multiplicity one (the Main Lemma)🔗

Theorem5.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 3
Reverse dependency previews
Preview
Theorem 3.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

(Main Lemma — Miyake Theorem 4.6.8.) A cusp form in S_k(N, \chi) whose Fourier coefficients a_n vanish for all n coprime to N lies in the old subspace S_k^{\flat}(N) (Definition 1.2, Definition 4.3). This is the engine of the whole theory: it converts "almost all coefficients vanish" into a structural conclusion.

Lean code for Theorem5.1●1 theorem
  • theoremdefined in LeanModularForms/SMOObligations.lean
    complete
    theorem HeckeRing.GL2.mainLemma_charSpace_routeB {N : ℕ} [NeZero N] {k : ℤ}
  (χ : (ZMod N)ˣ →* ℂˣ)
  (f :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)
  (hfχ : f ∈ HeckeRing.GL2.cuspFormCharSpace k χ)
  (h_vanish :
    ∀ (n : ℕ),
      n.Coprime N →
        (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f) = 0) :
  f ∈ HeckeRing.GL2.cuspFormsOld N k
    theorem HeckeRing.GL2.mainLemma_charSpace_routeB
  {N : ℕ} [NeZero N] {k : ℤ}
  (χ : (ZMod N)ˣ →* ℂˣ)
  (f :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)
  (hfχ :
    f ∈
      HeckeRing.GL2.cuspFormCharSpace k χ)
  (h_vanish :
    ∀ (n : ℕ),
      n.Coprime N →
        (PowerSeries.coeff n)
            (UpperHalfPlane.qExpansion 1
              ⇑f) =
          0) :
  f ∈ HeckeRing.GL2.cuspFormsOld N k
    **Per-character unconditional Miyake 4.6.8 (route B).**  A cusp form
`f ∈ S_k(Γ_1(N), χ)` whose period-1 `q`-expansion vanishes at every index coprime to
`N` is an oldform.  This is `mainLemma_charSpace_routeB` with the `h_chi_factor`
hypothesis **removed**: the per-prime character factorisation needed by the
same-level divisor decomposition is supplied internally by Miyake's dichotomy 4.6.4
(`coprimeSieve_admits_squarefree_decomposition_in_charSpace`).
Proof for Theorem 5.1
uses 0

This is the per-character form of Miyake Theorem 4.6.8. Vanishing of all coprime coefficients lets one run the squarefree descent (peel off one prime at a time via the V_p/U_p degeneracy maps and the conductor dichotomy 4.6.4), expressing the form as a same-level sum of degeneracy images of lower-level forms — i.e. an oldform.

Definition5.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 5
Reverse dependency previews
Preview
Theorem 5.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A newform of level \Gamma_1(N) and weight k is an eigenform lying in the new subspace and normalised so that its first Fourier coefficient is a_1 = 1 (Definition 2.1, Definition 4.3). In LeanModularForms this is the structure \texttt{Newform}, extending \texttt{Eigenform} with the new-membership and normalisation fields. Following Miyake §4.6.

Lean code for Definition5.2●1 definition
  • structure(extends 3, 11 fields)defined in LeanModularForms/HeckeRIngs/GL2/Newforms/MainLemma.lean
    complete
    structure HeckeRing.GL2.Newform (N : ℕ) [NeZero N] (k : ℤ) : Type
    structure HeckeRing.GL2.Newform (N : ℕ) [NeZero N]
  (k : ℤ) : Type
    A **newform** of level Γ₁(N) and weight k: a cusp form that is
1. an eigenform (common eigenfunction of all T_n with (n,N)=1)
2. in the new subspace
3. normalised: a_1(f) = 1

By Atkin-Lehner uniqueness (DS Theorem 5.8.2), newforms are uniquely determined
by their Hecke eigenvalues away from the level.

    Extends

    • HeckeRing.GL2.Eigenform N k

    Fields

    toFun : UpperHalfPlane → ℂ
    Inherited from
    1. HeckeRing.GL2.Eigenform
    2. CuspForm
    3. SlashInvariantForm
    slash_action_eq' : ∀ γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N),
  SlashAction.map k γ self.toFun = self.toFun
    Inherited from
    1. HeckeRing.GL2.Eigenform
    2. CuspForm
    3. SlashInvariantForm
    holo' : MDiff ⇑self.toSlashInvariantForm
    Inherited from
    1. HeckeRing.GL2.Eigenform
    2. CuspForm
    zero_at_cusps' : ∀ {c : OnePoint ℝ},
  IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) → c.IsZeroAt self.toFun k
    Inherited from
    1. HeckeRing.GL2.Eigenform
    2. CuspForm
    χ : (ZMod N)ˣ →* ℂˣ
    Inherited from
    1. HeckeRing.GL2.Eigenform
    mem_charSpace : self.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k self.χ
    Inherited from
    1. HeckeRing.GL2.Eigenform
    ringEigenvalue : ℕ+ → ℂ
    Inherited from
    1. HeckeRing.GL2.Eigenform
    isRingEigen : ∀ (n : ℕ+),
  (↑n).Coprime N →
    (HeckeRing.GL2.Unified.heckeRingHomCharSpace (HeckeRing.GL2.Unified.heckeRingDn ↑n)) ⟨self.toModularForm', ⋯⟩ =
      self.ringEigenvalue n • ⟨self.toModularForm', ⋯⟩
    Inherited from
    1. HeckeRing.GL2.Eigenform
    ringEigen_bad : ∀ (n : ℕ+), ¬(↑n).Coprime N → self.ringEigenvalue n = 0
    Inherited from
    1. HeckeRing.GL2.Eigenform
    isNew : self.toCuspForm ∈ HeckeRing.GL2.cuspFormsNewExtended N k
    The form is in the new subspace. 
    isNorm : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑self.toCuspForm) = 1
    Normalisation at the **canonical Fourier period** (`h = 1`): the first
Fourier coefficient is `1`, i.e. `a₁ = 1` (the Diamond–Shurman / Miyake
normalisation).
Theorem5.3
Statement uses 2
Statement dependency previews
Preview
Definition 4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

A nonzero newform at level N does not lie in the (extended) old subspace (Definition 5.2, Definition 4.3). Its eigenvalue system is genuinely of level N, occurring at no proper divisor.

Lean code for Theorem5.3●1 theorem
  • theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean
    complete
    theorem HeckeRing.GL2.newform_notMem_cuspFormsOldExtended {N : ℕ} [NeZero N]
  {k : ℤ} (f : HeckeRing.GL2.Newform N k) (hf0 : f.toCuspForm ≠ 0) :
  f.toCuspForm ∉ HeckeRing.GL2.cuspFormsOldExtended N k
    theorem HeckeRing.GL2.newform_notMem_cuspFormsOldExtended
  {N : ℕ} [NeZero N] {k : ℤ}
  (f : HeckeRing.GL2.Newform N k)
  (hf0 : f.toCuspForm ≠ 0) :
  f.toCuspForm ∉
    HeckeRing.GL2.cuspFormsOldExtended N k
    A nonzero `Newform` at level `N` does not lie in the extended old space
`cuspFormsOldExtended N k`.
Proof for Theorem 5.3
uses 1

A newform lies in the new subspace, which meets the old subspace only in 0 (Theorem 4.6); a nonzero new form therefore cannot be old.