Polynomial Ring Structure of the p-local Hecke Ring

Shimura's Theorem 3.20: the p-local Hecke ring RP^{(n)} is isomorphic to a polynomial ring ℤ[X₁,...,Xₙ] in n variables.

Main definitions

• TGenDiag — the diagonal for the k-th generator T(1,...,1,p,...,p)
• TGen — the k-th generator of RP: TGen k = T(1,...,1,p,...,p) with k+1 entries of p
• ppowWeight — weight of a p-power diagonal: sum of exponents

Main results

• divChain_T_gen — the TGen diagonal satisfies the divisibility chain condition
• T_gen_mem_R_p — each generator lies in RP

References

• Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §3.2, Theorem 3.20

Generator diagonals

def HeckeRing.GLn.TGenDiag (n p : ℕ) (k : Fin n) : Fin n → ℕ

The diagonal for the k-th generator: (1,...,1,p,...,p) with n-1-k ones followed by k+1 entries of p. Here k : Fin n, giving n generators.

Equations

• HeckeRing.GLn.TGenDiag n p k i = if ↑i < n - 1 - ↑k then 1 else p

@[simp]

theorem HeckeRing.GLn.T_gen_diag_val (n p : ℕ) (k i : Fin n) : TGenDiag n p k i = if ↑i < n - 1 - ↑k then 1 else p

theorem HeckeRing.GLn.T_gen_diag_pos (n p : ℕ) (hp : Nat.Prime p) (k i : Fin n) : 0 < TGenDiag n p k i

theorem HeckeRing.GLn.divChain_T_gen (n p : ℕ) (k : Fin n) : DivChain n (TGenDiag n p k)

The TGen diagonal satisfies the divisibility chain condition.

theorem HeckeRing.GLn.T_gen_diag_is_ppow (n p : ℕ) (k : Fin n) : TGenDiag n p k = ppowDiag n p fun (i : Fin n) => if ↑i < n - 1 - ↑k then 0 else 1

The TGen diagonal has p-power entries (each entry is 1 = p^0 or p = p^1).

theorem HeckeRing.GLn.T_gen_exp_monotone (n : ℕ) (k : Fin n) : Monotone fun (i : Fin n) => if ↑i < n - 1 - ↑k then 0 else 1

The exponent function for TGen is monotone.

noncomputable def HeckeRing.GLn.TGen (n p : ℕ) [NeZero n] (k : Fin n) : HeckeAlgebra n

The k-th generator of RP: T(1,...,1,p,...,p) with k+1 entries of p.

Equations

• HeckeRing.GLn.TGen n p k = HeckeRing.GLn.TElem (HeckeRing.GLn.TGenDiag n p k)

theorem HeckeRing.GLn.T_gen_mem_R_p (n p : ℕ) (hp : Nat.Prime p) [NeZero n] (k : Fin n) : TGen n p k ∈ RP n p hp

Each TGen lies in RP.

Weight of a p-power diagonal

def HeckeRing.GLn.ppowWeight (n : ℕ) (e : Fin n → ℕ) : ℕ

Weight of a p-power diagonal: the sum of all exponents.

Equations

• HeckeRing.GLn.ppowWeight n e = ∑ i : Fin n, e i

theorem HeckeRing.GLn.ppowWeight_eq_zero_iff (n : ℕ) (e : Fin n → ℕ) : ppowWeight n e = 0 ↔ ∀ (i : Fin n), e i = 0

Weight is zero iff all exponents are zero.

Polynomial ring isomorphism (Theorem 3.20)

noncomputable def HeckeRing.GLn.evalHom (n : ℕ) [NeZero n] (p : ℕ) : MvPolynomial (Fin n) ℤ →+* HeckeAlgebra n

Evaluation homomorphism: Xₖ ↦ TGen k. Maps ℤ[X₁,...,Xₙ] into the Hecke algebra.

Equations

• HeckeRing.GLn.evalHom n p = MvPolynomial.eval₂Hom (Int.castRingHom (HeckeRing.GLn.HeckeAlgebra n)) fun (k : Fin n) => HeckeRing.GLn.TGen n p k

Infrastructure for the isomorphism

theorem HeckeRing.GLn.T_elem_ones_eq_one (n : ℕ) [NeZero n] : (TElem fun (x : Fin n) => 1) = 1

T(1,...,1) is the multiplicative identity in the Hecke algebra, for any n.

theorem HeckeRing.GLn.T_scalar_pow (n : ℕ) [NeZero n] (c : ℕ) (hc : 0 < c) (k : ℕ) : (TElem fun (x : Fin n) => c) ^ k = TElem fun (x : Fin n) => c ^ k

T(c,...,c)^k = T(c^k,...,c^k): scalar diagonal elements are closed under powers.

theorem HeckeRing.GLn.T_gen_mem_evalHom_range (n : ℕ) [NeZero n] (p : ℕ) (k : Fin n) : TGen n p k ∈ (evalHom n p).range

Each TGen k lies in the range of evalHom.

