Hecke Ring
Results named in Tau Ceti's TauCeti.NumberTheory.HeckeRing modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremThe generators generate R_p (Shimura, Theorem 3.20)#
for p prime, the polynomials in
the generators heckeGen k are exactly the elements of the p-local Hecke ring.
HeckeRing.GLn.range_evalHom (n : ℕ) [NeZero n] {p : ℕ} (hp : Nat.Prime p) :
(HeckeRing.GLn.evalHom n p).range = HeckeRing.GLn.pLocalSubring n p
TheoremThe prime-power degree (Shimura, Theorem 3.24, degree count)#
for prime p and
k ≥ 1, a divisibility chain a of ratio a₁ / a₀ = pᵏ has deg T(a₀, a₁) = pᵏ⁻¹ (p + 1).
The archetype is a = (pⁱ, pⁱ⁺ᵏ).
HeckeRing.GL2.degree_diagCoset_of_ratio_eq_prime_pow (p : ℕ) (hp : Nat.Prime p) (a : Fin 2 → ℕ)
(hdiv : HeckeRing.GLn.IsDvdChain a) (k : ℕ) (hk : 0 < k) (h_ratio : a 1 / a 0 = p ^ k) :
(HeckeRing.GLn.diagCoset a).degree = p ^ (k - 1) * (p + 1)
Lean
Formalized in Tau Ceti as HeckeRing.GL2.degree_diagCoset_of_ratio_eq_prime_pow.
Sources
TheoremShimura's commutativity criterion (Proposition 3.8 of [Shimura][shimura1971])#
the Hecke ring over a commutative semiring is commutative when an anti-involution fixes every double coset.
HeckeCosetModule.mul_comm_of_antiInvolution.{u_1, u_2} {G : Type u_1} [Group G] (R : Type u_2)
{Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] [CommSemiring R]
(ι : HeckeAntiInvolution Δ H) (h_fix : ∀ (D : HeckeCoset Δ H H), ι.onHeckeCoset D = D)
(f g : HeckeRing Δ H R) : f * g = g * f
Used by 7
U_p at every prime p dividing the level, with eigenvalue a_p(f) · HeckeRing.GL2.Newform.L_eulerProduct · The Atkin–Li pseudo-eigenvalue · The coefficient field of a newform of weight at least two is a number field · The generators generate R_p (Shimura, Theorem 3.20) · Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3) · Strong multiplicity one (Miyake, Theorem 4.6.12, fixed level)TheoremShimura's covering identity for a product of double cosets (§3.4)#
If Γ₁ δ₁ Γ₂ is the
union of the right cosets Γ₁ aᵢ and Γ₂ δ₂ Γ₃ is the union of the right cosets Γ₂ bⱼ, then
the pointwise product Γ₁ δ₁ Γ₂ · Γ₂ δ₂ Γ₃ is the union of the right cosets Γ₁ aᵢ bⱼ.
The two double cosets splice because Γ₂ Γ₂ = Γ₂: an element of the product is u v with
u ∈ Γ₁ δ₁ Γ₂ and v ∈ Γ₂ δ₂ Γ₃; writing v = g bⱼ with g ∈ Γ₂ moves g into u, and u g
is again in Γ₁ δ₁ Γ₂, hence in some Γ₁ aᵢ.
⚠ The union is not disjoint, and the family (i, j) ↦ Γ₁ aᵢ bⱼ is in general far from
injective. Any repetitions here are right-coset collisions; this theorem neither counts them nor
identifies them with DoubleCoset.multiplicity, which uses left-coset representatives. The
identity supplies coverage only, exactly as
doubleCoset_eq_iUnion_rightCosets_of_forall_exists does for a single double coset.
DoubleCoset.doubleCoset_mul_doubleCoset_eq_iUnion_rightCosets.{u_1, u_2, u_3} {G : Type u_1}
[Group G] {Γ₁ Γ₂ Γ₃ : Subgroup G} {δ₁ δ₂ : G} {ι : Type u_2} {κ : Type u_3} (a : ι → G)
(b : κ → G) (hcover₁ : DoubleCoset.doubleCoset δ₁ ↑Γ₁ ↑Γ₂ = ⋃ i, MulOpposite.op (a i) • ↑Γ₁)
(hcover₂ : DoubleCoset.doubleCoset δ₂ ↑Γ₂ ↑Γ₃ = ⋃ j, MulOpposite.op (b j) • ↑Γ₂) :
DoubleCoset.doubleCoset δ₁ ↑Γ₁ ↑Γ₂ * DoubleCoset.doubleCoset δ₂ ↑Γ₂ ↑Γ₃ =
⋃ p, MulOpposite.op (a p.1 * b p.2) • ↑Γ₁
Lean
Formalized in Tau Ceti as DoubleCoset.doubleCoset_mul_doubleCoset_eq_iUnion_rightCosets.
Sources
TheoremShimura's decomposition of a double coset into right cosets#
Γ₁gΓ₂ is the union of the
right cosets Γ₁ · (g τᵥ⁻¹), where τᵥ runs over representatives of Γ₂ ⧸ (Γ₂ ∩ g⁻¹Γ₁g) — the
mirror of DoubleCoset.doubleCoset_eq_iUnion_leftCosets, and of Mathlib's
doubleCoset_union_rightCoset, which is indexed by all of Γ₂ and so repeats each coset.
The inverse on τᵥ is what converts the left-coset quotient Γ₂ ⧸ (Γ₂ ∩ g⁻¹Γ₁g) into an index
for the right cosets: Γ₁ g τ = Γ₁ g τ' exactly when τ'τ⁻¹ ∈ Γ₂ ∩ g⁻¹Γ₁g.
It lives here rather than beside doubleCoset_eq_iUnion_leftCosets because it is phrased with
DecompQuotient, which this file defines.
DoubleCoset.doubleCoset_eq_iUnion_rightCosets.{u_1} {G : Type u_1} [Group G] (Γ₁ Γ₂ : Subgroup G)
(g : G) :
DoubleCoset.doubleCoset g ↑Γ₁ ↑Γ₂ = ⋃ v, MulOpposite.op (g * (↑(Quotient.out v))⁻¹) • ↑Γ₁
Lean
Formalized in Tau Ceti as DoubleCoset.doubleCoset_eq_iUnion_rightCosets.
Other forms
Shimura's decomposition of the double coset, in the rightCosetRep spelling. Formalized in Tau Ceti as DoubleCoset.doubleCoset_eq_iUnion_rightCosetRep.
DoubleCoset.doubleCoset_eq_iUnion_rightCosetRep.{u_1} {G : Type u_1} [Group G] {Δ : Submonoid G}
{Γ₁ Γ₂ : Subgroup G} (D : HeckeCoset Δ Γ₁ Γ₂) :
DoubleCoset.doubleCoset ↑(Quotient.out D) ↑Γ₁ ↑Γ₂ =
⋃ v, MulOpposite.op (DoubleCoset.rightCosetRep D v) • ↑Γ₁
Sources
Used by 8
U_p at every prime p dividing the level, with eigenvalue a_p(f) · HeckeRing.GL2.Newform.L_eulerProduct · The Atkin–Li pseudo-eigenvalue · The coefficient field of a newform of weight at least two is a number field · The Main Lemma, per character (Miyake, Lemma 4.6.8; Diamond–Shurman, Theorem 5.7.1) · Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3) · Strong multiplicity one (Miyake, Theorem 4.6.12, fixed level) · The Petersson adjoint formula in the second argumentLoading dependency explorer…
The dependency explorer needs JavaScript and its graph data.