A simultaneous eigenbasis for the good Hecke operators

On a fixed nebentypus space S_k(N, χ), the good prime Hecke operators commute and are normal for the Petersson product. This file applies the finite-dimensional spectral theorem to obtain a Petersson-orthonormal basis whose vectors are good Hecke eigenforms.

The Petersson product is not installed globally as the inner product on cusp forms, because that would replace their existing function-space norm. Accordingly, the public result exposes an ordinary algebraic basis together with its explicit Petersson orthonormality equation. Internally we install the Petersson inner-product core only while applying Mathlib's joint-eigenspace API.

Main result

• HeckeRing.GL2.exists_peterssonOrthonormalBasis_eigenformAwayFromLevel: every fixed nebentypus cusp space has a finite Petersson-orthonormal basis whose vectors underlie bundled good Hecke eigenforms with that nebentypus.

Provenance

The rescaling of a good Hecke operator to a symmetric operator follows the proof of exists_simultaneous_eigenform_basis in the AINTLIB LeanModularForms project at commit 112d12d95 (HeckeRIngs/GL2/AdjointTheoryPetersson.lean, Apache-2.0). The basis construction here instead uses Mathlib's joint-eigenspace and collected-orthonormal-basis APIs, and the public statement records spanning and unit norm explicitly.

References

• F. Diamond and J. Shurman, A first course in modular forms, Theorem 5.5.4.
• T. Miyake, Modular forms, Theorem 4.5.4.

The commuting symmetric family

@[instance_reducible]

noncomputable def HeckeRing.GL2.peterssonInnerCosetsCoreInstance {N : ℕ} [NeZero N] (k : ℤ) : InnerProductSpace.Core ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The Petersson core, installed locally for the spectral argument.

Equations

• HeckeRing.GL2.peterssonInnerCosetsCoreInstance k = CuspForm.peterssonInnerCosetsCore

@[instance_reducible]

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

The Petersson normed additive structure, installed only for the spectral argument.

Equations

• HeckeRing.GL2.peterssonNormedAddCommGroup k = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

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

The Petersson inner-product structure, installed only for the spectral argument.

Equations

• HeckeRing.GL2.peterssonInnerProductSpace k = InnerProductSpace.ofCore (HeckeRing.GL2.peterssonInnerCosetsCoreInstance k).toCore

The simultaneous eigenbasis

theorem HeckeRing.GL2.exists_peterssonOrthonormalBasis_eigenformAwayFromLevel {N : ℕ} [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) : ∃ (I : Type) (b : Module.Basis I ℂ ↥(cuspFormCharSpace k χ)), Finite I ∧ (∀ (i : I), (↑(b i)).peterssonInnerCosets ↑(b i) = 1) ∧ (∀ (i j : I), i ≠ j → (↑(b i)).peterssonInnerCosets ↑(b j) = 0) ∧ ∀ (i : I), ∃ (f : EigenformAwayFromLevel N k), f.χ = χ ∧ f.toCuspForm = ↑(b i)

The good Hecke operators admit a simultaneous Petersson-orthonormal eigenbasis.

More precisely, the fixed-nebentypus cusp space has a finite algebraic basis b satisfying <b_i, b_j>_Pet = δ_ij, and every b_i is the underlying form of a bundled EigenformAwayFromLevel with nebentypus χ. The explicit Petersson equation avoids changing the globally installed function-space norm on cusp forms.