`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

@[instance_reducible]

noncomputable def HeckeRing.GLn.localCommSemiringForInjectivity (n : ℕ) [NeZero n] :

CommSemiring (IntegralHeckeRing n)

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

PolynomialRing/Basic.lean carries the same reconstruction, but as a local instance, which does not cross the module boundary; and commSemiringIntegralHeckeRing is a sealed def, so registering it for typeclass search does not make its body reduce to the ambient NonAssocSemiring. Writing the structure here makes it transparent exactly where this file needs it, leaving the upstream definitions sealed for every other consumer.

Equations

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

Instances For

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