4. Degeneracy maps and the old/new decomposition🔗

Definition4.1

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 4.2

Loading preview

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

✓L∃∀N

For a divisor M \mid N and \ell with \ell M = N, the degeneracy / level-raising map V_\ell : f \mapsto f(\ell z) carries S_k(\Gamma_1(M)) into S_k(\Gamma_1(N)) (\texttt{levelRaise}); the case \ell = 1 is the inclusion \texttt{levelInclude\_cusp}. Iterated level-raises compose, V_{d} \circ V_{e} = V_{de}. Following Miyake §4.6 (Lemma 4.6.2).

Lean code for Definition4.1●2 definitions

defdefined in LeanModularForms/HeckeRIngs/GL2/LevelRaise.lean

complete

def HeckeRing.GL2.levelRaise (M : ℕ) [NeZero M] (d : ℕ) [NeZero d] (k : ℤ) :
  CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 M))
      k →ₗ[ℂ]
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 (d * M)))
      k

def HeckeRing.GL2.levelRaise (M : ℕ)
  [NeZero M] (d : ℕ) [NeZero d] (k : ℤ) :
  CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 M))
      k →ₗ[ℂ]
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1
          (d * M)))
      k

The level-raising operator `ι_d : S_k(Γ₁(M)) → S_k(Γ₁(d*M))`, defined as
`(ι_d f)(τ) = f(d·τ)`, equivalently `d^{1-k} · (f ∣[k] [[d,0],[0,1]])`
(DS (5.16); Miyake §4.6 Lemma 4.6.1).

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

complete

def HeckeRing.GL2.levelInclude_cusp {M N : ℕ} [NeZero M] [NeZero N]
  (hMN : M ∣ N) (k : ℤ) :
  CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 M))
      k →ₗ[ℂ]
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k

def HeckeRing.GL2.levelInclude_cusp {M N : ℕ}
  [NeZero M] [NeZero N] (hMN : M ∣ N)
  (k : ℤ) :
  CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 M))
      k →ₗ[ℂ]
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k

Trivial-inclusion CuspForm map: for `M ∣ N`, a `Γ₁(M)`-cusp form is
automatically `Γ₁(N)`-invariant, so this lifts it to a `Γ₁(N)`-cusp form
with the same underlying function.

Theorem4.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 0✓L∃∀N

The level-raise of a T_n-eigenform (\gcd(n, N) = 1) is again a T_n-eigenform with the same eigenvalue (Definition 2.1, Definition 4.1): if T_n h = \lambda h at level M, then T_n(V_\ell h) = \lambda\,(V_\ell h) at level N. (Miyake Lemma 4.6.2.)

Lean code for Theorem4.2●1 theorem

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.heckeT_n_levelRaise_eigen {N : ℕ} [NeZero N] {k : ℤ}
  {M : ℕ} [NeZero M] {l : ℕ} [NeZero l] (heq : l * M = N) (n : ℕ)
  [NeZero n] (hn : n.Coprime N)
  (h :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 M))
      k)
  (lam : ℂ) (h_eig : HeckeRing.GL2.heckeT_n_cusp k n h = lam • h) :
  HeckeRing.GL2.heckeT_n_cusp k n
      (heq ▸ (HeckeRing.GL2.levelRaise M l k) h) =
    lam • heq ▸ (HeckeRing.GL2.levelRaise M l k) h

theorem HeckeRing.GL2.heckeT_n_levelRaise_eigen
  {N : ℕ} [NeZero N] {k : ℤ} {M : ℕ}
  [NeZero M] {l : ℕ} [NeZero l]
  (heq : l * M = N) (n : ℕ) [NeZero n]
  (hn : n.Coprime N)
  (h :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 M))
      k)
  (lam : ℂ)
  (h_eig :
    HeckeRing.GL2.heckeT_n_cusp k n h =
      lam • h) :
  HeckeRing.GL2.heckeT_n_cusp k n
      (heq ▸
        (HeckeRing.GL2.levelRaise M l k)
          h) =
    lam •
      heq ▸
        (HeckeRing.GL2.levelRaise M l k) h

