Generators of the p-local Hecke ring

Towards Shimura's Theorem 3.20, that the p-local Hecke ring pLocalSubring of GL_n is a polynomial ring ℤ[X₁, …, Xₙ] on the n diagonal prime cosets. This file sets up the generators and proves the surjectivity half for n = 1 and n = 2. The injectivity half — algebraic independence of the generators — and the resulting isomorphisms live in the companion file PolynomialRing/Injective.lean, which consumes evalHom_def and evalHom_apply from here.

Main definitions

• HeckeRing.GLn.heckeGenExponent k — the exponent vector of the k-th generator's diagonal, 0 on the first n - 1 - k positions and 1 on the last k + 1.
• HeckeRing.GLn.heckeGen k — the k-th generator T(1, …, 1, p, …, p), with k + 1 entries equal to p.
• HeckeRing.GLn.evalHom — evaluation of ℤ[X₁, …, Xₙ] at the generators, into the ambient Hecke ring.
• HeckeRing.GLn.evalHomLocal — the same map with codomain pLocalSubring n p, which is the presentation map Theorem 3.20 is about.

Main results

• HeckeRing.GLn.evalHomLocal_two_surjective, HeckeRing.GLn.evalHomLocal_one_surjective: the presentation is onto, ℤ[X₁, X₂] ↠ R_p and ℤ[X₁] ↠ R_p — the surjectivity half of Theorem 3.20 at n = 2 and n = 1.
• HeckeRing.GLn.heckeGen_mem_pLocalSubring: each generator lies in pLocalSubring.
• HeckeRing.GLn.pLocalSubring_two_le_evalHom_range, HeckeRing.GLn.pLocalSubring_one_le_evalHom_range: the underlying inclusions of pLocalSubring into the range of evalHom, from which the two surjectivity statements above are read off.

Implementation notes

The roadmap records that general n needs two further steps (uniqueness of the leading double coset in the triangular expansion, and recovery of the generator exponents from the leading elementary-divisor vector); those are not formalised in the source and are not ported. Only the n = 1 and n = 2 cases below are proved, and they are the ones the classical theory consumes.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/PolynomialRing.lean, Chris Birkbeck), first three sections.

References

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

@[instance_reducible]

noncomputable def HeckeRing.GLn.commSemiringIntegralHeckeRingLocal (n : ℕ) [NeZero n] : CommSemiring (IntegralHeckeRing n)

The CommSemiring structure this module needs on IntegralHeckeRing n, rebuilt locally from the two public ingredients HeckeCosetModule.instSemiringHeckeRing and HeckeCosetModule.mul_comm_of_antiInvolution.

commSemiringIntegralHeckeRing already packages exactly this, but as a sealed def: its body does not reduce across the module boundary, so the NonAssocSemiring it carries is not definitionally the ambient one and MvPolynomial.eval₂Hom will not typecheck against it. Writing the same structure here makes its body transparent where it is needed and nowhere else, which is why the upstream definitions stay sealed rather than @[expose]d.

Equations

• HeckeRing.GLn.commSemiringIntegralHeckeRingLocal n = { toSemiring := HeckeCosetModule.instSemiringHeckeRing ℤ, mul_comm := ⋯ }

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

The exponent vector of the k-th generator's diagonal: 0 on the first n - 1 - k positions and 1 on the last k + 1, so that heckeGenDiag n p k is p raised to it entrywise (heckeGenDiag_eq_primePowDiag).

Equations

• HeckeRing.GLn.heckeGenExponent n k i = if ↑i < n - 1 - ↑k then 0 else 1

@[simp]

theorem HeckeRing.GLn.heckeGenExponent_apply (n : ℕ) (k i : Fin n) : heckeGenExponent n k i = if ↑i < n - 1 - ↑k then 0 else 1

Defining equation for the sealed definition heckeGenExponent.

