Prime decomposition of diagonal Hecke operators

The p-adic decomposition of the diagonal Hecke operators: every T(a₁,...,aₙ) with entrywise nonzero a splits off its p-power part, T(a) = T(p-part) · T(p-free part), by the coprime product theorem. Nonvanishing is what is required throughout — it is all Nat.factorization and ordCompl ask for, and it is exactly what keeps natDiagGL off its junk value, which it takes on a tuple with a zero entry.

The p-power operators whose exponent vector is monotone generate the p-local Hecke subring R_p (Shimura's R_p). For 1 < p, monotonicity is exactly what makes the exponent vector a divisibility chain, hence a canonical diagonal. p itself is left unrestricted, so the definition carries no hypothesis, and the two degenerate values fail that reading in opposite ways: at p = 0 a positive exponent gives 0 ^ e i = 0, so the generator is natDiagGL's junk value rather than a coset, while at p = 1 every exponent vector gives the constant-one chain, so monotonicity is not necessary. In practice p is prime.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/PrimeDecomposition.lean, Chris Birkbeck).

Main definitions

• HeckeRing.GLn.primePowDiag: the p-power diagonal i ↦ p ^ e i.
• HeckeRing.GLn.diagFactorizationAt: the entrywise p-adic valuation of a diagonal — the full Nat.factorization evaluated at the single prime p in each coordinate, hence the At suffix; it is a Fin n → ℕ, not a finitely supported factorization.
• HeckeRing.GLn.diagOrdCompl: the entrywise p-free part of a diagonal, i.e. ordCompl[p] applied in each coordinate.
• HeckeRing.GLn.pLocalSubring: the p-local Hecke subring R_p.

Main results

• HeckeRing.GLn.diagElem_eq_primePowDiag_mul_diagOrdCompl: T(a) = T(p-part) · T(p-free part).

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.2.

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

The p-power diagonal: entries are p ^ e i.

Equations

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

@[simp]

theorem HeckeRing.GLn.primePowDiag_apply (n p : ℕ) (e : Fin n → ℕ) (i : Fin n) : primePowDiag n p e i = p ^ e i

Defining equation for the sealed definition primePowDiag.

theorem HeckeRing.GLn.primePowDiag_pos (n p : ℕ) (hp : 0 < p) (e : Fin n → ℕ) (i : Fin n) : 0 < primePowDiag n p e i

Every entry of a p-power diagonal is positive when p is.

@[simp]

theorem HeckeRing.GLn.primePowDiag_add (n p : ℕ) (e f : Fin n → ℕ) : primePowDiag n p (e + f) = primePowDiag n p e * primePowDiag n p f

The p-power diagonal turns a sum of exponent vectors into the entrywise product.

theorem HeckeRing.GLn.isDvdChain_primePowDiag (n p : ℕ) (e : Fin n → ℕ) (hmono : Monotone e) : IsDvdChain (primePowDiag n p e)

Monotone exponents give a divisibility chain of p-power diagonals.

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

The entrywise p-adic valuation of a diagonal.

Equations

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

@[simp]

theorem HeckeRing.GLn.diagFactorizationAt_apply (n p : ℕ) (a : Fin n → ℕ) (i : Fin n) : diagFactorizationAt n p a i = (a i).factorization p

Defining equation for the sealed diagFactorizationAt.

theorem HeckeRing.GLn.diagFactorizationAt_monotone (n : ℕ) (a : Fin n → ℕ) (ha_ne : ∀ (i : Fin n), a i ≠ 0) (ha : IsDvdChain a) (p : ℕ) : Monotone (diagFactorizationAt n p a)

The p-component of a divisibility chain is monotone.

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

The entrywise p-free part of a diagonal: a i ↦ a i / p ^ (v_p (a i)).

Equations

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

@[simp]

theorem HeckeRing.GLn.diagOrdCompl_apply (n p : ℕ) (a : Fin n → ℕ) (i : Fin n) : diagOrdCompl n p a i = a i / p ^ (a i).factorization p

Defining equation for the sealed diagOrdCompl.