**Miyake Lemma 4.6.2** (eigenvalue-preservation form).  If `h` is a `T_n`-eigenform
at level `M` with eigenvalue `λ` for some `(n, l*M) = 1`, then its level-raise
`V_l h = h(l·)` is a `T_n`-eigenform at level `l*M` with the same eigenvalue.

Proof for Theorem 4.2

uses 0

The Hecke operators at the good primes commute with the degeneracy maps, so T_n(V_\ell h) = V_\ell(T_n h) = V_\ell(\lambda h) = \lambda\,(V_\ell h).

Definition4.3

Statement uses 2

Statement dependency previews

Preview

Definition 4.1

Loading preview

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

Used by 9

Reverse dependency previews

Preview

Theorem 2.2

Loading preview

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

✓L∃∀N

The old subspace S_k^{\flat}(N) (\texttt{cuspFormsOld}) is the span of all degeneracy images V_\ell f of cusp forms at proper divisor levels M \mid N, M \ne N, \ell > 1 (Definition 4.1); the new subspace S_k^{\sharp}(N) (\texttt{cuspFormsNew}) is its Petersson-orthogonal complement (Definition 4.4). Following Miyake §4.6.

Lean code for Definition4.3●2 definitions

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

complete

def HeckeRing.GL2.cuspFormsOld (N : ℕ) [NeZero N] (k : ℤ) :
  Submodule ℂ
    (CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)

def HeckeRing.GL2.cuspFormsOld (N : ℕ)
  [NeZero N] (k : ℤ) :
  Submodule ℂ
    (CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)

The **oldform subspace** `S_k(Γ₁(N))^old`: the submodule generated by all
`levelRaise` images from proper divisors of N.

DS (5.18): `S_k^old = ⊕_{M | N, M ≠ N} ι_{N/M}(S_k(Γ₁(M))^2)` (sum over divisors).

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

complete

def HeckeRing.GL2.cuspFormsNew (N : ℕ) [NeZero N] (k : ℤ) :
  Submodule ℂ
    (CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)

def HeckeRing.GL2.cuspFormsNew (N : ℕ)
  [NeZero N] (k : ℤ) :
  Submodule ℂ
    (CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)

The **new subspace** `S_k(Γ₁(N))^new`: orthogonal complement of oldforms.

DS (5.19): `S_k^new = (S_k^old)⊥`.

Definition4.4

uses 1

Used by 3

Reverse dependency previews

Preview

Definition 4.3

Loading preview

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

✓L∃∀N

The Petersson inner product \langle f, g \rangle is the \Gamma-invariant integral pairing on cusp forms; it is positive definite (\langle f, f \rangle = 0 \Rightarrow f = 0). Two common eigenfunctions in the same Nebentypus space with different T_n-eigenvalues at some \gcd(n, N) = 1 are Petersson-orthogonal, hence linearly independent (Definition 2.1). Following Miyake §4.5.

Lean code for Definition4.4●2 theorems

theoremdefined in LeanModularForms/HeckeRIngs/GL2/AdjointTheoryPetersson.lean

complete

