Normality of the good Hecke operators

For an index n coprime to the level, the Petersson adjoint of Tₙ on S_k(Γ₁(N)) is ⟨n⟩⁻¹ Tₙ. The inverse diamond operator commutes with Tₙ, so this adjoint commutes with Tₙ: the good Hecke operator is normal for the Petersson product.

The result is stated without installing a global inner-product-space instance on cusp forms. Instead, peterssonInnerCosetsₛₗ.flip records the Petersson product as a sesquilinear form, peterssonInnerCosets_heckeTCuspNat_right supplies the adjoint formula in the opposite argument, and isAdjointPair_heckeTCuspNat packages both formulas in Mathlib's LinearMap.IsAdjointPair API. The final commutation theorem is therefore the instance-free form of normality needed for simultaneous diagonalization.

Main results

• HeckeRing.GL2.isAdjointPair_heckeTCuspNat: Tₙ and ⟨n⟩⁻¹ Tₙ are a Petersson-adjoint pair.
• HeckeRing.GL2.commute_peterssonAdjoint_heckeTCuspNat: the Petersson adjoint of Tₙ commutes with Tₙ.
• HeckeRing.GL2.isAdjointPair_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0: on a fixed nebentypus space, the adjoint of a good Tₚ is the scalar multiple χ(p)⁻¹ Tₚ.
• HeckeRing.GL2.commute_peterssonAdjoint_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0: this adjoint commutes with Tₚ on the fixed-nebentypus space.

References

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

noncomputable def TauCeti.CuspForm.peterssonInnerCosetsCharSpaceₛₗ {N : ℕ} [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) : ↥(cuspFormCharSpace k χ) →ₗ⋆[ℂ] ↥(cuspFormCharSpace k χ) →ₗ[ℂ] ℂ

The Petersson product restricted to the cusp forms of weight k and nebentypus χ.

This is a sesquilinear form rather than an InnerProductSpace instance: the analytic function space underlying cusp forms already has a normed structure, and the Petersson norm should not silently replace it.

Equations

• TauCeti.CuspForm.peterssonInnerCosetsCharSpaceₛₗ k χ = TauCeti.CuspForm.peterssonInnerCosetsₛₗ.domRestrict₁₂ (cuspFormCharSpace k χ) (cuspFormCharSpace k χ)

@[simp]

theorem TauCeti.CuspForm.peterssonInnerCosetsCharSpaceₛₗ_apply_apply {N : ℕ} [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) (f g : ↥(cuspFormCharSpace k χ)) : ((peterssonInnerCosetsCharSpaceₛₗ k χ) f) g = (↑f).peterssonInnerCosets ↑g

Evaluation of the Petersson product on a nebentypus space.

The Petersson-adjoint pair

theorem HeckeRing.GL2.peterssonInnerCosets_heckeTCuspNat_right {N n : ℕ} [NeZero N] [NeZero n] (k : ℤ) (hn : n.Coprime N) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : f.peterssonInnerCosets ((heckeTCuspNat k n) g) = ((diamondOpCusp k (ZMod.unitOfCoprime n hn)⁻¹) ((heckeTCuspNat k n) f)).peterssonInnerCosets g

The Petersson adjoint formula in the second argument. For n coprime to N,

⟪f, Tₙ g⟫ = ⟪⟨n⟩⁻¹ Tₙ f, g⟫.

This is the Hermitian transpose of peterssonInnerCosets_heckeTCuspNat_left.

theorem HeckeRing.GL2.isAdjointPair_heckeTCuspNat {N n : ℕ} [NeZero N] [NeZero n] (k : ℤ) (hn : n.Coprime N) : TauCeti.CuspForm.peterssonInnerCosetsₛₗ.flip.IsAdjointPair TauCeti.CuspForm.peterssonInnerCosetsₛₗ.flip ⇑(heckeTCuspNat k n) ⇑(diamondOpCusp k (ZMod.unitOfCoprime n hn)⁻¹ * heckeTCuspNat k n)

The Petersson adjoint of Tₙ is ⟨n⟩⁻¹ Tₙ, as an adjoint pair.

The Petersson form is flipped because LinearMap.IsAdjointPair is formulated for a form linear in its first argument, while peterssonInnerCosetsₛₗ follows the usual mathematical convention and is conjugate-linear in its first argument.

Normality

theorem HeckeRing.GL2.commute_peterssonAdjoint_heckeTCuspNat {N n : ℕ} [NeZero N] [NeZero n] (k : ℤ) (hn : n.Coprime N) : Commute (diamondOpCusp k (ZMod.unitOfCoprime n hn)⁻¹ * heckeTCuspNat k n) (heckeTCuspNat k n)

The good Hecke operator is Petersson-normal. For n coprime to N, its Petersson adjoint ⟨n⟩⁻¹ Tₙ commutes with Tₙ.

Together with isAdjointPair_heckeTCuspNat, this is the instance-free statement that Tₙ is a normal operator. It applies on the whole space S_k(Γ₁(N)), hence in particular after restricting to any Tₙ-stable nebentypus subspace.

Normality on a fixed nebentypus space

theorem HeckeRing.GL2.isAdjointPair_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0 {N : ℕ} [NeZero N] (k : ℤ) {χ : (ZMod N)ˣ →* ℂˣ} {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : (TauCeti.CuspForm.peterssonInnerCosetsCharSpaceₛₗ k χ).flip.IsAdjointPair (TauCeti.CuspForm.peterssonInnerCosetsCharSpaceₛₗ k χ).flip (⇑((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p))) ((↑(χ (ZMod.unitOfCoprime p hpN)))⁻¹ • ⇑((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)))

The Petersson adjoint of a good prime Hecke operator on S_k(N, χ). If p is prime and coprime to N, then the Hecke-ring action of Tₚ and its scalar multiple χ(p)⁻¹ Tₚ are an adjoint pair for the Petersson product restricted to the nebentypus space.

The operator is expressed through heckeRingHomCuspCharSpace, the canonical action on S_k(N, χ); heckeRingHomCuspCharSpace_heckeTGeneratorGamma0 identifies it with the classical Tₚ used by the ambient adjoint theorem.

theorem HeckeRing.GL2.commute_peterssonAdjoint_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0 {N : ℕ} [NeZero N] (k : ℤ) {χ : (ZMod N)ˣ →* ℂˣ} {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : Commute ((↑(χ (ZMod.unitOfCoprime p hpN)))⁻¹ • (heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p))

A good prime Hecke operator on S_k(N, χ) is Petersson-normal. Its adjoint χ(p)⁻¹ Tₚ commutes with Tₚ, in the canonical Hecke-ring action on the fixed-nebentypus space. Together with isAdjointPair_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0, this is the instance-free normality statement on S_k(N, χ).