Good Hecke eigenforms and newforms, as bundled forms

A good Hecke eigenform of level Γ₁(N) and weight k is a nonzero cusp form with a nebentypus χ that is a simultaneous eigenvector of the Γ₀(N) Hecke ring acting on cuspFormCharSpace k χ (heckeRingHomCuspCharSpace), at every index coprime to the level. A newform is a good Hecke eigenform lying in the new subspace and normalised by a₁ = 1: Miyake's primitive form (§4.6). Both are bundled here as structures extending CuspForm, so that the character, the eigenvalue system and the analytic invariants travel with the form.

Design

• Eigen-ness is demanded only at indices coprime to N, and the eigenvalues are stored only there: eigenvalue n hn takes the coprimality proof hn as an argument, and isEigen n hn is its characteristic equation, heckeTCompositeGamma0 N n acting on the form by eigenvalue n hn. No value and no eigencondition is packaged at an index not coprime to N; the ring element exists there, but its action on a good eigenform is not part of this notion (and is not a claim about U_n).
• A good eigenform is determined by its underlying cusp form: the character by eq_of_mem_cuspFormCharSpace_of_ne_zero, the eigenvalues by cancelling the nonzero form in the eigenvector equations (EigenformAwayFromLevel.ext).
• That a newform is an eigenvector of every T_n is a theorem (Atkin–Lehner–Li; Miyake Theorem 4.6.13), not a field, and so is the comparison of the ring eigenvalues with the classical operator heckeTCuspNat; neither is proved here.

Main definitions

• HeckeRing.GL2.EigenformAwayFromLevel: the bundled good Hecke eigenform, with its eigenvalue system EigenformAwayFromLevel.eigenvalue at the indices coprime to the level.
• HeckeRing.GL2.Newform: the bundled newform.
• HeckeRing.GL2.Newform.dirichletLift: its nebentypus as a zero-extended Dirichlet character.

Main results

• HeckeRing.GL2.EigenformAwayFromLevel.ext, HeckeRing.GL2.Newform.ext: the bundled data is determined by the underlying cusp form.
• HeckeRing.GL2.Newform.qExpansion_coeff_one: the normalisation a₁ = 1 as a simp lemma.

Provenance

Follows the shapes of structure Eigenform and structure Newform of the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Newforms/{Basic,MainLemma}.lean, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), with these differences: the structure is named for the qualified notion, nonzeroness is a field, the character space is the cusp-form one, and the eigenvalues are stored at the good indices only rather than as a total function with unconstrained values at the bad ones. The source's classical eigenvalue Eigenform.eigenvalue (which in its convention carries a diamond factor χ(n)) is not reproduced.

References

• F. Diamond and J. Shurman, A first course in modular forms, §5.8.
• T. Miyake, Modular forms, §4.6.

structure HeckeRing.GL2.EigenformAwayFromLevel (N : ℕ) [NeZero N] (k : ℤ) extends CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k : Type

A good Hecke eigenform, bundled. A nonzero cusp form of level Γ₁(N) with a nebentypus χ, together with an eigenvalue system for the Γ₀(N) Hecke ring acting on cuspFormCharSpace k χ: at every index n coprime to N, the ring element heckeTCompositeGamma0 N n acts by the scalar eigenvalue n hn. Eigen-ness is demanded, and an eigenvalue stored, only away from the level.

• toFun : UpperHalfPlane → ℂ
• slash_action_eq' (γ : GL (Fin 2) ℝ) : γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) → SlashAction.map k γ self.toFun = self.toFun
• holo' : MDiff ⇑self.toSlashInvariantForm
• zero_at_cusps' {c : OnePoint ℝ} (hc : IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N))) : c.IsZeroAt self.toFun k
• χ : (ZMod N)ˣ →* ℂˣ

  The nebentypus character.

• mem_charSpace : self.toCuspForm ∈ cuspFormCharSpace k self.χ

  The form transforms under the diamond operators by χ.

• eigenvalue (n : ℕ+) : (↑n).Coprime N → ℂ

  The eigenvalue at an index coprime to the level.

• isEigen (n : ℕ+) (hn : (↑n).Coprime N) : ((heckeRingHomCuspCharSpace k self.χ) (heckeTCompositeGamma0 N ↑n)) ⟨self.toCuspForm, ⋯⟩ = self.eigenvalue n hn • ⟨self.toCuspForm, ⋯⟩

  At an index n coprime to N, the Hecke ring element heckeTCompositeGamma0 N n acts on the form by eigenvalue n hn.

