Finiteness of the integral algebra generated by the cusp-form Hecke operators

The ℤ-algebra generated by all positive-index Tₙ on S_k(Γ₁(N)) is a finite ℤ-module when k ≥ 2. Consequently each of these operators is integral over ℤ, including the operators at primes dividing the level.

The integral object is the finite module of modular symbols, paired with cusp forms through the injective period map. The free-algebra transfer evaluates the symbol operators in the opposite endomorphism ring, accounting for the order reversal under precomposition. No commutativity of the operators and no lattice inside the space of cusp forms are needed.

The algebra here is generated by the Tₙ alone. Diamond operators are not included in its definition.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Chapter 3, especially Theorems 3.48 and 3.51.
• T. Miyake, Modular forms, Section 4.5.

def TauCeti.heckeTCuspAlgebra (N : ℕ) [NeZero N] (k : ℤ) : Subalgebra ℤ (Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k))

The integral algebra of endomorphisms of S_k(Γ₁(N)) generated by the Hecke operators Tₙ at every positive index, including indices sharing prime factors with the level.

Equations

• TauCeti.heckeTCuspAlgebra N k = Algebra.adjoin ℤ (Set.range (TauCeti.heckeTCuspPos✝ N k))

theorem TauCeti.heckeTCuspAlgebra_def (N : ℕ) [NeZero N] (k : ℤ) : heckeTCuspAlgebra N k = Algebra.adjoin ℤ (Set.range fun (n : ℕ+) => HeckeRing.GL2.heckeTCuspNat k ↑n)

The defining generators of the integral cusp-form Hecke algebra.

@[simp]

theorem TauCeti.heckeTCuspNat_mem_heckeTCuspAlgebra (N : ℕ) [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] : HeckeRing.GL2.heckeTCuspNat k n ∈ heckeTCuspAlgebra N k

Each positive-index Hecke operator belongs to the integral cusp-form Hecke algebra.

theorem TauCeti.heckeTCuspAlgebra_le_iff (N : ℕ) [NeZero N] (k : ℤ) (A : Subalgebra ℤ (Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k))) : heckeTCuspAlgebra N k ≤ A ↔ ∀ (n : ℕ) [inst : NeZero n], HeckeRing.GL2.heckeTCuspNat k n ∈ A

An integral subalgebra contains the cusp-form Hecke algebra exactly when it contains Tₙ at every positive index.

def TauCeti.heckeTCuspPrimeAlgebra (N : ℕ) [NeZero N] (k : ℤ) : Subalgebra ℤ (Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k))

The integral algebra of endomorphisms of S_k(Γ₁(N)) generated by the prime-index Hecke operators Tₚ.

Equations

• TauCeti.heckeTCuspPrimeAlgebra N k = Algebra.adjoin ℤ (Set.range fun (p : { p : ℕ // Nat.Prime p }) => HeckeRing.GL2.heckeTCuspNat k ↑p)

theorem TauCeti.heckeTCuspPrimeAlgebra_def (N : ℕ) [NeZero N] (k : ℤ) : heckeTCuspPrimeAlgebra N k = Algebra.adjoin ℤ (Set.range fun (p : { p : ℕ // Nat.Prime p }) => HeckeRing.GL2.heckeTCuspNat k ↑p)

The defining generators of the prime-index cusp-form Hecke algebra.

@[simp]

theorem TauCeti.heckeTCuspNat_mem_heckeTCuspPrimeAlgebra (N : ℕ) [NeZero N] (k : ℤ) {p : ℕ} (hp : Nat.Prime p) : HeckeRing.GL2.heckeTCuspNat k p ∈ heckeTCuspPrimeAlgebra N k

Every prime-index Hecke operator belongs to the prime-index cusp-form Hecke algebra.

theorem TauCeti.heckeTCuspPrimeAlgebra_le_iff (N : ℕ) [NeZero N] (k : ℤ) (A : Subalgebra ℤ (Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k))) : heckeTCuspPrimeAlgebra N k ≤ A ↔ ∀ (p : ℕ) (hp : Nat.Prime p), HeckeRing.GL2.heckeTCuspNat k p ∈ A

An integral subalgebra contains the prime-index cusp-form Hecke algebra exactly when it contains Tₚ at every prime.

theorem TauCeti.heckeTCuspPrimeAlgebra_le_heckeTCuspAlgebra (N : ℕ) [NeZero N] (k : ℤ) : heckeTCuspPrimeAlgebra N k ≤ heckeTCuspAlgebra N k

The prime-index cusp-form Hecke algebra is contained in the cusp-form Hecke algebra.

theorem TauCeti.heckeTCuspAlgebra_finite (N : ℕ) [NeZero N] (k : ℤ) (hk : 2 ≤ k) : Module.Finite ℤ ↥(heckeTCuspAlgebra N k)

The integral algebra generated by all Tₙ on cusp forms is a finite ℤ-module in weight at least two. This includes every bad-prime operator.

theorem TauCeti.heckeTCuspPrimeAlgebra_finite (N : ℕ) [NeZero N] (k : ℤ) (hk : 2 ≤ k) : Module.Finite ℤ ↥(heckeTCuspPrimeAlgebra N k)

The integral algebra generated by the prime-index Hecke operators on cusp forms is a finite ℤ-module in weight at least two.

theorem TauCeti.isIntegral_of_mem_heckeTCuspAlgebra (N : ℕ) [NeZero N] (k : ℤ) (hk : 2 ≤ k) {T : Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)} (hT : T ∈ heckeTCuspAlgebra N k) : IsIntegral ℤ T

Every operator in the integral cusp-form Hecke algebra is integral over ℤ.

theorem TauCeti.isIntegral_heckeTCuspNat (N : ℕ) [NeZero N] (k : ℤ) (hk : 2 ≤ k) (n : ℕ) [NeZero n] : IsIntegral ℤ (HeckeRing.GL2.heckeTCuspNat k n)

Each positive-index Tₙ acting on cusp forms of weight at least two is integral over ℤ. At a prime dividing the level this asserts integrality of Uₚ = Tₚ.