The upper-triangular coset factorisation at Γ₀ #
Write γ = !![a, b; c, d] ∈ SL(2, ℤ). Matching entries in
!![1, j; 0, p] · γ = γ' · !![1, j'; 0, p] forces γ' = !![a + jc, b'; pc, d - cj'] and
p b' = b + jd - (a + jc) j', so the offset j' must solve
(a + jc) j' ≡ b + jd (mod p).
That has a unique solution in [0, p) exactly when a + jc is invertible modulo p, and
upperTriShift p γ j is it. On Γ₀(p) invertibility is automatic and uniform in j: p ∣ c
collapses a + jc to a, and ad - bc = 1 reduces to ad ≡ 1 (mod p), exhibiting d as the
inverse of a, so the solution takes the closed form j' = d b + j d² mod p and the map is a
bijection of Fin p.
Everything here is a statement about matrices and congruence subgroups. Nothing in this file
mentions the slash action; the equivariance of the upper-triangular sum, which consumes these
results, lives in ModularForms/HeckeSlash/UpperTri/Invariance.lean.
Main definitions #
HeckeRing.GL2.upperTriShift: the offset map,j ↦ (a + jc)⁻¹ (b + jd) mod p.
Main results #
HeckeRing.GL2.mul_upperTriShift_natCast: it solves(a + jc) j' ≡ b + jd (mod p)whenevera + jcis invertible.HeckeRing.GL2.upperTriShift_eq_iff: and it is the only solution in[0, p).HeckeRing.GL2.upperTriShift_natCast_of_mem_Gamma0: onΓ₀(p)it isj ↦ d b + j d² mod p.HeckeRing.GL2.upperTriShift_bijective: onΓ₀(p)it is a bijection ofFin p.HeckeRing.GL2.exists_mem_Gamma0_upperTriRep_mul_of_isUnit: the factorisation!![1, j; 0, p] · γ = γ' · !![1, j'; 0, p]withγ' ∈ Γ₀(N), froma + jcinvertible modulopandN ∣ p c.HeckeRing.GL2.exists_mem_Gamma0_upperTriRep_mul: the same atγ ∈ Γ₀(p), where the first hypothesis holds for every offset at once.HeckeRing.GL2.exists_mem_Gamma0_upperTriRep_mul_of_mem_Gamma0: its specialisation top ∣ Nandγ ∈ Γ₀(N), whose conclusion is the modulo-Ncongruence of the lower-right entry.
The offset map, j ↦ (a + j c)⁻¹ (b + j d) mod p, where γ = !![a, b; c, d].
a + j c and b + j d are the top-left and top-right entries of !![1, j; 0, p] · γ
before dividing by p, so this is the unique solution in [0, p) of
(a + j c) j' ≡ b + j d (mod p) — whenever a + j c is invertible modulo p. Outside that case
the value is ZMod's junk inverse and solves nothing, so every lemma that reads the value as a
solution of that congruence carries the invertibility hypothesis. Lemmas that merely evaluate the
map, such as upperTriShift_natCast, hold for every γ and j.
Equations
- HeckeRing.GL2.upperTriShift p γ j = (ZMod.finEquiv p).symm ((↑(↑γ 0 0 + ↑↑j * ↑γ 1 0))⁻¹ * ↑(↑γ 0 1 + ↑↑j * ↑γ 1 1))
Instances For
The value of upperTriShift in ZMod p. Deliberately not a simp lemma: the junk inverse on
the right is not a normal form, and the two facts callers want are mul_upperTriShift_natCast and
upperTriShift_natCast_of_mem_Gamma0.
The defining congruence. For a + j c invertible modulo p, upperTriShift p γ j solves
(a + j c) j' ≡ b + j d (mod p). That it is the only solution in [0, p) is
upperTriShift_eq_iff.
The offset map is the only solution. Under invertibility of a + j c, an offset j'
in [0, p) solves (a + j c) j' ≡ b + j d (mod p) exactly when it is upperTriShift p γ j.
This is the elimination half of the characteristic API: mul_upperTriShift_natCast says the map
solves the congruence, and this says nothing else does.
On Γ₀(p) the offset map is j ↦ d b + j d². The closed form used by the equivariance
results in TauCeti/NumberTheory/ModularForms/HeckeSlash/UpperTri/Invariance.lean, and the reason
upperTriShift_bijective holds: d is the inverse of a, and d² is again a unit.
The offset map is a bijection. For γ ∈ Γ₀(p) it is the affine permutation
x ↦ d² x + d b of ZMod p, read through ZMod.finEquiv: d is the inverse of a modulo p,
so d² is a unit and multiplication by it is a permutation.
The coset factorisation. The product !![1, j; 0, p] · γ factors as
γ' · !![1, j'; 0, p] with γ' ∈ Γ₀(N) and j' the shifted offset, and the new lower-right
entry is d - c j'.
The two hypotheses are exactly what the factorisation consumes, and neither mentions how p and
N are related. a + j c invertible modulo p — for the single offset j at hand, not
uniformly — is what makes the offset j' exist; N ∣ p c is what puts the lower-left entry
p c of γ' back in Γ₀(N). Neither p ∣ N nor any membership at a level built from N is
assumed, so p ∤ N is not excluded. The Γ₀(p) specialisation exists_mem_Gamma0_upperTriRep_mul,
where invertibility holds for every offset at once and the map is a bijection, is the form callers
usually want.
The lower-right entry is given as an equation rather than as a congruence because the modulus
at which it is useful varies with the caller; the equivariance results in
TauCeti/NumberTheory/ModularForms/HeckeSlash/UpperTri/Invariance.lean read off the congruence
modulo N they need from that equation and Γ₀(N)-membership.
The coset factorisation at γ ∈ Γ₀(p). The specialisation in which every offset is
admissible at once: on Γ₀(p) the entry a + j c is a, a unit for every j, so the general
statement applies uniformly and the offset map is the closed form j ↦ d b + j d².
The coset factorisation at γ ∈ Γ₀(N). The specialisation of
exists_mem_Gamma0_upperTriRep_mul that p ∣ N and γ ∈ Γ₀(N) afford: both hypotheses of the
general statement follow, and the lower-right entry d - c j' becomes a congruence modulo N,
so γ' has the same Gamma0Map value as γ. That congruence is what lets the equivariance
results in TauCeti/NumberTheory/ModularForms/HeckeSlash/UpperTri/Invariance.lean carry a fixed
character, and it is the form every Γ₀(N) caller wants.
Conjugating an element of Γ(N) through [1, 0; 0, p] lands in Γ₁(N), for p ∣ N:
[1, 0; 0, p] · δ = ε · [1, 0; 0, p] with ε ∈ Γ₁(N). This is what lets a Γ₁(N)-invariant
function absorb a change of the extra representative of the descent family
(Newforms/Descent/LevelCommute.lean).