The double coset Γ₁(N) · diag(1, p) · Γ₁(N) at an index supported on the level #
GL2/CosetDecomposition.lean supplies the p upper-triangular matrices
upperTriRep p b = !![1, b; 0, p], and HeckeSlash/UpperTri/ builds an operator on
M_k(Γ₁(N)) by slashing against them and summing. Nothing so far says that this family is the
double coset of diag(1, p), and without that the classical operator and the abstract Hecke
ring's operator are two unrelated objects. This file proves the missing statement, whenever every
prime factor of p divides N:
Γ₁(N) · diag(1, p) · Γ₁(N) = ⋃_{b < p} Γ₁(N) · !![1, b; 0, p],
a disjoint union of right cosets — the handedness Shimura's slash sum needs
(HeckeSlash/Basic.lean).
Why the index must be supported on the level, and where that enters #
Only the inclusion ⊆ uses it. An element of the double coset is γ₁ · diag(1, p) · γ₂, and
since the left factor is absorbed by the coset, the content is that diag(1, p) · γ₂ lies in one
of the p right cosets. Writing γ₂ = !![a, b; c, d], the candidate is
diag(1, p) · γ₂ = !![a, m; p c, d - c j] · !![1, j; 0, p],
which asks for p ∣ b - a j — solvable for j because a is invertible modulo p. That
is where the level enters: γ₂ ∈ Γ₁(N) gives a ≡ 1 (mod N), so a is coprime to N, and the
hypothesis p.primeFactors ⊆ N.primeFactors promotes that to coprimality with p. The new left
factor lands back in Γ₁(N) because N ∣ c makes both p c ≡ 0 and d - c j ≡ d ≡ 1 modulo
N.
The hypothesis is p.primeFactors ⊆ N.primeFactors rather than p ∣ N because the prime powers
p = q ^ r with q ∣ N are exactly the indices the bad-prime operators T_{q^r} = U_q^r need,
and they need not divide N. Divisibility is the special case, by
Nat.primeFactors_mono.
Failure is known when p is prime and p ∤ N: the double coset then has p + 1 right cosets,
the extra one represented by
!![m, n; N, p] · diag(p, 1) for any m p − n N = 1 (Diamond–Shurman, Proposition 5.2.1). That
case is proved in Gamma1/CoprimeCosets.lean by
doubleCoset_natDiagGL_eq_iUnion_rightCosets_of_prime.
The reverse inclusion needs no hypothesis on the index: !![1, b; 0, p] = diag(1, p) · Tᵇ and
every power of T = !![1, 1; 0, 1] lies in Γ₁(N).
Main definitions #
HeckeRing.GL2.diagCosetGamma1: the double coset ofdiag(1, p)in the Hecke triple ofΓ₁(N), an element ofHeckeCoset (Δ₀(N)) (Γ₁(N)) (Γ₁(N)).
Main results #
HeckeRing.GL2.natDiagGL_one_mem_Delta0,HeckeRing.GL2.coe_natDiagGL_one, andHeckeRing.GL2.coe_map_natDiagGL_one:diag(1, p)lies inΔ₀(N)at every level, and its matrix overℚandℝ.HeckeRing.GL2.natDiagGL_mul_mapGL_T_zpow:diag(1, p) · Tᵇ = !![1, b; 0, p], the reverse inclusion in one line.HeckeRing.GL2.exists_mem_Gamma1_natDiagGL_mul_of_dvd: the factorisationdiag(1, p) · γ = δ · !![1, j; 0, p]withδ ∈ Γ₁(N), at any offsetjwithp ∣ b − a j;HeckeRing.GL2.exists_mem_Gamma1_natDiagGL_mulchooses such an offset fromp.primeFactors ⊆ N.primeFactors, and is the forward inclusion.HeckeRing.GL2.op_upperTriRep_smul_injective: thepright cosets are pairwise distinct, so the union is disjoint. Stated for an arbitrary subgroup ofSL₂(ℤ), since only integrality is used.DoubleCoset.doubleCoset_eq_iUnion_rightCosets_of_forall_exists: the general criterion turning forward factorizations and reverse witnesses into a right-coset decomposition.HeckeRing.GL2.doubleCoset_out_diagCosetGamma1_eq_doubleCoset_natDiagGL: the chosen representative ofdiagCosetGamma1 N phas the canonical double coset.HeckeRing.GL2.doubleCoset_natDiagGL_eq_iUnion_rightCosets: the decomposition itself, andHeckeRing.GL2.doubleCoset_out_diagCosetGamma1_eq_iUnion_rightCosetsthe same statement read at the chosen representative ofdiagCosetGamma1 N p, which is the shape the slash sum ofModularForms/HeckeSlash/Independence.leanconsumes.
Provenance #
No code is transcribed. The statement generalises Diamond–Shurman Proposition 5.2.1 in the
bad-prime case, proved here directly for this repository's own representative families
natDiagGL and upperTriRep, rather than for transcribed matrices. The AINTLIB
LeanModularForms project (Chris Birkbeck, Apache-2.0) organises the same case as its
heckeT_p_divN branch of heckeT_p_all
(LeanModularForms/HeckeRIngs/GL2/HeckeT_n.lean), on the operator rather than the coset side;
the coset statement below is what identifies the two, and is proved from the group law here.
References #
diag(1, p) ∈ Δ₀(N), for every level N: the upper-left entry is 1, a unit modulo
anything. This is natDiagGL_mem_Delta0_of_coprime with its hypothesis discharged.
The matrix of diag(1, p), for 0 < p.
The real matrix obtained by mapping diag(1, p) from GL₂(ℚ), for nonzero p.
The Hecke double coset of diag(1, p) at level Γ₁(N). For p ∣ N this is the coset
whose slash sum is the classical Tₚ = Uₚ; the identification is
doubleCoset_natDiagGL_eq_iUnion_rightCosets, and its operator form lives in
ModularForms/HeckeSlash/UpperTri/DoubleCoset.lean.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Defining equation for the sealed definition diagCosetGamma1.
The underlying set of diagCosetGamma1 N p is the double coset of diag(1, p).
diag(1, p) · Tᵇ = !![1, b; 0, p]. Right multiplication by the b-th power of the
translation matrix moves diag(1, p) onto the b-th upper-triangular representative; this is
the reverse inclusion of the coset decomposition below.
The forward factorisation, at a prescribed offset. If γ ∈ Γ₁(N) and the offset
j < p satisfies p ∣ b − a j for γ = !![a, b; c, d], then diag(1, p) · γ lies in the
right coset Γ₁(N) · !![1, j; 0, p]: explicitly
diag(1, p) · γ = !![a, m; p c, d − c j] · !![1, j; 0, p], where b − a j = p m.
The divisibility on the offset is the only arithmetic input, and it is where the two branches
of Diamond–Shurman's Proposition 5.2.1 differ: when every prime factor of p divides N, every
γ ∈ Γ₁(N) admits such a j (exists_mem_Gamma1_natDiagGL_mul), while at a prime p ∤ N only
those with p ∤ a do, the rest needing the further coset of Gamma1/CoprimeCosets.lean.
The forward factorisation at an index supported on the level. If every prime factor of
p divides N, then for γ ∈ Γ₁(N) the product diag(1, p) · γ lies in one of the p right
cosets Γ₁(N) · !![1, j; 0, p].
The p right cosets are pairwise distinct. If Γ · !![1, j₁; 0, p] = Γ · !![1, j₂; 0, p]
for a subgroup Γ of SL₂(ℤ), then j₁ = j₂: the comparison matrix has upper-left entry 1
and upper-right entry (j₂ − j₁)/p, and integrality forces p ∣ j₂ − j₁, which two offsets
below p can only satisfy by being equal.
Only integrality of Γ is used, so no congruence condition and no divisibility appear.
The Tₚ double coset at an index supported on the level is the union of the p
upper-triangular right cosets.
Γ₁(N) · diag(1, p) · Γ₁(N) = ⋃_{j < p} Γ₁(N) · !![1, j; 0, p], whenever every prime factor of
p divides N — Diamond–Shurman's Proposition 5.2.1 in the bad-prime case, and its extension
to the prime powers q ^ r with q ∣ N.
The inclusion ⊇ is natDiagGL_mul_mapGL_T_zpow and needs no hypothesis on the index; the
inclusion ⊆ is exists_mem_Gamma1_natDiagGL_mul and is where the hypothesis enters. That the
union is disjoint is op_upperTriRep_smul_injective.
The chosen representative of diagCosetGamma1 N p has the same double coset as the
canonical matrix diag(1, p).
The decomposition of doubleCoset_natDiagGL_eq_iUnion_rightCosets, read at the chosen
representative D.out of diagCosetGamma1 N p — the shape the slash-sum machinery of
HeckeSlash/Independence.lean consumes.
The right-coset decomposition of Γ₁(N) diag(1,n) Γ₁(N) is finite. Stated on the
underlying rational matrix so instance search does not need to recover its Δ₀(N) membership.