Surjectivity for n = 2 (Shimura Theorem 3.20)

Bridge lemmas: TGen at n=2 matches GL2 definitions

theorem HeckeRing.GLn.Surj.T_gen_zero_eq_T_ad (p : ℕ) (hp : Nat.Prime p) : TGen 2 p 0 = GL2.TAd 1 p

TGen 2 p 0 = TAd 1 p: the first generator is T(1,p).

theorem HeckeRing.GLn.Surj.T_gen_one_eq_T_pp (p : ℕ) (hp : Nat.Prime p) : TGen 2 p 1 = GL2.TPp p

TGen 2 p 1 = TPp p: the second generator is the diamond operator.

theorem HeckeRing.GLn.Surj.T_sum_p_eq_T_gen_zero (p : ℕ) (hp : Nat.Prime p) : GL2.TSum ⟨p, ⋯⟩ = TGen 2 p 0

TSum(p) = TGen 0: the sum T(p) is the first generator for p prime.

Step 3: TSum(p^k) in evalHom range by strong induction

theorem HeckeRing.GLn.Surj.T_sum_ppow_in_range (p : ℕ) (hp : Nat.Prime p) (k : ℕ) : GL2.TSum ⟨p ^ k, ⋯⟩ ∈ (evalHom 2 p).range

TSum(p^k) lies in the range of the evaluation homomorphism, for all k.

Step 4: TAd(1, p^k) in evalHom range

theorem HeckeRing.GLn.Surj.T_ad_one_ppow_in_range (p : ℕ) (hp : Nat.Prime p) (k : ℕ) : GL2.TAd 1 (p ^ k) ∈ (evalHom 2 p).range

TAd(1, p^k) lies in the range of the evaluation homomorphism.

Step 5: General ppow element for n=2

theorem HeckeRing.GLn.Surj.T_elem_ppow_in_range (p : ℕ) (hp : Nat.Prime p) (e : Fin 2 → ℕ) (hmono : Monotone e) : TElem (ppowDiag 2 p e) ∈ (evalHom 2 p).range

TElem (ppowDiag 2 p e) is in the evalHom range when e is monotone. Factor out T(p^{e₀}, p^{e₀}) to reduce to T(1, p^{e₁-e₀}).

Step 6: Assembly — every RP element is in the image

theorem HeckeRing.GLn.Surj.T_gen_generates_R_p_two (p : ℕ) (hp : Nat.Prime p) (f : HeckeAlgebra 2) : f ∈ RP 2 p hp → f ∈ (evalHom 2 p).range

Surjectivity of evalHom at n=2: every element of RP 2 p is in the range of the evaluation homomorphism ℤ[X₁, X₂] → HeckeAlgebra 2.

Surjectivity for n = 1

theorem HeckeRing.GLn.SurjOne.T_gen_generates_R_p_one (p : ℕ) (hp : Nat.Prime p) (f : HeckeAlgebra 1) : f ∈ RP 1 p hp → f ∈ (evalHom 1 p).range

n=1 surjectivity: every element of RP is in the range of evalHom.

Injectivity

evalHom maps into RP

theorem HeckeRing.GLn.Inj.evalHom_mem_R_p (n : ℕ) [NeZero n] (p : ℕ) (hp : Nat.Prime p) (P : MvPolynomial (Fin n) ℤ) : (evalHom n p) P ∈ RP n p hp

Every element in the image of evalHom belongs to RP.

noncomputable def HeckeRing.GLn.Inj.evalHomR (n : ℕ) [NeZero n] (p : ℕ) (hp : Nat.Prime p) : MvPolynomial (Fin n) ℤ →+* ↥(RP n p hp)

The restricted evaluation homomorphism into RP.

Equations

• HeckeRing.GLn.Inj.evalHomR n p hp = { toFun := fun (P : MvPolynomial (Fin n) ℤ) => ⟨(HeckeRing.GLn.evalHom n p) P, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

n=1 injectivity

theorem HeckeRing.GLn.Inj.evalHom_injective_one (p : ℕ) (hp : Nat.Prime p) : Function.Injective ⇑(evalHom 1 p)

n=1: evalHom is injective. Different monomials map to distinct basis elements, so the images are ℤ-linearly independent.

Surjectivity of restricted evalHom

theorem HeckeRing.GLn.Inj.evalHomR_surjective (n : ℕ) [NeZero n] (p : ℕ) (hp : Nat.Prime p) (h_surj : ∀ f ∈ RP n p hp, f ∈ (evalHom n p).range) : Function.Surjective ⇑(evalHomR n p hp)

Surjectivity of evalHomR follows from surjectivity onto RP.

theorem HeckeRing.GLn.Inj.evalHomR_injective (n : ℕ) [NeZero n] (p : ℕ) (_hp : Nat.Prime p) (h_inj : Function.Injective ⇑(evalHom n p)) : Function.Injective ⇑(evalHomR n p _hp)

Injectivity of evalHomR follows from injectivity of evalHom.