Prime Decomposition of Hecke Ring Elements

p-adic decomposition of diagonal Hecke operators and the p-local Hecke subring RP. Every T(a₁,...,aₙ) factors into a product of p-power T-elements via coprime splitting.

Main definitions

• ppowDiag — p-power diagonal: entries are p^(e i)
• pComponent — extract the p-adic valuation of each diagonal entry
• removePrime — remove the p-component from a diagonal (p-free part)
• RP — the p-local Hecke subring generated by p-power T-elements

Main results

• divChain_ppow — monotone exponents give a divisibility chain for p-power diagonals
• T_elem_split_prime — binary prime splitting: T(a) = T(p-part) · T(p-free part)
• T_elem_ppow_mem_R_p — p-power T-elements lie in RP
• T_elem_mem_closure_ppow — every T-element is in the subring generated by all p-local pieces

References

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

p-power diagonals

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

p-power diagonal: entries are p^(e i).

Equations

• HeckeRing.GLn.ppowDiag n p e i = p ^ e i

theorem HeckeRing.GLn.ppowDiag_pos (n p : ℕ) (hp : Nat.Prime p) (e : Fin n → ℕ) (i : Fin n) : 0 < ppowDiag n p e i

theorem HeckeRing.GLn.divChain_ppow (n p : ℕ) (e : Fin n → ℕ) (hmono : Monotone e) : DivChain n (ppowDiag n p e)

DivChain for p-power diagonals when exponents are monotone.

def HeckeRing.GLn.pComponent (n p : ℕ) (a : Fin n → ℕ) : Fin n → ℕ

Extract the p-component of each entry in a positive diagonal.

Equations

• HeckeRing.GLn.pComponent n p a i = (a i).factorization p

theorem HeckeRing.GLn.pComponent_monotone (n : ℕ) (a : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) (ha : DivChain n a) (p : ℕ) : Monotone (pComponent n p a)

The p-component of a divisibility chain is monotone.

Prime removal: extracting the p-free part

noncomputable def HeckeRing.GLn.removePrime (n p : ℕ) (a : Fin n → ℕ) : Fin n → ℕ

Remove the p-component from each entry: a_i ↦ a_i / p^{v_p(a_i)}. This is the p-free part (ordCompl) of each diagonal entry.

Equations

• HeckeRing.GLn.removePrime n p a i = a i / p ^ (a i).factorization p

theorem HeckeRing.GLn.removePrime_pos (n p : ℕ) (a : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) (i : Fin n) : 0 < removePrime n p a i

theorem HeckeRing.GLn.removePrime_divChain (n p : ℕ) (a : Fin n → ℕ) (ha : DivChain n a) : DivChain n (removePrime n p a)

The p-free part preserves divisibility chains.

theorem HeckeRing.GLn.mul_ppow_remove_eq (n p : ℕ) (a : Fin n → ℕ) : ppowDiag n p (pComponent n p a) * removePrime n p a = a

Recovery: the pointwise product of p-part and p-free part equals the original.

Coprimality of p-part and p-free part determinants

theorem HeckeRing.GLn.prod_ppow (n p : ℕ) (e : Fin n → ℕ) : ∏ i : Fin n, ppowDiag n p e i = p ^ ∑ i : Fin n, e i

The determinant of a p-power diagonal is a power of p.

theorem HeckeRing.GLn.prod_ppow_remove_coprime (n p : ℕ) (hp : Nat.Prime p) (a : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) : (∏ i : Fin n, ppowDiag n p (pComponent n p a) i).Coprime (∏ i : Fin n, removePrime n p a i)

The p-part and p-free part determinants are coprime.

Binary prime splitting theorem

theorem HeckeRing.GLn.T_elem_congr_diag (n : ℕ) [NeZero n] {a b : Fin n → ℕ} (h : a = b) : TElem a = TElem b

TElem is determined by its diagonal, independent of the positivity/DivChain proofs.

theorem HeckeRing.GLn.T_elem_split_prime (n : ℕ) [NeZero n] (a : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) (ha : DivChain n a) (p : ℕ) (hp : Nat.Prime p) : TElem a = TElem (ppowDiag n p (pComponent n p a)) * TElem (removePrime n p a)

Binary prime splitting: T(a) = T(p-part) · T(p-free part). Every diagonal Hecke element factors into its p-power component and its p-free component, for any prime p.

p-local Hecke subring

noncomputable def HeckeRing.GLn.RP (n : ℕ) [NeZero n] (p : ℕ) (hp : Nat.Prime p) : Subring (HeckeAlgebra n)

The p-local Hecke ring: subring generated by TElem with p-power entries. This is Shimura's RP^{(n)}.

Equations

• HeckeRing.GLn.RP n p hp = Subring.closure {f : HeckeRing.GLn.HeckeAlgebra n | ∃ (e : Fin n → ℕ) (_ : Monotone e), f = HeckeRing.GLn.TElem (HeckeRing.GLn.ppowDiag n p e)}

theorem HeckeRing.GLn.T_elem_ppow_mem_R_p (n : ℕ) [NeZero n] (p : ℕ) (hp : Nat.Prime p) (e : Fin n → ℕ) (hmono : Monotone e) : TElem (ppowDiag n p e) ∈ RP n p hp

A TElem with p-power entries lies in RP.

theorem HeckeRing.GLn.one_mem_R_p (n : ℕ) [NeZero n] (p : ℕ) (hp : Nat.Prime p) : (TElem fun (x : Fin n) => 1) ∈ RP n p hp

The identity T(1,...,1) is in every RP (as the zero-exponent element).

Full prime factorization

theorem HeckeRing.GLn.T_elem_mem_closure_ppow (n : ℕ) [NeZero n] (a : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) (ha : DivChain n a) : TElem a ∈ Subring.closure (HeckeRing.GLn.ppowClosureSet✝ n)

Every TElem is in the subring generated by all p-local T-elements.

Generation by R_p's

theorem HeckeRing.GLn.HeckeAlgebra_generated_by_R_p (n : ℕ) [NeZero n] : ⊤ ≤ Subring.closure (HeckeRing.GLn.ppowClosureSet✝ n)

Every element of the Hecke algebra is in the subring generated by all p-local pieces.