• ne_zero : self.toCuspForm ≠ 0

  An eigenform is nonzero.

structure HeckeRing.GL2.Newform (N : ℕ) [NeZero N] (k : ℤ) extends HeckeRing.GL2.EigenformAwayFromLevel N k : Type

A newform: a good Hecke eigenform lying in the new subspace and normalised by a₁ = 1 (Miyake's primitive form). That a newform is an eigenform for every T_n is a theorem, not part of the definition.

• toFun : UpperHalfPlane → ℂ
• slash_action_eq' (γ : GL (Fin 2) ℝ) : γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) → SlashAction.map k γ self.toFun = self.toFun
• holo' : MDiff ⇑self.toSlashInvariantForm
• zero_at_cusps' {c : OnePoint ℝ} (hc : IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N))) : c.IsZeroAt self.toFun k
• χ : (ZMod N)ˣ →* ℂˣ
• mem_charSpace : self.toCuspForm ∈ cuspFormCharSpace k self.χ
• eigenvalue (n : ℕ+) : (↑n).Coprime N → ℂ
• isEigen (n : ℕ+) (hn : (↑n).Coprime N) : ((heckeRingHomCuspCharSpace k self.χ) (heckeTCompositeGamma0 N ↑n)) ⟨self.toCuspForm, ⋯⟩ = self.eigenvalue n hn • ⟨self.toCuspForm, ⋯⟩
• ne_zero : self.toCuspForm ≠ 0
• isNew : self.toCuspForm ∈ TauCeti.cuspFormsNew N k

  The form lies in the new subspace S_k(Γ₁(N))ⁿᵉʷ.

• isNorm : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑self.toCuspForm) = 1

  The form is normalised: its first Fourier coefficient is 1.

theorem HeckeRing.GL2.EigenformAwayFromLevel.ext {N : ℕ} [NeZero N] {k : ℤ} {f g : EigenformAwayFromLevel N k} (h : f.toCuspForm = g.toCuspForm) : f = g

Extensionality: two good Hecke eigenforms with the same underlying cusp form are equal. The form determines its nebentypus, and the eigenvalues at good indices are read off the eigenvector equations.

theorem HeckeRing.GL2.EigenformAwayFromLevel.ext_iff {N : ℕ} [NeZero N] {k : ℤ} {f g : EigenformAwayFromLevel N k} : f = g ↔ f.toCuspForm = g.toCuspForm

noncomputable def HeckeRing.GL2.Newform.dirichletLift {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : DirichletCharacter ℂ N

The nebentypus of a newform, extended by zero from units modulo N to a Dirichlet character. This packages Mathlib's MulChar.ofUnitHom for formulas attached to the newform.

Equations

• f.dirichletLift = MulChar.ofUnitHom f.χ

theorem HeckeRing.GL2.Newform.dirichletLift_def {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : f.dirichletLift = MulChar.ofUnitHom f.χ

The zero extension defining the Dirichlet character of a newform.

@[simp]

theorem HeckeRing.GL2.Newform.dirichletLift_equivToUnitHom {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : MulChar.equivToUnitHom f.dirichletLift = f.χ

Restricting the zero-extended nebentypus to units recovers the character of the newform.

@[simp]

theorem HeckeRing.GL2.Newform.dirichletLift_apply_eq_zero {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (n : ℕ) (hn : ¬n.Coprime N) : f.dirichletLift ↑n = 0

The zero-extended nebentypus vanishes at indices not coprime to the level.

theorem HeckeRing.GL2.Newform.dirichletLift_apply_of_coprime {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {n : ℕ} (hn : n.Coprime N) : f.dirichletLift ↑n = ↑(f.χ (ZMod.unitOfCoprime n hn))

At an index coprime to the level, the zero-extended nebentypus takes the value of the nebentypus at the corresponding unit.

@[simp]

theorem HeckeRing.GL2.Newform.qExpansion_coeff_one {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = 1

The normalisation a₁ = 1, as a simp lemma. The eigenvector equation isEigen has no simp form: its right-hand side depends on the coprimality proof, so no rewrite rule can produce it.

theorem HeckeRing.GL2.Newform.ext {N : ℕ} [NeZero N] {k : ℤ} {f g : Newform N k} (h : f.toCuspForm = g.toCuspForm) : f = g

Extensionality: two newforms with the same underlying cusp form are equal.

theorem HeckeRing.GL2.Newform.ext_iff {N : ℕ} [NeZero N] {k : ℤ} {f g : Newform N k} : f = g ↔ f.toCuspForm = g.toCuspForm