theorem HeckeRing.GLn.diagOrdCompl_pos (n p : ℕ) (a : Fin n → ℕ) (ha_ne : ∀ (i : Fin n), a i ≠ 0) (i : Fin n) : 0 < diagOrdCompl n p a i

Removing the p-part preserves positivity of every entry.

theorem HeckeRing.GLn.isDvdChain_diagOrdCompl (n p : ℕ) (a : Fin n → ℕ) (ha : IsDvdChain a) : IsDvdChain (diagOrdCompl n p a)

The p-free part preserves divisibility chains.

@[simp]

theorem HeckeRing.GLn.primePowDiag_mul_diagOrdCompl (n p : ℕ) (a : Fin n → ℕ) : primePowDiag n p (diagFactorizationAt n p a) * diagOrdCompl n p a = a

The pointwise product of the p-part and the p-free part recovers the diagonal.

theorem HeckeRing.GLn.coprime_prod_primePowDiag_diagOrdCompl (n p : ℕ) (hp : Nat.Prime p) (a : Fin n → ℕ) (ha_ne : ∀ (i : Fin n), a i ≠ 0) : (∏ i : Fin n, primePowDiag n p (diagFactorizationAt n p a) i).Coprime (∏ i : Fin n, diagOrdCompl n p a i)

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

theorem HeckeRing.GLn.diagElem_eq_primePowDiag_mul_diagOrdCompl (n : ℕ) [NeZero n] (a : Fin n → ℕ) (ha_ne : ∀ (i : Fin n), a i ≠ 0) (p : ℕ) (hp : Nat.Prime p) : diagElem a = diagElem (primePowDiag n p (diagFactorizationAt n p a)) * diagElem (diagOrdCompl n p a)

Binary prime splitting (Shimura, §3.2): every diagonal Hecke operator with entrywise nonzero entries factors into its p-power component and its p-free component, for any prime p. The hypothesis is essential, not cosmetic: on a tuple with a zero entry natDiagGL takes its junk value and the two factors need not multiply back to T(a). Callers holding positivity discharge it with .ne'.

noncomputable def HeckeRing.GLn.pLocalSubring (n : ℕ) [NeZero n] (p : ℕ) : Subring (IntegralHeckeRing n)

The p-local Hecke subring R_p: generated by the diagonal Hecke operators T(p^e₁,...,p^eₙ) whose exponent vector e is monotone (Shimura's R_p). Monotonicity is part of the generating set, not an afterthought: for 1 < p it is exactly the condition making the entries a divisibility chain, so each generator names a canonical double coset.

p is unrestricted, so no hypothesis is needed to form the subring, but that canonical-double-coset reading needs 1 < p (in practice p prime). At p = 0 a positive exponent gives a zero entry, so the generator is natDiagGL's junk value rather than a diagonal coset; at p = 1 every exponent vector gives the constant-one chain, so monotonicity is not necessary.

Equations

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

theorem HeckeRing.GLn.pLocalSubring_def (n : ℕ) [NeZero n] (p : ℕ) : pLocalSubring n p = Subring.closure {f : IntegralHeckeRing n | ∃ (e : Fin n → ℕ) (_ : Monotone e), f = diagElem (primePowDiag n p e)}

Defining equation for the sealed definition pLocalSubring.

@[simp]

theorem HeckeRing.GLn.diagElem_primePowDiag_mem_pLocalSubring (n : ℕ) [NeZero n] (p : ℕ) (e : Fin n → ℕ) (hmono : Monotone e) : diagElem (primePowDiag n p e) ∈ pLocalSubring n p

A diagonal Hecke operator with p-power entries lies in R_p, provided its exponent vector is monotone — that is the generating set of pLocalSubring.

@[simp]

theorem HeckeRing.GLn.pLocalSubring_le_iff (n : ℕ) [NeZero n] (p : ℕ) (S : Subring (IntegralHeckeRing n)) : pLocalSubring n p ≤ S ↔ ∀ (e : Fin n → ℕ), Monotone e → diagElem (primePowDiag n p e) ∈ S

The universal property of R_p: a subring contains R_p exactly when it contains every monotone p-power generator. This is the elimination form — pLocalSubring is a Subring.closure, so proving a map or an inclusion out of it should go through this rather than unfolding the closure and manipulating the generating set by hand.