def HeckeRing.GLn.heckeGenDiag (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.heckeGenDiag n p k i = if ↑i < n - 1 - ↑k then 1 else p

@[simp]

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

theorem HeckeRing.GLn.heckeGenDiag_one_eq_const (p : ℕ) : heckeGenDiag 1 p 0 = fun (x : Fin 1) => p

At n = 1 the generator diagonal is the constant p: the index condition i < 1 - 1 - 0 is never satisfied.

theorem HeckeRing.GLn.heckeGenDiag_eq_primePowDiag (n p : ℕ) (k : Fin n) : heckeGenDiag n p k = primePowDiag n p (heckeGenExponent n k)

The heckeGen diagonal has p-power entries (each entry is 1 = p^0 or p = p^1): it is p raised entrywise to heckeGenExponent n k.

theorem HeckeRing.GLn.heckeGenExponent_monotone (n : ℕ) (k : Fin n) : Monotone (heckeGenExponent n k)

The exponent function for heckeGen is monotone.

noncomputable def HeckeRing.GLn.heckeGen (n p : ℕ) (k : Fin n) : IntegralHeckeRing n

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

Equations

• HeckeRing.GLn.heckeGen n p k = HeckeRing.GLn.diagElem (HeckeRing.GLn.heckeGenDiag n p k)

theorem HeckeRing.GLn.heckeGen_def (n p : ℕ) (k : Fin n) : heckeGen n p k = diagElem (heckeGenDiag n p k)

Defining equation for the sealed definition heckeGen.

theorem HeckeRing.GLn.heckeGen_mem_pLocalSubring (n p : ℕ) [NeZero n] (k : Fin n) : heckeGen n p k ∈ pLocalSubring n p

Each generator lies in the p-local subsemiring R_p.

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

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

Equations

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

theorem HeckeRing.GLn.evalHom_def (n : ℕ) [NeZero n] (p : ℕ) : evalHom n p = MvPolynomial.eval₂Hom (Int.castRingHom (IntegralHeckeRing n)) fun (k : Fin n) => heckeGen n p k

Defining equation for the sealed definition evalHom: evaluation of a polynomial at the generators, with integer coefficients cast into the Hecke ring.

@[simp]

theorem HeckeRing.GLn.evalHom_X (n : ℕ) [NeZero n] (p : ℕ) (k : Fin n) : (evalHom n p) (MvPolynomial.X k) = heckeGen n p k

evalHom sends the k-th variable to the k-th generator.

theorem HeckeRing.GLn.evalHom_C (n : ℕ) [NeZero n] (p : ℕ) (a : ℤ) : (evalHom n p) (MvPolynomial.C a) = ↑a

evalHom sends a constant to its image under ℤ → IntegralHeckeRing n.

Deliberately not @[simp]: simp already discharges this through eq_intCast and map_intCast, evalHom being a ring hom, and simpNF rejects the redundant marking. The lemma is kept as the named computation rule for rw.

theorem HeckeRing.GLn.evalHom_apply (n : ℕ) [NeZero n] (p : ℕ) (P : MvPolynomial (Fin n) ℤ) (D : HeckeCoset (posDetInt n) (SLnZ n) (SLnZ n)) : ((evalHom n p) P) D = ∑ d ∈ P.support, P.coeff d • (∏ i : Fin n, heckeGen n p i ^ d i) D

Evaluation rule for evalHom at a double coset. The coefficient of evalHom P at D is the sum, over the support of P, of P.coeff d times the coefficient of the monomial ∏ heckeGen i ^ d i at D.

This is the wrapper-level counterpart of evalHom_def: it is stated here, where evalHom and IntegralHeckeRing are both transparent, so that consumers can evaluate a polynomial image at a coset without depending on either definition reducing at their own use site.

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

Each heckeGen k lies in the range of evalHom.

theorem HeckeRing.GLn.evalHom_mem_pLocalSubring (n : ℕ) [NeZero n] (p : ℕ) (f : MvPolynomial (Fin n) ℤ) : (evalHom n p) f ∈ pLocalSubring n p

Every value of evalHom lies in R_p: the generators do, and pLocalSubring is a subring, so it absorbs the constants, sums and products that build an arbitrary polynomial.

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

The evaluation homomorphism with its true codomain: ℤ[X₁, …, Xₙ] →+* R_p.

evalHom lands in the ambient Hecke ring, which makes the results below mere inclusions; this is the map whose surjectivity is the presentation statement of Theorem 3.20.

Equations

• HeckeRing.GLn.evalHomLocal n p = (HeckeRing.GLn.evalHom n p).codRestrict (HeckeRing.GLn.pLocalSubring n p) ⋯

@[simp]

theorem HeckeRing.GLn.evalHomLocal_coe (n : ℕ) [NeZero n] (p : ℕ) (f : MvPolynomial (Fin n) ℤ) : ↑((evalHomLocal n p) f) = (evalHom n p) f

@[simp]

theorem HeckeRing.GLn.evalHomLocal_X (n : ℕ) [NeZero n] (p : ℕ) (k : Fin n) : (evalHomLocal n p) (MvPolynomial.X k) = ⟨heckeGen n p k, ⋯⟩

The computation rule of the presentation map: the k-th variable goes to the k-th generator, taken in pLocalSubring rather than in the ambient ring.

theorem HeckeRing.GLn.heckeGen_zero_eq_heckeTDiag (p : ℕ) (hp : 0 < p) : heckeGen 2 p 0 = GL2.heckeTDiag 1 p

heckeGen 2 p 0 = heckeTDiag 1 p: the first generator is T(1,p).

Positivity, not primality: nothing here needs p prime.

theorem HeckeRing.GLn.heckeGen_one_eq_heckeTScalar (p : ℕ) (hp : 0 < p) : heckeGen 2 p 1 = GL2.heckeTScalar p

heckeGen 2 p 1 = heckeTScalar p: the second generator is the diamond operator.

Positivity, not primality, for the same reason as heckeGen_zero_eq_heckeTDiag.

theorem HeckeRing.GLn.heckeT_prime_eq_heckeGen_zero (p : ℕ) (hp : Nat.Prime p) : GL2.heckeT ⟨p, ⋯⟩ = heckeGen 2 p 0

heckeT(p) = heckeGen 0: the sum T(p) is the first generator for p prime.

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

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

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

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

theorem HeckeRing.GLn.diagElem_primePowDiag_mem_evalHom_range (p : ℕ) (hp : Nat.Prime p) (e : Fin 2 → ℕ) (hmono : Monotone e) : diagElem (primePowDiag 2 p e) ∈ (evalHom 2 p).range

diagElem (primePowDiag 2 p e) is in the evalHom range when e is monotone.

theorem HeckeRing.GLn.pLocalSubring_two_le_evalHom_range (p : ℕ) (hp : Nat.Prime p) : pLocalSubring 2 p ≤ (evalHom 2 p).range

Surjectivity of evalHom at n = 2: pLocalSubring 2 p lies in the range of the evaluation homomorphism ℤ[X₁, X₂] → IntegralHeckeRing 2. Together with heckeGen_mem_pLocalSubring for the reverse inclusion, the two generators T(1, p) and T(p, p) therefore generate the whole p-local Hecke ring of GL₂.

theorem HeckeRing.GLn.pLocalSubring_one_le_evalHom_range (p : ℕ) (hp : 0 < p) : pLocalSubring 1 p ≤ (evalHom 1 p).range

Surjectivity of evalHom at n = 1: pLocalSubring 1 p lies in the range of evalHom. The p-local Hecke ring of GL₁ is generated by the single element T(p).

theorem HeckeRing.GLn.evalHomLocal_two_surjective (p : ℕ) (hp : Nat.Prime p) : Function.Surjective ⇑(evalHomLocal 2 p)

The presentation is onto at n = 2: ℤ[X₁, X₂] ↠ R_p, the surjectivity half of Shimura's Theorem 3.20. This is the inclusion above read through evalHomLocal, whose codomain is R_p itself.

theorem HeckeRing.GLn.evalHomLocal_one_surjective (p : ℕ) (hp : 0 < p) : Function.Surjective ⇑(evalHomLocal 1 p)

The presentation is onto at n = 1: ℤ[X₁] ↠ R_p.