The double coset Γ₁(N) · diag(1, p) · Γ₁(N) at a prime p ∤ N #
Gamma1/UpperTriCosets.lean decomposes this double coset at p ∣ N, where the p
representatives !![1, b; 0, p] exhaust it. At a prime p ∤ N they do not: there is exactly one
further right coset, and this file produces it, giving Diamond–Shurman's Proposition 5.2.1 in its
remaining case,
Γ₁(N) · diag(1, p) · Γ₁(N) = (⋃_{b < p} Γ₁(N) · !![1, b; 0, p]) ∪ Γ₁(N) · σ · diag(p, 1),
a disjoint union of p + 1 right cosets. Here σ = !![m, n; N, p] is any integral matrix
with m p − n N = 1: an element of Γ₀(N), not of Γ₁(N), and it is that twist which later
supplies the factor χ(p) in the Hecke recurrence at a good prime.
Where the hypotheses enter #
The whole statement is carried by the bottom row of σ. Its two entries N and p together
with det σ = 1 say exactly m p − n N = 1
(mul_sub_mul_eq_one_of_lowerRow), so such a σ exists precisely when p and N are coprime,
as also follows from Matrix.SpecialLinearGroup.isCoprime_row. Everything below is stated for
an arbitrary such σ, which
keeps the coprimality implicit in the data rather than as a side hypothesis, and lets the caller
supply whichever Bézout witness it already has.
The field property supplied by primality is used only in the forward inclusion: writing
γ = !![a, b; c, d] for an element of Γ₁(N), the product diag(1, p) · γ lands in an
upper-triangular coset as soon as the congruence a j ≡ b (mod p) is solvable, which for p ∤ a
needs a invertible modulo p. The complementary case p ∣ a is where the twisted coset is
used, and it needs no primality:
diag(1, p) · γ = !![a − b N, b m − a′ n; p(c − d N), p d m − c n] · σ · diag(p, 1), a = p a′,
whose left factor has determinant (a d − b c)(m p − n N) = 1 and lies in Γ₁(N) because
N ∣ c and m p ≡ 1 (mod N). (For composite p ∤ N neither branch covers a γ with
1 < gcd(a, p) < p, and indeed the coset count is then not p + 1.)
Disjointness of the last coset from the others uses only 1 < p and integrality: comparing
σ · diag(p, 1) with !![1, b; 0, p] forces p ∣ n, which m p − n N = 1 forbids.
Main definitions #
HeckeRing.GL2.primeRep: thep + 1right-coset representatives, indexed byOption (Fin p)—some bthe upper-triangular!![1, b; 0, p],nonethe twistedσ · diag(p, 1).
Main results #
HeckeRing.GL2.exists_mem_Gamma1_natDiagGL_mul_primeRep_none_of_dvd: the factorisation ofdiag(1, p) · γthrough the twisted representative, forp ∣ a.HeckeRing.GL2.exists_mem_Gamma1_natDiagGL_mul_eq_primeRep_none:diag(1, p) · !![m p, n; N, 1] = σ · diag(p, 1)with!![m p, n; N, 1] ∈ Γ₁(N)— the reverse inclusion for the twisted coset.HeckeRing.GL2.exists_adjugateGL_natDiagGL_eq: for an index coprime to the level, the adjugate ofdiag(1, n)factors on either side throughdiag(1, n), aΓ₁(N)element, and aΓ₀(N)element whose diamond label isn⁻¹.HeckeRing.GL2.exists_mem_Gamma1_natDiagGL_mul_primeRep: for primep, everydiag(1, p) · γwithγ ∈ Γ₁(N)lies in one of thep + 1right cosets.HeckeRing.GL2.op_primeRep_smul_injective: thep + 1right cosets are pairwise distinct.HeckeRing.GL2.doubleCoset_natDiagGL_eq_iUnion_rightCosets_of_prime: the decomposition, andHeckeRing.GL2.doubleCoset_out_diagCosetGamma1_eq_iUnion_rightCosets_of_primethe 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 is Diamond–Shurman Proposition 5.2.1 in the case p ∤ N,
proved here for this repository's own representative families natDiagGL, upperTriRep and
scaleRep. The AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0) organises the same
case as the heckeT_p_coprime 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 #
- F. Diamond and J. Shurman, A first course in modular forms, Proposition 5.2.1 and §5.5.
- G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4–3.5.
The adjugate of diag(1, n) is an inverse-diamond translate of its double coset, on
either side. For n coprime to N there are A ∈ Γ₀(N) with diamond label ⟨n⟩⁻¹ (its
lower-right entry is n⁻¹ mod N) and B ∈ Γ₁(N) with
adj(diag(1, n)) = A · diag(1, n) · B = B · diag(1, n) · A in GL₂(ℝ).
The family of p + 1 matrices out of which the good-prime Tₚ is built. The p
upper-triangular matrices !![1, b; 0, p], indexed by some b, together with the twisted
diagonal σ · diag(p, 1), indexed by none; the definition makes no assumption on p or σ.
They are the right-coset representatives of Γ₁(N) · diag(1, p) · Γ₁(N) exactly under the
hypotheses of doubleCoset_natDiagGL_eq_iUnion_rightCosets_of_prime, namely for p prime and
σ with bottom row (N, p). The index type Option (Fin p) is what the slash-sum machinery of
HeckeSlash/Independence.lean sums over.
Equations
Instances For
The representative indexed by some b is the b-th upper-triangular matrix.
The representative indexed by none is the twisted diagonal σ · diag(p, 1).
The matrix of the twisted representative: multiplying by diag(p, 1) on the right scales the
first column of σ by p, so !![a, b; c, d] · diag(p, 1) = !![a p, b; c p, d]. At the bottom
row (N, p) the decomposition uses, this reads σ · diag(p, 1) = !![m p, n; N p, p].
The forward factorisation through the twisted coset. The product diag(1, p) · γ lies in
the right coset Γ₁(N) · σ · diag(p, 1) for every γ = !![a, b; c, d] ∈ Γ₁(N) with p ∣ a,
where σ = !![m, n; N, p], so that m p − n N = 1; p need not be prime. With a = p a′,
diag(1, p) · γ = !![a − b N, b m − a′ n; p(c − d N), p d m − c n] · σ · diag(p, 1).
The witness for the reverse inclusion. For 0 < p and σ = !![m, n; N, p], the matrix
γ = !![m p, n; N, 1] lies in Γ₁(N) and satisfies diag(1, p) · γ = σ · diag(p, 1), the twisted
representative.
The forward inclusion. The product diag(1, p) · γ lies in one of the p + 1 right cosets
Γ₁(N) · primeRep σ p i for every γ ∈ Γ₁(N), if p is prime and σ has bottom row (N, p).
The p + 1 right cosets are pairwise distinct, modulo any subgroup G ≤ SL(2, ℤ),
whenever 1 < p and σ has lower-right entry p.
The Tₚ double coset at a prime p ∤ N is the union of p + 1 right cosets.
Γ₁(N) · diag(1, p) · Γ₁(N) = ⋃_{j < p} Γ₁(N) · !![1, j; 0, p] ∪ Γ₁(N) · σ · diag(p, 1),
Diamond–Shurman's Proposition 5.2.1 in the case p ∤ N — the coprimality being carried by the
existence of the twist σ rather than stated separately (equivalently, by
Matrix.SpecialLinearGroup.isCoprime_row, the bottom-row entries are coprime).
The inclusion ⊆ is exists_mem_Gamma1_natDiagGL_mul_primeRep and is where primality enters;
⊇ is natDiagGL_mul_mapGL_T_zpow on the upper-triangular cosets and
exists_mem_Gamma1_natDiagGL_mul_eq_primeRep_none on the twisted one. That the union is disjoint
is op_primeRep_smul_injective, which only needs 1 < p.
The decomposition of doubleCoset_natDiagGL_eq_iUnion_rightCosets_of_prime, read at the
chosen representative D.out of diagCosetGamma1 N p — the shape the slash-sum machinery of
HeckeSlash/Independence.lean consumes.