The arithmetic Hecke triple for GL_n #
The canonical arithmetic Hecke triple in GL_n(ℚ), following Shimura §3.2:
H = SL_n(ℤ) (embedded via mapGL ℚ) and Δ the submonoid of integral matrices with
positive determinant. The heart is Shimura's Lemma 3.10
(posDetInt_le_commensurator): Δ lies in the commensurator of SL_n(ℤ), because for an
integral α with det α = d ≠ 0 the congruence subgroup
Γ(d) = ker(SL_n(ℤ) → SL_n(ℤ/dℤ)) has finite index and has conjugates in both directions
contained in SL_n(ℤ) — since α⁻¹ = adj(α)/d and γ ≡ 1 mod d.
The file ends with the resulting IsHeckeTriple instance, on which the Hecke ring
𝕋 Δ SL_n(ℤ) ℤ of GL_n is founded.
Ported from the AINTLIB LeanModularForms project
(LeanModularForms/HeckeRIngs/GLn/Basic.lean, Chris Birkbeck), realizing the Layer-2
substrate of the ModularForms roadmap (the GL₂ case specializes to the Hecke operators on
modular forms); the AINTLIB HeckePair bundle is replaced by Mathlib's IsHeckeTriple.
Main definitions #
SLnZ:SL_n(ℤ)as a subgroup ofGL_n(ℚ), viamapGL ℚ.posDetInt: integral matrices with positive determinant, Shimura'sΔ.intMatrix: the integral matrix underlying an element ofintEntries n, as a monoid homomorphism, characterised bymap_intMatrixandintMatrix_eq_iff.
Main results #
SLnZ_le_posDetInt:SL_n(ℤ) ≤ Δ.posDetInt_le_commensurator:Δ ≤ commensurator(SL_n(ℤ))(Shimura's Lemma 3.10).commensurable_map_SLnZ: the image of a finite-index subgroup ofSL_n(ℤ)is commensurable withSL_n(ℤ)— the step by which each congruence subgroup inherits Lemma 3.10 and so sits in a Hecke triple of its own.mem_doubleCoset_of_intMatrix_eq_of_mem: double-coset membership from an integral identityτ * A * δ = Bbetween the witnesses, for any two subgroups containing the images ofτandδ.mem_doubleCoset_SLnZ_of_intMatrix_eqis itsSL_n(ℤ)case, anddet_eq_of_mem_doubleCoset_of_le_SLnZextracts the determinant invariant in the other direction.mem_intEntries_of_mem_doubleCoset: the double coset of an integral matrix between images of subgroups ofSL_n(ℤ)consists of integral matrices;mem_intEntries_of_rightCoset_eq,mem_intEntries_of_coverandmem_intEntries_of_mem_doubleCoset_mul_doubleCosetread this off a right coset, a family covering the double coset, and a product of two double cosets.- the
IsHeckeTriple (posDetInt n) (SLnZ n) (SLnZ n)instance, and the Hecke ringIntegralHeckeRing nit founds.
References #
SL_n(ℤ) as a subgroup of GL_n(ℚ), via mapGL ℚ : SL(n, ℤ) →* GL(n, ℚ).
Following mathlib's pattern for arithmetic subgroups.
Equations
Instances For
Coercion from SL_n(ℤ) to GL_n(ℚ) via mapGL ℚ.
Equations
- HeckeRing.GLn.coeMapGLRat n = { coe := ⇑(Matrix.SpecialLinearGroup.mapGL ℚ) }
Instances For
The canonical membership: integral special-linear matrices land in SL_n(ℤ). Not a
simp lemma: mem_SLnZ_iff subsumes it as a normal form.
Membership in SL_n(ℤ) characterised by an integral special-linear witness: the
elimination principle paired with coe_mem_SLnZ. SLnZ is a sealed definition, so modules
downstream cannot unfold it to MonoidHom.range; this lemma is how they extract the witness.
An element of SL_n(ℤ) has matrix determinant one over ℚ.
SpecialLinearGroup.det_mapGL is the same fact for GeneralLinearGroup.det, which is
ℚˣ-valued; every consumer needs the Matrix.det of the coerced matrix, so this is the
Units.val bridge rather than a second proof.
Integral representatives survive two-sided integral translation. If A represents
g ∈ GL_n(ℚ) entrywise over ℤ, then τ * A * δ represents mapGL τ * g * mapGL δ for any
τ δ : SL_n(ℤ).
Nothing here is specific to a level or a dimension: it is the statement that the entrywise
ℤ → ℚ cast is multiplicative, packaged for the two-sided translations that every
change-of-representative argument performs.
Lifting an integral equivalence to GL_n(ℚ). The converse reading of
mapGL_mul_coe_eq_intMatrix: if the integral witnesses of g and h are related by
τ * A * δ = B with τ, δ of determinant one, then h is the two-sided translate
of g.
mapGL_mul_coe_eq_intMatrix computes the matrix of a translate; this recovers the translate
from its matrix, which is what a change-of-representative argument actually needs — such an
argument produces an integral identity and must conclude an identity in GL_n(ℚ).
Double-coset membership from an integral equivalence. Integral matrices of determinant
one relating the witnesses of g and h put h in the H₁-H₂-double coset of g, for any
two subgroups containing the images of those matrices.
This is the shape every "same double coset" argument ends in: the work is done over ℤ, by
exhibiting the two determinant-one factors, and this converts that into the membership
statement. Nothing forces the subgroups to be SL_n(ℤ) — all that is used is that each factor
lies in its own subgroup, which is a hypothesis here, so the lemma applies equally to images of
congruence subgroups.
det_eq_of_mem_doubleCoset_of_le_SLnZ is the companion in the other direction, extracting the
determinant invariant from such a membership.
The SL_n(ℤ) case of mem_doubleCoset_of_intMatrix_eq_of_mem, where the two factors lie in
the subgroups for free.
The case of coefficient subgroups inside SL_n(ℤ), which is how the congruence subgroups
get it.
The SL_n(ℤ) case of det_eq_of_mem_doubleCoset_of_le_SLnZ.
The image in GL_n(ℚ) of a finite-index subgroup of SL_n(ℤ) is commensurable with
SL_n(ℤ). Since mapGL ℚ is injective, both relative indices transport along it: one is the
index of H, finite by hypothesis, and the other is 1.
This is the commensurability every congruence subgroup needs in order to sit in a Hecke
triple, so it is stated once here for an arbitrary finite-index subgroup rather than
re-proved at each of Γ₀(N), Γ₁(N), Γ(N).
The identity matrix has integer entries.
Product of integer-entry matrices has integer entries.
The submonoid of GL_n(ℚ) consisting of invertible matrices with integer entries
and positive determinant — Shimura's Δ, as the integral-entry part of Mathlib's
positive-determinant subgroup Matrix.GLPos.
Equations
Instances For
posDetInt n is contained in the positive-determinant submonoid, forgetting integrality.
posDetInt n is defined as a meet, so this is one projection of it — but the meet is not visible
outside this file (posDetInt is not @[expose]), so consumers that need only positivity, and
not integrality, must go through this lemma.
posDetInt n is contained in the integral-entry submonoid, forgetting positivity — the other
projection of the meet, for consumers that need only integrality.
The image of SL_n(ℤ) has integer entries.
The image in GL_n(ℚ) of a subgroup of SL_n(ℤ) has integer entries.
The double coset Γ₁' δ Γ₂' of an integral matrix δ between the images
Γᵢ' = Γᵢ.map (mapGL ℚ) of two subgroups of SL_n(ℤ) consists of integral matrices.
A matrix generating the same right coset of Γ' = Γ.map (mapGL ℚ) as an integral matrix is
integral: Γ' δ₁ = Γ' δ₂ puts δ₂ = (δ₂ δ₁⁻¹) δ₁ with δ₂ δ₁⁻¹ ∈ Γ'.
Every member of a family whose right cosets cover the double coset Γ₁' δ Γ₂' of an integral
matrix δ is integral: it lies in its own right coset, hence in the double coset. Membership of
the family in intEntries n is therefore not an extra hypothesis on statements that assume such
a covering.
The product Γ₁' δ₁ Γ₂' · Γ₂' δ₂ Γ₃' of the double cosets of two integral matrices consists
of integral matrices.
The integral matrix underlying an element of intEntries n #
Membership in intEntries n is an existential over integral matrices, so reading off the
integral matrix of an element chooses a witness. The choice is harmless: the entrywise cast
ℤ → ℚ is injective, so the witness is unique (intMatrix_eq_iff), and intMatrix is a monoid
homomorphism. It is the interface through which integral structures — binary forms with integer
coefficients, modular symbols — receive the action of a Hecke coset representative.
The integral matrix underlying an element of intEntries n, as a monoid homomorphism
intEntries n →* Matrix (Fin n) (Fin n) ℤ. It is characterised by map_intMatrix (its cast to
ℚ is the matrix of g) and intMatrix_eq_iff.
Equations
- HeckeRing.GLn.intMatrix n = { toFun := HeckeRing.GLn.intMatrixFun✝ n, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The cast to ℚ of the integral matrix of g is the matrix of g.
The integral matrix is characterised by its cast: intMatrix n g = A exactly when the
matrix of g is the cast of A. This is the introduction rule for computing intMatrix at an
element given by an explicit integral matrix.
The integral matrix of the image of σ ∈ SL_n(ℤ) is σ itself.
SL_n(ℤ) ⊆ Δ: elements of SL_n(ℤ) have integer entries and det = 1 > 0.
SL_n(ℤ) has positive determinant, forgetting integrality — the composite of
SLnZ_le_posDetInt with posDetInt_le_glpos, for consumers that need only the determinant.
If g has integer matrix A and γ ∈ SL_n(ℤ) is congruent to the identity modulo
|det A|, then g⁻¹ γ g is again in SL_n(ℤ).
Reverse direction of inv_conjugate_mem_SLnZ_of_mem_ker: if g has integer matrix A
and γ ∈ SL_n(ℤ) is congruent to the identity modulo |det A|, then g γ g⁻¹ is again in
SL_n(ℤ).
Every integral-entry element of GL_n(ℚ) lies in the commensurator of SL_n(ℤ)
(Shimura Lemma 3.10): if α has integer entries with |det(α)| = d — nonzero, since
invertibility already forces the determinant of an integral witness to be nonzero, so
positivity is not needed — then the congruence subgroup Γ(d) = ker(SL_n(ℤ) → SL_n(ℤ/dℤ))
has finite index in SL_n(ℤ) and is contained in both SL_n(ℤ) ∩ α·SL_n(ℤ)·α⁻¹ and
SL_n(ℤ) ∩ α⁻¹·SL_n(ℤ)·α, establishing commensurability.
Δ ⊆ commensurator(SL_n(ℤ)), by projection: a positive-determinant integral matrix is
in particular integral.
The arithmetic Hecke triple for GL_n: SL_n(ℤ) ≤ Δ ≤ commensurator(SL_n(ℤ)) in
GL_n(ℚ), where Δ is the positive-determinant integral submonoid. This is the Hecke triple
underlying the classical Hecke operators, following Shimura §3.2.
The Hecke ring of GL_n over ℤ: the Hecke ring of the arithmetic triple.