theorem HeckeRing.GL2.petN_self_re_nonneg {k : ℤ} {N : ℕ} [NeZero N]
  (f :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  0 ≤ (petN f f).re

theorem HeckeRing.GL2.petN_self_re_nonneg {k : ℤ}
  {N : ℕ} [NeZero N]
  (f :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  0 ≤ (petN f f).re

`petN f f` has non-negative real part.

theoremdefined in LeanModularForms/HeckeRIngs/GL2/AdjointTheoryPetersson.lean

complete

theorem HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues {k : ℤ} {N : ℕ}
  [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ)
  {f g :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k}
  (hf_char : f ∈ HeckeRing.GL2.cuspFormCharSpace k χ)
  (hg_char : g ∈ HeckeRing.GL2.cuspFormCharSpace k χ) (hf_ne : f ≠ 0)
  (_hg_ne : g ≠ 0) {n : ℕ} [NeZero n] (hn : n.Coprime N) {a b : ℂ}
  (hf_eig : HeckeRing.GL2.heckeT_n_cusp k n f = a • f)
  (hg_eig : HeckeRing.GL2.heckeT_n_cusp k n g = b • g)
  (h_diff_ab : a ≠ b) : petN f g = 0

theorem HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues
  {k : ℤ} {N : ℕ} [NeZero N]
  (χ : (ZMod N)ˣ →* ℂˣ)
  {f g :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k}
  (hf_char :
    f ∈
      HeckeRing.GL2.cuspFormCharSpace k χ)
  (hg_char :
    g ∈
      HeckeRing.GL2.cuspFormCharSpace k χ)
  (hf_ne : f ≠ 0) (_hg_ne : g ≠ 0) {n : ℕ}
  [NeZero n] (hn : n.Coprime N) {a b : ℂ}
  (hf_eig :
    HeckeRing.GL2.heckeT_n_cusp k n f =
      a • f)
  (hg_eig :
    HeckeRing.GL2.heckeT_n_cusp k n g =
      b • g)
  (h_diff_ab : a ≠ b) : petN f g = 0

Definition4.5

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4.7

Loading preview

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

✓L∃∀N

Since S_k(\Gamma_1(N)) = S_k^{\flat}(N) \oplus S_k^{\sharp}(N) is an orthogonal direct sum (Definition 4.3), every cusp form f decomposes uniquely as f = \operatorname{old}(f) + \operatorname{new}(f). The old part \texttt{oldPart} and new part \texttt{newPart} are the projections onto the two summands.

Lean code for Definition4.5●2 definitions

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

complete

def HeckeRing.GL2.oldPart {N : ℕ} [NeZero N] {k : ℤ}
  (f :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  CuspForm
    (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma1 N))
    k

def HeckeRing.GL2.oldPart {N : ℕ} [NeZero N]
  {k : ℤ}
  (f :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  CuspForm
    (Subgroup.map
      (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma1 N))
    k

**Oldform part.**  The image of `f` under the oldform projection.
Equivalent to `cuspFormsOldProjection N k f`.

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

complete

def HeckeRing.GL2.newPart {N : ℕ} [NeZero N] {k : ℤ}
  (f :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  CuspForm
    (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma1 N))
    k

def HeckeRing.GL2.newPart {N : ℕ} [NeZero N]
  {k : ℤ}
  (f :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  CuspForm
    (Subgroup.map
      (Matrix.SpecialLinearGroup.mapGL ℝ)
      (CongruenceSubgroup.Gamma1 N))
    k

**Newform part.**

Theorem4.6

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 2

Reverse dependency previews

Preview

Theorem 3.3

Loading preview

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

✓L∃∀N

The old and new subspaces are complementary: they are disjoint and together span S_k(\Gamma_1(N)) (Definition 4.3, Definition 4.4).

Lean code for Theorem4.6●2 theorems

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

complete

theorem HeckeRing.GL2.cuspFormsOld_disjoint_cuspFormsNew {N : ℕ} [NeZero N]
  {k : ℤ} :
  Disjoint (HeckeRing.GL2.cuspFormsOld N k)
    (HeckeRing.GL2.cuspFormsNew N k)

theorem HeckeRing.GL2.cuspFormsOld_disjoint_cuspFormsNew
  {N : ℕ} [NeZero N] {k : ℤ} :
  Disjoint
    (HeckeRing.GL2.cuspFormsOld N k)
    (HeckeRing.GL2.cuspFormsNew N k)

The intersection of `cuspFormsOld` and `cuspFormsNew` is trivial: applying orthogonality
of `f ∈ cuspFormsNew` to `g = f ∈ cuspFormsOld` gives `petN f f = 0`, so `f = 0` by
`petN_definite`.

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

complete

theorem HeckeRing.GL2.cuspFormsOld_isCompl_cuspFormsNew {N : ℕ} [NeZero N]
  {k : ℤ} :
  IsCompl (HeckeRing.GL2.cuspFormsOld N k)
    (HeckeRing.GL2.cuspFormsNew N k)

theorem HeckeRing.GL2.cuspFormsOld_isCompl_cuspFormsNew
  {N : ℕ} [NeZero N] {k : ℤ} :
  IsCompl (HeckeRing.GL2.cuspFormsOld N k)
    (HeckeRing.GL2.cuspFormsNew N k)

DS (5.20): `S_k(Γ₁(N)) = S_k^old ⊕ S_k^new` as inner product spaces.  `Disjoint` is
`cuspFormsOld_disjoint_cuspFormsNew`; `Codisjoint` comes from applying Mathlib's
`BilinForm.isCompl_orthogonal_iff_disjoint` to the reflexive form `petN_realBilin` over the
finite-dimensional ℝ-space, using `cuspFormsNew = (cuspFormsOld)^⊥`.

Proof for Theorem 4.6

uses 0

Disjointness is immediate from positive definiteness of the Petersson form: a form in both is orthogonal to itself, hence zero. Complementarity follows by applying the orthogonal-complement theory of the non-degenerate Petersson form on the finite-dimensional cusp space, giving S_k^{\sharp}(N) = (S_k^{\flat}(N))^{\perp} as a genuine complement.

Theorem4.7

Statement uses 2

Statement dependency previews

Preview

Theorem 1.6

Loading preview

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

used by 1✓L∃∀N

The old projection commutes with every T_n (\gcd(n,N)=1) and with the diamond operators (Definition 4.5, Theorem 1.6); consequently the old part of an eigenform is again an eigenform with the same eigenvalues. (Miyake 4.6.10.)

Lean code for Theorem4.7●2 theorems

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.oldPart_heckeT_n_cusp_comm {N : ℕ} [NeZero N] {k : ℤ}
  (n : ℕ) [NeZero n] (hn : n.Coprime N)
  (x :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  HeckeRing.GL2.oldPart (HeckeRing.GL2.heckeT_n_cusp k n x) =
    HeckeRing.GL2.heckeT_n_cusp k n (HeckeRing.GL2.oldPart x)

theorem HeckeRing.GL2.oldPart_heckeT_n_cusp_comm
  {N : ℕ} [NeZero N] {k : ℤ} (n : ℕ)
  [NeZero n] (hn : n.Coprime N)
  (x :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k) :
  HeckeRing.GL2.oldPart
      (HeckeRing.GL2.heckeT_n_cusp k n
        x) =
    HeckeRing.GL2.heckeT_n_cusp k n
      (HeckeRing.GL2.oldPart x)

The old projection commutes with `T(n)` for `(n,N)=1` (Miyake 4.6.10).

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.oldPart_isEigen_of_eigenform {N : ℕ} [NeZero N] {k : ℤ}
  (g : HeckeRing.GL2.Eigenform N k) (n : ℕ+) (hn : (↑n).Coprime N) :
  HeckeRing.GL2.heckeT_n_cusp k (↑n)
      (HeckeRing.GL2.oldPart g.toCuspForm) =
    g.eigenvalue n • HeckeRing.GL2.oldPart g.toCuspForm

theorem HeckeRing.GL2.oldPart_isEigen_of_eigenform
  {N : ℕ} [NeZero N] {k : ℤ}
  (g : HeckeRing.GL2.Eigenform N k)
  (n : ℕ+) (hn : (↑n).Coprime N) :
  HeckeRing.GL2.heckeT_n_cusp k (↑n)
      (HeckeRing.GL2.oldPart
        g.toCuspForm) =
    g.eigenvalue n •
      HeckeRing.GL2.oldPart g.toCuspForm

The old projection of an `Eigenform` `g` is a `T(n)`-eigenform with `g`'s eigenvalues for
`(n,N)=1` (Miyake 4.6.10).

Proof for Theorem 4.7

uses 0

Both subspaces are T_n- and \langle d \rangle-stable, so the projection along the decomposition commutes with each operator. Applying this to an eigenform and using T_n(\operatorname{old} g) = \operatorname{old}(T_n g) = \operatorname{old}(\lambda_n g) = \lambda_n \operatorname{old} g gives the eigen-claim.

Theorem4.8

Statement uses 3

Statement dependency previews

Preview

Theorem 2.2

Loading preview

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

used by 1✓L∃∀N

Every element of the (\chi-refined) old space is a finite sum of level-raises V_\ell h of new eigenforms h at proper divisor levels M, each carrying its own level-M Nebentypus character (Definition 4.3, Definition 4.1, Theorem 2.2). This is the descent normal form. (Miyake Lemma 4.6.9(3).)

Lean code for Theorem4.8●1 theorem

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
  {N : ℕ} [NeZero N] {k : ℤ} (χ : (ZMod N)ˣ →* ℂˣ) (m_χ : ℕ)
  (f :
    CuspForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)
  (hf : f ∈ HeckeRing.GL2.cuspFormsOldChar N k χ m_χ) :
  ∃ ι x M l,
    ∃ (x_1 : ∀ (i : ι), NeZero (M i)) (x_2 : ∀ (i : ι), NeZero (l i)) (_
      : ∀ (i : ι), m_χ ∣ M i) (_ : ∀ (i : ι), M i ≠ N) (heq :
      ∀ (i : ι), l i * M i = N),
      ∃ h χM,
        (∀ (i : ι), h i ∈ HeckeRing.GL2.cuspFormsNew (M i) k) ∧
          (∀ (i : ι), HeckeRing.GL2.IsEigenform (h i)) ∧
            (∀ (i : ι),
                h i ∈ HeckeRing.GL2.cuspFormCharSpace k (χM i)) ∧
              f =
                ∑ i, ⋯ ▸ (HeckeRing.GL2.levelRaise (M i) (l i) k) (h i)

theorem HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
  {N : ℕ} [NeZero N] {k : ℤ}
  (χ : (ZMod N)ˣ →* ℂˣ) (m_χ : ℕ)
  (f :
    CuspForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k)
  (hf :
    f ∈
      HeckeRing.GL2.cuspFormsOldChar N k χ
        m_χ) :
  ∃ ι x M l,
    ∃ (x_1 : ∀ (i : ι), NeZero (M i)) (x_2
      : ∀ (i : ι), NeZero (l i)) (_ :
      ∀ (i : ι), m_χ ∣ M i) (_ :
      ∀ (i : ι), M i ≠ N) (heq :
      ∀ (i : ι), l i * M i = N),
      ∃ h χM,
        (∀ (i : ι),
            h i ∈
              HeckeRing.GL2.cuspFormsNew
                (M i) k) ∧
          (∀ (i : ι),
              HeckeRing.GL2.IsEigenform
                (h i)) ∧
            (∀ (i : ι),
                h i ∈
                  HeckeRing.GL2.cuspFormCharSpace
                    k (χM i)) ∧
              f =
                ∑ i,
                  ⋯ ▸
                    (HeckeRing.GL2.levelRaise
                        (M i) (l i) k)
                      (h i)

**Miyake Lemma 4.6.9(3) (generation)**: every element of the χ-refined old space is a
finite sum of `V_l`-images of **eigenforms** in new spaces at proper divisor levels that
are multiples of `m_χ`.  This is the descent normal form used in step (i) of 4.6.12.

Each summand `hᵢ` additionally carries its level-`Mᵢ` Nebentypus character `χM i`
(`hᵢ ∈ cuspFormCharSpace k (χM i)`); this character-tracking is consumed by
4.6.12 step (i) (the `χ`-isotypic collapse of the orthogonality argument, via the level-`N`
pullback `(χM i)∘unitsMap`).

Proof for Theorem 4.8

uses 1

Induct over the span generators of the old space. Each generator is V_\ell of a new form at a proper divisor; decompose that new form into character pieces and then, by Theorem 2.2, into new eigenform summands. Level-raising is additive, so the generator becomes a sum of level-raised new eigenforms with tracked characters.

Theorem4.9

Statement uses 2

Statement dependency previews

Preview

Theorem 1.3

Loading preview

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

used by 1✓L∃∀N

On the \chi-isotypic part the project's degeneracy-defined old space coincides with Miyake's character-refined old space (span of V_\ell-images of new spaces at conductor-divisible levels) (Definition 4.3, Theorem 1.3). This identification makes the constant-multiple form of Strong Multiplicity One unconditional. (Miyake Lemma 4.6.4, 4.6.9.)

Lean code for Theorem4.9●2 theorems

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.cuspFormsOld_inf_charSpace_le_cuspFormsOldChar {N : ℕ}
  [NeZero N] {k : ℤ} (χ : DirichletCharacter ℂ N) :
  HeckeRing.GL2.cuspFormsOld N k ⊓
      HeckeRing.GL2.cuspFormCharSpace k (MulChar.toUnitHom χ) ≤
    HeckeRing.GL2.cuspFormsOldChar N k (MulChar.toUnitHom χ) χ.conductor

theorem HeckeRing.GL2.cuspFormsOld_inf_charSpace_le_cuspFormsOldChar
  {N : ℕ} [NeZero N] {k : ℤ}
  (χ : DirichletCharacter ℂ N) :
  HeckeRing.GL2.cuspFormsOld N k ⊓
      HeckeRing.GL2.cuspFormCharSpace k
        (MulChar.toUnitHom χ) ≤
    HeckeRing.GL2.cuspFormsOldChar N k
      (MulChar.toUnitHom χ) χ.conductor

**Gap #4, reverse inclusion (Miyake 4.6.12, T012).**  Every project-oldform in the
`χ`-Nebentypus space is a Miyake `χ`-oldform.  This is the reverse of the proven forward
`cuspFormsOldChar_le_cuspFormsOld`; together they identify the two old spaces on the
`χ`-isotypic part, making `strongMultiplicityOne_constMul` (Theorem 4.6.12) **unconditional**.

Proof: Phase 1 (`cuspFormsOld_le_oldNewGenSpan`, the Diamond–Shurman recursive normal form via
level-raise associativity) ∘ generator refinement (`oldNewGenSpan_le_oldNewGenCharSpan`) ∘
Phase 2 (`oldNewGenCharSpan_inf_charSpace_le_cuspFormsOldChar`, the isotypic collapse with the
conductor divisibility from Miyake 4.6.4).

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.cuspFormsOldChar_le_cuspFormsOld {N : ℕ} [NeZero N]
  {k : ℤ} (χ : (ZMod N)ˣ →* ℂˣ) (m_χ : ℕ) :
  HeckeRing.GL2.cuspFormsOldChar N k χ m_χ ≤
    HeckeRing.GL2.cuspFormsOld N k

theorem HeckeRing.GL2.cuspFormsOldChar_le_cuspFormsOld
  {N : ℕ} [NeZero N] {k : ℤ}
  (χ : (ZMod N)ˣ →* ℂˣ) (m_χ : ℕ) :
  HeckeRing.GL2.cuspFormsOldChar N k χ
      m_χ ≤
    HeckeRing.GL2.cuspFormsOld N k

**Gap #4 bridge.**  The χ-refined old space is contained in the project's
character-agnostic `cuspFormsOld N k`.  This lets the new-part argument and the
final contradiction in 4.6.12 reuse the existing `cuspFormsOld_disjoint_cuspFormsNew`
and route-B Main Lemma without re-deriving them for `cuspFormsOldChar`.

(One inclusion suffices for the proof of 4.6.12; the reverse inclusion — that every
project-oldform in the χ-space is a Miyake-oldform — is NOT needed and is harder.)

Proof for Theorem 4.9

uses 1

One inclusion is direct. For the reverse: rewrite the old space in the recursive normal form (span of V_\ell of new spaces) using level-raise associativity; refine each generator to a single character at its own level; then on the \chi-isotypic part the character-space independence (Theorem 1.3) collapses the sum to the matching-character pieces, whose source levels are conductor divisible by Miyake 4.6.4.