Complex characters of the newspace Hecke algebra

The complex algebra generated on the new subspace by the good prime Hecke operators and the diamond operators has exactly one character for each normalized newform. Its character on T_p is the Fourier coefficient a_p, and its character on ⟨u⟩ is the nebentypus value χ(u). Including the diamonds distinguishes forms with different nebentypus.

heckeTDiamondCuspNewAlgebraEquiv identifies this algebra with the product of copies of ℂ indexed by newforms. Every complex character corresponds to a unique normalized newform.

References

• F. Diamond and J. Shurman, A first course in modular forms, Theorem 5.8.2.
• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Chapter 3, for the Hecke algebra and its eigenvalue characters.

noncomputable def TauCeti.heckeTCuspNewEnd (N : ℕ) [NeZero N] (k : ℤ) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : Module.End ℂ ↥(cuspFormsNew N k)

The restriction of a good prime Hecke operator to the new subspace.

Equations

• TauCeti.heckeTCuspNewEnd N k hp hpN = LinearMap.restrict (HeckeRing.GL2.heckeTCuspNat k p) ⋯

noncomputable def TauCeti.diamondOpCuspNewEnd (N : ℕ) [NeZero N] (k : ℤ) (u : (ZMod N)ˣ) : Module.End ℂ ↥(cuspFormsNew N k)

The restriction of a diamond operator to the new subspace.

Equations

• TauCeti.diamondOpCuspNewEnd N k u = (diamondOpCusp k u).restrict ⋯

@[simp]

theorem TauCeti.coe_heckeTCuspNewEnd_apply (N : ℕ) [NeZero N] (k : ℤ) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) (f : ↥(cuspFormsNew N k)) : ↑((heckeTCuspNewEnd N k hp hpN) f) = (HeckeRing.GL2.heckeTCuspNat k p) ↑f

@[simp]

theorem TauCeti.coe_diamondOpCuspNewEnd_apply (N : ℕ) [NeZero N] (k : ℤ) (u : (ZMod N)ˣ) (f : ↥(cuspFormsNew N k)) : ↑((diamondOpCuspNewEnd N k u) f) = (diamondOpCusp k u) ↑f

noncomputable def TauCeti.heckeTDiamondCuspNewAlgebra (N : ℕ) [NeZero N] (k : ℤ) : Subalgebra ℂ (Module.End ℂ ↥(cuspFormsNew N k))

