Atkin–Lehner matrices #
For an exact divisor Q of the level N — Q ∣ N with Q coprime to N / Q, the notion of
TauCeti/Data/Nat/ExactDivisor.lean — an Atkin–Lehner matrix is an integral
W = !![Q * a, b; N * c, Q * d] with det W = Q.
Writing N = Q * m, the determinant condition Q ^ 2 * a * d - Q * m * b * c = Q is Q times
the reduced determinant equation Q * a * d - m * b * c = 1, which is the identity every
computation below runs on.
Such a W exists exactly because Q and m are coprime: Bézout supplies Q * x + m * y = 1,
and !![Q * x, -y; N, Q] is an Atkin–Lehner matrix. That is atkinLehnerMatrix N Q, a choice
and not a canonical object — but the choice does not matter, because any two Atkin–Lehner
matrices for the same Q differ by an element of Γ₀(N) on either side
(IsAtkinLehnerMatrix.exists_mem_Gamma0_eq_mul_left and its right-handed twin), and a form on
which Γ₀(N) acts trivially cannot tell them apart. The two-sided version of that statement is that
W normalizes Γ₀(N), which is what makes the weight-k slash by W an operator on
M_k(Γ₀(N)) at all.
Two degenerate members of the family are worth naming. At Q = 1 an Atkin–Lehner matrix is
exactly an element of Γ₀(N), so the operator is the identity; at Q = N the Fricke matrix
!![0, -1; N, 0] of TauCeti/NumberTheory/ModularForms/Fricke/Matrix.lean is one, so the whole
Fricke theory is the Q = N member of this family.
The family is multiplicative in the divisor: whenever Q * R divides the level, a product of an
Atkin–Lehner matrix for Q and one for R is an Atkin–Lehner matrix for Q * R
(IsAtkinLehnerMatrix.mul). For coprime exact divisors Q and R the product Q * R is again
an exact divisor (TauCeti.Nat.IsExactDivisor.mul), so the exact-divisor members of the family are
closed under coprime products. Squaring stays inside Γ₀(N) up to the scalar Q
(exists_mem_Gamma0_mul_self) — the matrix-level source of the involution 𝒲_Q ^ 2 = 1 in even
weight. The diamond label of W ^ 2 / Q is -1 modulo Q, and Q times it is W₁₁ ^ 2 modulo
N; this is what the square of W_Q on a nebentypus space is computed from.
Moving γ ∈ Γ₀(N) across W, as γ W = W δ, does not preserve the lower-right entry s of γ
modulo N, which is the diamond label of γ: the lower-right entry of δ is s⁻¹ modulo Q and
s modulo N / Q. In terms of the idempotent e_Q of ZMod N it is e_Q s⁻¹ + (1 - e_Q) s,
because the reduced determinant equation of W reads -m b c ≡ e_Q and Q a d ≡ 1 - e_Q. So W
normalizes Γ₁(N) too, and acts on the diamond labels through Nat.IsExactDivisor.unitsInvPart.
Main definitions #
TauCeti.IsAtkinLehnerMatrix: the predicate above.TauCeti.atkinLehnerMatrix: the Bézout witness!![Q * x, -y; N, Q].TauCeti.atkinLiMatrix: the witness!![Q, 1; N * z, Q * w]normalized as by Atkin and Li, with lower-right entry1moduloN / Q.
Main results #
TauCeti.isAtkinLehnerMatrix_atkinLehnerMatrix,TauCeti.isAtkinLehnerMatrix_atkinLiMatrix: the witnesses work, for every exact divisor.TauCeti.isAtkinLehnerMatrix_one_iff_mem_Gamma0,TauCeti.isAtkinLehnerMatrix_fricke: the two degenerate members,Q = 1andQ = N.TauCeti.IsAtkinLehnerMatrix.mul_left,TauCeti.IsAtkinLehnerMatrix.mul_right: the family is stable under multiplication byΓ₀(N)on either side.TauCeti.IsAtkinLehnerMatrix.exists_mem_Gamma0_eq_mul_left,TauCeti.IsAtkinLehnerMatrix.exists_mem_Gamma0_eq_mul_right: any two members for the sameQdiffer by an element ofΓ₀(N), on the left and on the right respectively.TauCeti.IsAtkinLehnerMatrix.exists_mem_Gamma0_mul_eq_mul_left,TauCeti.IsAtkinLehnerMatrix.exists_mem_Gamma0_mul_eq_mul_right:WnormalizesΓ₀(N), with the new element ofΓ₀(N)produced on the left and on the right respectively.TauCeti.IsAtkinLehnerMatrix.exists_mem_Gamma0_mul_self:W ^ 2 = Q • γwithγ ∈ Γ₀(N).TauCeti.IsAtkinLehnerMatrix.toHomUnits_gamma0Map_of_mul_self_eq: the diamond label of thatγis the unit that is-1moduloQand satisfiesQ * u = W₁₁ ^ 2moduloN; under the Atkin–Li normalization it isQ⁻¹moduloN / Q(TauCeti.IsAtkinLehnerMatrix.unitsMap_div_toHomUnits_gamma0Map_of_mul_self_eq), so a split character takes the valueχ_Q(-1) χ_{N/Q}(Q)⁻¹on it (TauCeti.IsAtkinLehnerMatrix.mul_comp_unitsMap_toHomUnits_gamma0Map_of_mul_self_eq).TauCeti.IsAtkinLehnerMatrix.mul: the multiplicativity of the family in the divisor.TauCeti.IsAtkinLehnerMatrix.isExactDivisor: a divisor of the level that carries an Atkin–Lehner matrix is an exact divisor.TauCeti.IsAtkinLehnerMatrix.toHomUnits_gamma0Map_of_mul_eq_mul: movingγ ∈ Γ₀(N)acrossWinverts the residue moduloQof its lower-right entry and keeps its residue moduloN / Q.
Relation to the Atkin–Lehner anti-involution #
TauCeti/NumberTheory/HeckeRing/GL2/Gamma0/AtkinLehner.lean also carries the name: it conjugates
by natDiagGL 2 ![1, N] to repair the transpose's failure to preserve Γ₀(N), proving the
Γ₀(N) Hecke ring commutative. That is a different construction from the matrices here, and the
two do not interact.
References #
- F. Diamond and J. Shurman, A First Course in Modular Forms, §5.
- A. O. L. Atkin and J. Lehner, Hecke operators on
Γ₀(m), Math. Ann. 185 (1970), 134–160.
An Atkin–Lehner matrix for the divisor Q of the level N: an integral matrix
!![Q * a, b; N * c, Q * d] of determinant Q.
The upper-left entry is divisible by
Q.The lower-left entry is divisible by the level
N.The lower-right entry is divisible by
Q.The determinant is
Q.
Instances For
The entries of an Atkin–Lehner matrix, with the reduced determinant equation. Writing the
level as N = Q * m, the determinant condition det W = Q divides through by Q to
Q * (a * d) - m * (b * c) = 1; that equation, and not the determinant itself, is what the
identities below are polynomial consequences of.
Building an Atkin–Lehner matrix from the reduced determinant equation, the converse of
IsAtkinLehnerMatrix.exists_entries.
The Bézout witness !![Q * x, -y; N, Q], where Q * x + (N / Q) * y = 1. It is an
Atkin–Lehner matrix for every exact divisor Q of N (isAtkinLehnerMatrix_atkinLehnerMatrix),
and every other one differs from it by an element of Γ₀(N).
Instances For
Every exact divisor carries an Atkin–Lehner matrix. Coprimality of Q and N / Q is
exactly what Bézout needs, and it is used nowhere else in this file.
The Atkin–Li normalized Atkin–Lehner matrix !![Q, 1; N * z, Q * w], where
Q * w - (N / Q) * z = 1: in the notation !![Q * x, y; N * z, Q * w] of Atkin and Li it has
x = 1 and y = 1, so x ≡ 1 modulo N / Q and y ≡ 1 modulo Q. Its lower-right entry
Q * w is 1 modulo N / Q (intCast_atkinLiMatrix_one_one), which is the normalization under
which the square of W_Q on a nebentypus space is the constant Q ^ (k - 2) χ_Q(-1) χ_{N/Q}(Q)⁻¹.
It is an Atkin–Lehner matrix for every exact divisor Q of N
(isAtkinLehnerMatrix_atkinLiMatrix).
Instances For
The Atkin–Li matrix is an Atkin–Lehner matrix, for every exact divisor Q of N.
The lower-right entry of the Atkin–Li matrix is 1 modulo N / Q.
At Q = 1 the Atkin–Lehner matrices are exactly Γ₀(N). The corresponding operator is
the identity, which is why the family is indexed by exact divisors up to this normalization.
The Fricke matrix is the Atkin–Lehner matrix at Q = N. The Fricke theory of
TauCeti/NumberTheory/ModularForms/Fricke/ is therefore the top member of this family.
Multiplying an Atkin–Lehner matrix by Γ₀(N) on the left gives an Atkin–Lehner matrix
for the same Q.
Multiplying an Atkin–Lehner matrix by Γ₀(N) on the right gives an Atkin–Lehner matrix
for the same Q.
Two Atkin–Lehner matrices for the same Q differ by Γ₀(N) on the left. The witness is
W' W⁻¹, integral because the reduced determinant equation clears the 1 / Q in W⁻¹.
Two Atkin–Lehner matrices for the same Q differ by Γ₀(N) on the right, the mirror of
IsAtkinLehnerMatrix.exists_mem_Gamma0_eq_mul_left with witness W⁻¹ W'.
An Atkin–Lehner matrix normalizes Γ₀(N): W γ = δ W with δ ∈ Γ₀(N). This is the fact
that turns the weight-k slash by W into an operator on M_k(Γ₀(N)).
An Atkin–Lehner matrix normalizes Γ₀(N), read the other way: γ W = W δ with
δ ∈ Γ₀(N).
The square of an Atkin–Lehner matrix is Q times an element of Γ₀(N). Since a scalar
matrix slashes as a constant, this is the matrix-level reason the normalized operator 𝒲_Q is an
involution in even weight.
Multiplicativity of the family. As soon as Q * R divides the level, an Atkin–Lehner
matrix for Q times one for R is an Atkin–Lehner matrix for Q * R. Coprime exact divisors
Q and R satisfy the hypothesis and have Q * R again an exact divisor
(TauCeti.Nat.IsExactDivisor.mul), which is the case the family is indexed by.
A divisor carrying an Atkin–Lehner matrix is an exact divisor: for Q ∣ N, the reduced
determinant equation Q * (a * d) - (N / Q) * (b * c) = 1 is a Bézout relation between Q and
N / Q. The hypothesis Q ∣ N is needed, since IsAtkinLehnerMatrix does not force it:
!![3, 3; 2, 3] satisfies IsAtkinLehnerMatrix 2 3.
Moving γ ∈ Γ₀(N) across an Atkin–Lehner matrix, read on lower-right entries modulo
N: if γ W = W δ, the lower-right entry of δ is e_Q a + (1 - e_Q) s, where a and s are
the diagonal entries of γ and e_Q is the idempotent of the exact divisor Q. Since a and
s are mutually inverse modulo N, this is the lower-right entry s of γ with its residue
modulo Q inverted.
Moving γ ∈ Γ₀(N) across an Atkin–Lehner matrix inverts the residue modulo Q of its
diamond label: if γ W = W δ with δ ∈ Γ₀(N), the label of δ is the label of γ with its
residue modulo Q inverted and its residue modulo N / Q kept.
The diamond label of W ^ 2 / Q, multiplied by Q, is the square of the lower-right entry
of W: if W * W = Q • γ, then Q * γ₁₁ ≡ W₁₁ ^ 2 modulo N, because the lower-left entry
of W vanishes modulo N. Since Q is a unit modulo N / Q, this pins down the residue of γ₁₁
modulo N / Q.
The diamond label of W ^ 2 / Q is -1 modulo Q: if W * W = Q • γ, the lower-right
entry of γ is -1 modulo Q. Writing W = !![Q * a, b; Q * m * c, Q * d], that entry is
m * b * c + Q * d ^ 2, and the reduced determinant equation makes m * b * c ≡ -1.
The diamond label of W ^ 2 / Q: if W * W = Q • γ with γ ∈ Γ₀(N), the diamond label of
γ is the unit u of ZMod N that is -1 modulo Q and satisfies Q * u = W₁₁ ^ 2, which
determines it modulo N / Q.
The residue modulo Q of the diamond label of W ^ 2 / Q is -1: the units form of
IsAtkinLehnerMatrix.intCast_apply_one_one_of_mul_self_eq.
The residue modulo N / Q of the diamond label of W ^ 2 / Q, under the Atkin–Li
normalization: if the lower-right entry of W is 1 modulo N / Q, as for atkinLiMatrix,
and W * W = Q • γ with γ ∈ Γ₀(N), the diamond label of γ is Q⁻¹ modulo N / Q.
The diamond label of W ^ 2 / Q, multiplied by Q, is W₁₁ ^ 2 modulo N: the units form
of IsAtkinLehnerMatrix.natCast_mul_intCast_apply_one_one_of_mul_self_eq.
A split character on the diamond label of W ^ 2 / Q, under the Atkin–Li normalization:
if the lower-right entry of W is 1 modulo N / Q and W * W = Q • γ with γ ∈ Γ₀(N), then
χ = χ_Q · χ_{N/Q} split along N = Q · (N / Q) takes the value χ_Q(-1) χ_{N/Q}(Q)⁻¹ on the
diamond label of γ.