Skip to content

Commit 32ea179

Browse files
CBirkbeckCBirkbeck
committed
feat(NumberTheory): the abstract Hecke ring of a Hecke pair (#41251)
The definitions underlying abstract Hecke rings: - `IsHeckeTriple Δ H₁ H₂`: compatibility conditions on a submonoid `Δ` and two subgroups. - `HeckeCoset Δ H₁ H₂`: the double cosets `H₁\Δ/H₂`. - `HeckeCosetModule Δ H₁ H₂ Z`: their finitely-supported `Z`-linear combinations; `𝕋 Δ H Z` is the diagonal Hecke ring. The convolution product and ring structure come in later PRs. Co-Authored-By: Claude Opus 4.8
1 parent 1c3e8f3 commit 32ea179

3 files changed

Lines changed: 257 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5743,6 +5743,7 @@ public import Mathlib.NumberTheory.Harmonic.EulerMascheroni
57435743
public import Mathlib.NumberTheory.Harmonic.GammaDeriv
57445744
public import Mathlib.NumberTheory.Harmonic.Int
57455745
public import Mathlib.NumberTheory.Harmonic.ZetaAsymp
5746+
public import Mathlib.NumberTheory.HeckeRing.Defs
57465747
public import Mathlib.NumberTheory.Height.Basic
57475748
public import Mathlib.NumberTheory.Height.EllipticCurve
57485749
public import Mathlib.NumberTheory.Height.MvPolynomial

‎Mathlib/NumberTheory/HeckeRing/Defs.lean‎

Lines changed: 227 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,227 @@
1+
/-
2+
Copyright (c) 2026 Chris Birkbeck. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Chris Birkbeck
5+
-/
6+
module
7+
8+
public import Mathlib.Algebra.Group.Finsupp
9+
public import Mathlib.GroupTheory.Commensurable
10+
public import Mathlib.GroupTheory.DoubleCoset
11+
12+
/-!
13+
# Hecke rings: definitions
14+
15+
This file introduces the abstract Hecke ring of a *Hecke pair* `(H, Δ)` and, more generally, the
16+
Hecke coset modules attached to a triple `(H₁, Δ, H₂)`, following [Shimura][shimura1971],
17+
Chapter 3, and [Krieg][krieg1990], Chapter I. It sets up the underlying types: the compatibility
18+
conditions `IsHeckeTriple Δ H₁ H₂` on a submonoid `Δ` of a group `G` and a pair of subgroups
19+
of `G`, the double-coset quotient `HeckeCoset Δ H₁ H₂` of `Δ` by `H₁gH₂ = H₁hH₂`, and the Hecke
20+
coset module `HeckeCosetModule Δ H₁ H₂ Z` of formal finitely-supported linear combinations of
21+
double cosets.
22+
The convolution product `HeckeCosetModule Δ H₁ H₂ Z × HeckeCosetModule Δ H₂ H₃ Z →
23+
HeckeCosetModule Δ H₁ H₃ Z` and the ring structure on the diagonal Hecke ring `𝕋 Δ H Z` are
24+
developed in later files.
25+
26+
The relevance of the submonoid `Δ` may not be immediately obvious; a natural example is
27+
`H = GL₂(ℤ)` inside `G = GL₂(ℚ)` with `Δ` the submonoid of integral matrices with nonzero
28+
determinant, which is the Hecke pair underlying the classical Hecke operators `T_n`. Mixed
29+
subgroups `H₁ ≠ H₂` arise for Hecke operators between different levels, e.g. `H₁ = Γ₀(N)` and
30+
`H₂ = Γ₀(M)` inside the same `Δ`.
31+
32+
## Main definitions
33+
34+
* `IsHeckeTriple Δ H₁ H₂`: `(H₁, Δ, H₂)` is a Hecke triple, i.e. `H₁ ≤ Δ`, `H₂ ≤ Δ`,
35+
`Commensurable H₁ H₂` and `Δ ≤ commensurator H₂`, making the double cosets `H₁\Δ/H₂` finite
36+
unions of left cosets. The classical Hecke pair `(H, Δ)` is the diagonal case
37+
`IsHeckeTriple Δ H H`.
38+
* `HeckeCoset Δ H₁ H₂`: the quotient of `Δ` by the relation `H₁gH₂ = H₁hH₂`, i.e. the double
39+
cosets `H₁\Δ/H₂` forming the basis of the Hecke coset module.
40+
* `HeckeCosetModule Δ H₁ H₂ Z`: the Hecke coset module with coefficients in `Z`, the
41+
finitely-supported `Z`-linear combinations of double cosets.
42+
* `HeckeRing Δ H Z`, notation `𝕋 Δ H Z`: the Hecke ring, the diagonal case
43+
`HeckeCosetModule Δ H H Z` of the Hecke coset module.
44+
45+
## Implementation notes
46+
47+
The data `(Δ, H₁, H₂)` enters unbundled, with the compatibility conditions collected in the
48+
Prop-valued class `IsHeckeTriple`: the types `HeckeCoset Δ H₁ H₂` and `HeckeCosetModule Δ H₁ H₂ Z`
49+
are built from the data alone and depend on no proofs, and a single ambient `Δ` shared by all
50+
levels
51+
(as in [Shimura][shimura1971]) means products of double cosets over different subgroups,
52+
`H₁g₁H₂ * H₂g₂H₃ ⊆ Δ`, need no compatibility hypotheses. The conditions are only needed for the
53+
finiteness of the coset decompositions, which enters through the `Fintype` instance on
54+
`DoubleCoset.DecompQuotient` in later files. Requiring `Δ` to be a submonoid rather than a
55+
subsemigroup loses no generality, since `H₁ ≤ Δ` already forces `1 ∈ Δ`.
56+
57+
## References
58+
59+
* [G. Shimura, *Introduction to the arithmetic theory of automorphic functions*][shimura1971]
60+
* [A. Krieg, *Hecke algebras*][krieg1990]
61+
-/
62+
63+
@[expose] public section
64+
65+
open Subgroup Subgroup.Commensurable
66+
open scoped Pointwise
67+
68+
variable {G : Type*} [Group G]
69+
70+
/-- A *Hecke triple* `(H₁, Δ, H₂)`: the compatibility conditions on a submonoid `Δ` and a pair
71+
of subgroups `H₁, H₂` of `G` making the double cosets `H₁\Δ/H₂` finite unions of left cosets:
72+
both subgroups are contained in `Δ`, they are commensurable, and `Δ` commensurates them. The
73+
classical Hecke pair `(H, Δ)` of [Shimura][shimura1971], Chapter 3, is the diagonal case
74+
`IsHeckeTriple Δ H H`. -/
75+
class IsHeckeTriple (Δ : Submonoid G) (H₁ H₂ : Subgroup G) : Prop where
76+
/-- The left subgroup is contained in `Δ`. -/
77+
left_le : H₁.toSubmonoid ≤ Δ
78+
/-- The right subgroup is contained in `Δ`. -/
79+
right_le : H₂.toSubmonoid ≤ Δ
80+
/-- The two subgroups are commensurable. -/
81+
commensurable : Commensurable H₁ H₂
82+
/-- The submonoid `Δ` lies in the commensurator of the right subgroup (hence, the subgroups
83+
being commensurable, also in that of the left one; see `le_commensurator_left`). -/
84+
le_commensurator_right : Δ ≤ (commensurator H₂).toSubmonoid
85+
86+
namespace IsHeckeTriple
87+
88+
variable {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G}
89+
90+
/-- The Hecke triple `(H, Δ, H)` coming from a pair `(H, Δ)` with `H ≤ Δ ≤ commensurator H`. -/
91+
theorem of_diagonal {H : Subgroup G} (h : H.toSubmonoid ≤ Δ)
92+
(hc : Δ ≤ (commensurator H).toSubmonoid) : IsHeckeTriple Δ H H :=
93+
⟨h, h, .refl H, hc⟩
94+
95+
/-- Elements of the left subgroup lie in `Δ`. -/
96+
theorem mem_of_mem_left (H₂ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] {x : G} (hx : x ∈ H₁) : x ∈ Δ :=
97+
left_le H₂ hx
98+
99+
/-- Elements of the right subgroup lie in `Δ`. -/
100+
theorem mem_of_mem_right (H₁ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] {x : G} (hx : x ∈ H₂) : x ∈ Δ :=
101+
right_le H₁ hx
102+
103+
/-- The submonoid `Δ` lies in the commensurator of the left subgroup. -/
104+
theorem le_commensurator_left (H₂ : Subgroup G) [h : IsHeckeTriple Δ H₁ H₂] :
105+
Δ ≤ (commensurator H₁).toSubmonoid := by
106+
rw [h.commensurable.eq]
107+
exact h.le_commensurator_right
108+
109+
/-- Elements of `Δ` lie in the commensurator of the right subgroup. -/
110+
theorem mem_commensurator_right (H₁ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] (g : Δ) :
111+
(g : G) ∈ commensurator H₂ :=
112+
le_commensurator_right H₁ g.2
113+
114+
/-- Elements of `Δ` lie in the commensurator of the left subgroup. -/
115+
theorem mem_commensurator_left (H₂ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] (g : Δ) :
116+
(g : G) ∈ commensurator H₁ :=
117+
le_commensurator_left H₂ g.2
118+
119+
/-- Conjugating the right subgroup of a Hecke triple `(H₁, Δ, H₂)` by an element of `Δ` gives a
120+
subgroup commensurable with the left one. -/
121+
theorem commensurable_conjAct_right [IsHeckeTriple Δ H₁ H₂] (g : Δ) :
122+
Commensurable (ConjAct.toConjAct (g : G) • H₂) H₁ := by
123+
have hg : Commensurable (ConjAct.toConjAct (g : G) • H₂) H₂ := mem_commensurator_right H₁ g
124+
exact hg.trans (commensurable (Δ := Δ)).symm
125+
126+
/-- Hecke coset module data compose. Not an instance, since the middle subgroup cannot be
127+
inferred from the goal. -/
128+
theorem trans [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₃] :
129+
IsHeckeTriple Δ H₁ H₃ :=
130+
⟨left_le H₂, right_le H₂,
131+
(commensurable (Δ := Δ) (H₁ := H₁) (H₂ := H₂)).trans
132+
(commensurable (Δ := Δ) (H₁ := H₂) (H₂ := H₃)),
133+
le_commensurator_right H₂⟩
134+
135+
/-- The left diagonal datum `(H₁, Δ, H₁)`. Not an instance, since `H₂` cannot be inferred. -/
136+
theorem diag_left [IsHeckeTriple Δ H₁ H₂] : IsHeckeTriple Δ H₁ H₁ :=
137+
⟨left_le H₂, left_le H₂, .refl H₁, le_commensurator_left H₂⟩
138+
139+
/-- The right diagonal datum `(H₂, Δ, H₂)`. Not an instance, since `H₁` cannot be inferred. -/
140+
theorem diag_right [IsHeckeTriple Δ H₁ H₂] : IsHeckeTriple Δ H₂ H₂ :=
141+
⟨right_le H₁, right_le H₁, .refl H₂, le_commensurator_right H₁⟩
142+
143+
end IsHeckeTriple
144+
145+
/-- The setoid on `Δ` identifying elements with the same double coset `H₁gH₂ = H₁hH₂`, pulled
146+
back from `DoubleCoset.setoid` along the inclusion `Δ ↪ G`.
147+
148+
This is an `abbrev` rather than a global instance: the subgroups `H₁, H₂` cannot be inferred
149+
from the submonoid `Δ`, so this cannot participate in instance search (and a global instance
150+
would also create a `Setoid` diamond on `↥Δ` with the left-coset setoid). The quotient map is
151+
`HeckeCoset.mk`. -/
152+
abbrev HeckeCoset.setoid (Δ : Submonoid G) (H₁ H₂ : Subgroup G) : Setoid Δ :=
153+
(DoubleCoset.setoid (H₁ : Set G) H₂).comap Subtype.val
154+
155+
/-- A Hecke double coset: an equivalence class of `Δ`-elements under `H₁gH₂ = H₁hH₂`. This is
156+
the basis type for the `HeckeCosetModule`. -/
157+
def HeckeCoset (Δ : Submonoid G) (H₁ H₂ : Subgroup G) := Quotient (HeckeCoset.setoid Δ H₁ H₂)
158+
159+
namespace HeckeCoset
160+
161+
variable {Δ : Submonoid G}
162+
163+
/-- The double coset `H₁gH₂` of an element `g : Δ`. -/
164+
def mk (H₁ H₂ : Subgroup G) (g : Δ) : HeckeCoset Δ H₁ H₂ :=
165+
Quotient.mk (setoid Δ H₁ H₂) g
166+
167+
variable (Δ) in
168+
instance (H₁ H₂ : Subgroup G) : Inhabited (HeckeCoset Δ H₁ H₂) := ⟨mk H₁ H₂ ⟨1, Δ.one_mem⟩⟩
169+
170+
variable (Δ) in
171+
/-- The identity double coset `H1H = H` of the diagonal (Hecke pair) case. -/
172+
instance (H : Subgroup G) : One (HeckeCoset Δ H H) := ⟨mk H H ⟨1, Δ.one_mem⟩⟩
173+
174+
lemma one_def (H : Subgroup G) : (1 : HeckeCoset Δ H H) = mk H H ⟨1, Δ.one_mem⟩ := rfl
175+
176+
end HeckeCoset
177+
178+
/-- The Hecke coset module with coefficients in `Z`: the finitely-supported `Z`-linear
179+
combinations of double cosets `H₁\Δ/H₂`. For `H₁ = H₂` this is the underlying module of the
180+
Hecke ring `𝕋 Δ H Z` (see `HeckeRing`). The coefficients `Z` need only carry a `Zero` for the
181+
type to make sense; algebraic structure is added by the instances below at the weakest level each
182+
requires. -/
183+
def HeckeCosetModule (Δ : Submonoid G) (H₁ H₂ : Subgroup G) (Z : Type*) [Zero Z] :=
184+
HeckeCoset Δ H₁ H₂ →₀ Z
185+
186+
/-- The Hecke ring `𝕋 Δ H Z` with coefficients in `Z`: the diagonal Hecke coset module
187+
`HeckeCosetModule Δ H H Z`, the finitely-supported `Z`-linear combinations of double cosets
188+
`H\Δ/H`. The convolution product making it a ring is developed in later files. -/
189+
abbrev HeckeRing (Δ : Submonoid G) (H : Subgroup G) (Z : Type*) [Zero Z] :=
190+
HeckeCosetModule Δ H H Z
191+
192+
@[inherit_doc]
193+
scoped[HeckeCosetModule] notation "𝕋" => HeckeRing
194+
195+
namespace HeckeCosetModule
196+
197+
variable (Δ : Submonoid G) (H₁ H₂ : Subgroup G) (Z : Type*)
198+
199+
/-- Elements of `HeckeCosetModule Δ H₁ H₂ Z` are functions `HeckeCoset Δ H₁ H₂ → Z` (finitely
200+
supported). -/
201+
instance [Zero Z] : FunLike (HeckeCosetModule Δ H₁ H₂ Z) (HeckeCoset Δ H₁ H₂) Z :=
202+
inferInstanceAs (FunLike (HeckeCoset Δ H₁ H₂ →₀ Z) (HeckeCoset Δ H₁ H₂) Z)
203+
204+
noncomputable instance [AddCommMonoid Z] : AddCommMonoid (HeckeCosetModule Δ H₁ H₂ Z) :=
205+
inferInstanceAs (AddCommMonoid (HeckeCoset Δ H₁ H₂ →₀ Z))
206+
207+
noncomputable instance [AddCommGroup Z] : AddCommGroup (HeckeCosetModule Δ H₁ H₂ Z) :=
208+
inferInstanceAs (AddCommGroup (HeckeCoset Δ H₁ H₂ →₀ Z))
209+
210+
/-- The sanctioned constructor of `HeckeCosetModule Δ H₁ H₂ Z` from a finitely-supported function
211+
on double cosets. Build elements through `of` rather than relying on the definitional unfolding
212+
`HeckeCosetModule Δ H₁ H₂ Z = (HeckeCoset Δ H₁ H₂ →₀ Z)`. -/
213+
def of {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type*} [Zero Z] :
214+
(HeckeCoset Δ H₁ H₂ →₀ Z) ≃ HeckeCosetModule Δ H₁ H₂ Z :=
215+
Equiv.refl _
216+
217+
@[simp]
218+
lemma of_apply {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type*} [Zero Z]
219+
(f : HeckeCoset Δ H₁ H₂ →₀ Z) (D : HeckeCoset Δ H₁ H₂) : of f D = f D :=
220+
rfl
221+
222+
@[ext]
223+
lemma ext {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type*} [Zero Z]
224+
{f g : HeckeCosetModule Δ H₁ H₂ Z} (h : ∀ D, f D = g D) : f = g :=
225+
Finsupp.ext h
226+
227+
end HeckeCosetModule

‎docs/references.bib‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3679,6 +3679,21 @@ @PhDThesis{ kremsater1972sequential
36793679
school = {University of British Columbia}
36803680
}
36813681

3682+
@Book{ krieg1990,
3683+
author = {Krieg, Aloys},
3684+
title = {Hecke algebras},
3685+
series = {Memoirs of the American Mathematical Society},
3686+
volume = {87},
3687+
number = {435},
3688+
publisher = {American Mathematical Society, Providence, RI},
3689+
year = {1990},
3690+
pages = {x+158},
3691+
issn = {0065-9266},
3692+
mrnumber = {1027069},
3693+
doi = {10.1090/memo/0435},
3694+
url = {https://doi.org/10.1090/memo/0435}
3695+
}
3696+
36823697
@Book{ kung_rota_yan2009,
36833698
author = {Kung, Joseph P. S. and Rota, Gian-Carlo and Yan, Catherine
36843699
H.},
@@ -5448,6 +5463,20 @@ @Book{ sga-4-tome-1
54485463
zbl = {0234.00007}
54495464
}
54505465

5466+
@Book{ shimura1971,
5467+
author = {Shimura, Goro},
5468+
title = {Introduction to the arithmetic theory of automorphic
5469+
functions},
5470+
series = {Publications of the Mathematical Society of Japan},
5471+
volume = {11},
5472+
note = {Kan\^{o} Memorial Lectures, No. 1},
5473+
publisher = {Iwanami Shoten Publishers, Tokyo; Princeton University
5474+
Press, Princeton, NJ},
5475+
year = {1971},
5476+
pages = {xiv+267},
5477+
mrnumber = {0314766}
5478+
}
5479+
54515480
@Book{ sierpinski1958,
54525481
author = {Wacław Sierpiński},
54535482
title = {Cardinal and Ordinal Numbers},

0 commit comments

Comments
 (0)