`pLocalSubring` is a polynomial ring for `n = 1, 2` #

The injectivity half of Shimura's Theorem 3.20 and the resulting isomorphism ℤ[X₁, …, Xₙ] ≃+* pLocalSubring, for n = 1 and n = 2. The generators and the surjectivity half are in PolynomialRing/Basic.lean.

Injectivity is proved by a determinant/leading-term argument: the determinant of a double coset representative is multiplicative, so a monomial in the generators has a predictable leading elementary-divisor vector, and distinct monomials have distinct leading terms.

Main results #

HeckeRing.GLn.evalHom_one_injective, HeckeRing.GLn.evalHom_two_injective: evaluation at the generators is injective for n = 1 and n = 2.
HeckeRing.GLn.polynomialRingEquivOne, HeckeRing.GLn.polynomialRingEquivTwo: Shimura, Theorem 3.20 for n = 1 and n = 2 — pLocalSubring ≅ ℤ[X₁, …, Xₙ].

Implementation notes #

The source states Theorem 3.20 at general n, dispatching on n = 1 and n = 2 and leaving the remaining case as a gap. Here the two proved cases are stated directly, so nothing rests on an unformalised step.

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

References #

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

source

theorem HeckeRing.GLn.evalHom_one_injective (p : ℕ) (hp : 1 < p) :

Function.Injective ⇑(evalHom 1 p)

For n = 1 and any base 1 < p, evaluation at the Hecke generator is injective.

source

theorem HeckeRing.GLn.evalHom_two_injective (p : ℕ) (hp : Nat.Prime p) :

Function.Injective ⇑(evalHom 2 p)

n=2: evalHom is injective.

source

theorem HeckeRing.GLn.evalHomLocal_injective (n : ℕ) [NeZero n] (p : ℕ) (h_inj : Function.Injective ⇑(evalHom n p)) :

Function.Injective ⇑(evalHomLocal n p)

Injectivity transfers from evalHom to its codomain restriction evalHomLocal: two polynomials with the same image in pLocalSubring have the same image in the ambient ring.

source

noncomputable def HeckeRing.GLn.polynomialRingEquivOne (p : ℕ) (hp : 1 < p) :

MvPolynomial (Fin 1) ℤ ≃+* ↥(pLocalSubring 1 p)

Shimura, Theorem 3.20 for n = 1: the p-local Hecke ring of GL₁ is the polynomial ring ℤ[X] on the single generator T(p).

Stated for 1 < p rather than p.Prime: rank one needs only that k ↦ p^k is injective.

Equations

HeckeRing.GLn.polynomialRingEquivOne p hp = RingEquiv.ofBijective (HeckeRing.GLn.evalHomLocal 1 p) ⋯

Instances For

source

@[simp]

theorem HeckeRing.GLn.polynomialRingEquivOne_apply (p : ℕ) (hp : 1 < p) (f : MvPolynomial (Fin 1) ℤ) :

(polynomialRingEquivOne p hp) f = (evalHomLocal 1 p) f

The rank-one presentation isomorphism is the evaluation map.

source

noncomputable def HeckeRing.GLn.polynomialRingEquivTwo (p : ℕ) (hp : Nat.Prime p) :

MvPolynomial (Fin 2) ℤ ≃+* ↥(pLocalSubring 2 p)

Shimura, Theorem 3.20 for n = 2: the p-local Hecke ring of GL₂ is the polynomial ring ℤ[X₁, X₂] on the generators T(1, p) and T(p, p). This is the case the classical theory of modular forms uses.

Primality is genuine here: the rank-two argument runs through the GL₂ recurrence.

Equations