The complex Hecke algebra on the new subspace, generated by the good T_p and diamonds.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.heckeTDiamondCuspNewAlgebra_def (N : ℕ) [NeZero N] (k : ℤ) : heckeTDiamondCuspNewAlgebra N k = Algebra.adjoin ℂ ((Set.range fun (p : { p : ℕ // Nat.Prime p ∧ p.Coprime N }) => heckeTCuspNewEnd N k ⋯ ⋯) ∪ Set.range (diamondOpCuspNewEnd N k))

The defining generators of the complex newspace Hecke algebra.

@[simp]

theorem TauCeti.heckeTCuspNewEnd_mem_heckeTDiamondCuspNewAlgebra (N : ℕ) [NeZero N] (k : ℤ) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : heckeTCuspNewEnd N k hp hpN ∈ heckeTDiamondCuspNewAlgebra N k

@[simp]

theorem TauCeti.diamondOpCuspNewEnd_mem_heckeTDiamondCuspNewAlgebra (N : ℕ) [NeZero N] (k : ℤ) (u : (ZMod N)ˣ) : diamondOpCuspNewEnd N k u ∈ heckeTDiamondCuspNewAlgebra N k

theorem TauCeti.heckeTDiamondCuspNewAlgebra_le_iff (N : ℕ) [NeZero N] (k : ℤ) (A : Subalgebra ℂ (Module.End ℂ ↥(cuspFormsNew N k))) : heckeTDiamondCuspNewAlgebra N k ≤ A ↔ (∀ (p : ℕ) (hp : Nat.Prime p) (hpN : p.Coprime N), heckeTCuspNewEnd N k hp hpN ∈ A) ∧ ∀ (u : (ZMod N)ˣ), diamondOpCuspNewEnd N k u ∈ A

An algebra contains the newspace Hecke algebra exactly when it contains every good prime Hecke operator and every diamond operator.

@[simp]

theorem TauCeti.heckeTCuspNewEnd_basis {N : ℕ} [NeZero N] {k : ℤ} {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) (f : HeckeRing.GL2.Newform N k) : (heckeTCuspNewEnd N k hp hpN) ((HeckeRing.GL2.Newform.basis N k) f) = f.eigenvalue ⟨p, ⋯⟩ hpN • (HeckeRing.GL2.Newform.basis N k) f

A good prime Hecke operator acts on a newform basis vector by its eigenvalue.

@[simp]

theorem TauCeti.diamondOpCuspNewEnd_basis {N : ℕ} [NeZero N] {k : ℤ} (u : (ZMod N)ˣ) (f : HeckeRing.GL2.Newform N k) : (diamondOpCuspNewEnd N k u) ((HeckeRing.GL2.Newform.basis N k) f) = ↑(f.χ u) • (HeckeRing.GL2.Newform.basis N k) f

A diamond operator acts on a newform basis vector by its nebentypus value.

noncomputable def TauCeti.Newform.heckeTDiamondCuspNewCharacter {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) : ↥(heckeTDiamondCuspNewAlgebra N k) →ₐ[ℂ] ℂ

The complex character of the newspace Hecke algebra associated with a normalized newform.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Newform.basis_repr_apply_eq_heckeTDiamondCuspNewCharacter {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) (T : ↥(heckeTDiamondCuspNewAlgebra N k)) : ((HeckeRing.GL2.Newform.basis N k).repr (↑T ((HeckeRing.GL2.Newform.basis N k) f))) f = (heckeTDiamondCuspNewCharacter f) T

The coordinate of an operator's image at its newform basis vector is its character.

@[simp]

theorem TauCeti.Newform.apply_basis_eq_heckeTDiamondCuspNewCharacter_smul {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) (T : ↥(heckeTDiamondCuspNewAlgebra N k)) : ↑T ((HeckeRing.GL2.Newform.basis N k) f) = (heckeTDiamondCuspNewCharacter f) T • (HeckeRing.GL2.Newform.basis N k) f

Every operator in the newspace Hecke algebra acts on a newform by its character.

@[simp]

theorem TauCeti.Newform.heckeTDiamondCuspNewCharacter_apply_heckeTCuspNewEnd {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : (heckeTDiamondCuspNewCharacter f) ⟨heckeTCuspNewEnd N k hp hpN, ⋯⟩ = f.eigenvalue ⟨p, ⋯⟩ hpN

The character on a good T_p is the good Hecke eigenvalue, hence the Fourier coefficient a_p of the normalized newform.

@[simp]

theorem TauCeti.Newform.heckeTDiamondCuspNewCharacter_apply_diamondOpCuspNewEnd {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) (u : (ZMod N)ˣ) : (heckeTDiamondCuspNewCharacter f) ⟨diamondOpCuspNewEnd N k u, ⋯⟩ = ↑(f.χ u)

The character on a diamond operator is the nebentypus value.

theorem TauCeti.Newform.heckeTDiamondCuspNewCharacter_injective {N : ℕ} [NeZero N] {k : ℤ} : Function.Injective heckeTDiamondCuspNewCharacter

Distinct newforms give distinct characters of the newspace Hecke algebra. The diamond values determine the nebentypus, and the good prime values then determine the newform.

noncomputable def TauCeti.Newform.heckeTDiamondCuspNewAlgebraEquiv {N : ℕ} [NeZero N] {k : ℤ} : ↥(heckeTDiamondCuspNewAlgebra N k) ≃ₐ[ℂ] HeckeRing.GL2.Newform N k → ℂ

Evaluation on the newform basis identifies the complex newspace Hecke algebra with the product of copies of ℂ indexed by normalized newforms. In particular it is a split semisimple commutative algebra.

Equations

• TauCeti.Newform.heckeTDiamondCuspNewAlgebraEquiv = AlgEquiv.ofBijective (AlgHom.pi TauCeti.Newform.heckeTDiamondCuspNewCharacter) ⋯

@[simp]

theorem TauCeti.Newform.heckeTDiamondCuspNewAlgebraEquiv_apply {N : ℕ} [NeZero N] {k : ℤ} (T : ↥(heckeTDiamondCuspNewAlgebra N k)) (f : HeckeRing.GL2.Newform N k) : heckeTDiamondCuspNewAlgebraEquiv T f = (heckeTDiamondCuspNewCharacter f) T

theorem TauCeti.Newform.heckeTDiamondCuspNewCharacter_surjective {N : ℕ} [NeZero N] {k : ℤ} : Function.Surjective heckeTDiamondCuspNewCharacter

Every complex character of the newspace Hecke algebra belongs to a normalized newform.

noncomputable def TauCeti.Newform.heckeTDiamondCuspNewCharacterEquiv {N : ℕ} [NeZero N] {k : ℤ} : HeckeRing.GL2.Newform N k ≃ (↥(heckeTDiamondCuspNewAlgebra N k) →ₐ[ℂ] ℂ)

The normalized newforms are in bijection with the complex characters of the newspace Hecke algebra.

Equations

• TauCeti.Newform.heckeTDiamondCuspNewCharacterEquiv = Equiv.ofBijective TauCeti.Newform.heckeTDiamondCuspNewCharacter ⋯

@[simp]

theorem TauCeti.Newform.heckeTDiamondCuspNewCharacterEquiv_apply {N : ℕ} [NeZero N] {k : ℤ} (f : HeckeRing.GL2.Newform N k) : heckeTDiamondCuspNewCharacterEquiv f = heckeTDiamondCuspNewCharacter f

@[instance_reducible]

noncomputable instance TauCeti.instCommRingHeckeTDiamondCuspNewAlgebra {N : ℕ} [NeZero N] {k : ℤ} : CommRing ↥(heckeTDiamondCuspNewAlgebra N k)

The newspace Hecke algebra is commutative, with its existing operator ring structure.

Equations

• TauCeti.instCommRingHeckeTDiamondCuspNewAlgebra = { toRing := (TauCeti.heckeTDiamondCuspNewAlgebra N k).toRing, mul_comm := ⋯ }