The Atkin–Lehner slash operator #
An Atkin–Lehner matrix W for a divisor Q of N normalizes Γ₀(N)
(TauCeti.IsAtkinLehnerMatrix.exists_mem_Gamma0_mul_eq_mul_left), so the weight-k slash by W
sends a modular form for Γ₀(N) to another one. That is the operator built here, on M_k(Γ₀(N))
and on S_k(Γ₀(N)).
The operator carries no normalizing scalar, so it is not an involution: W ^ 2 is Q times
an element of Γ₀(N), and a scalar matrix slashes by a power of its scalar, so the operator
squares to Q ^ (k - 2) (atkinLehnerOperator_atkinLehnerOperator). Dividing that away is the
job of the normalized operator 𝒲_Q = (√Q) ^ (2 - k) • (· ∣[k] W), built on top of this one in
TauCeti/NumberTheory/ModularForms/AtkinLehner/Normalized.lean. The Fricke member Q = N of the
family is studied separately in TauCeti/NumberTheory/ModularForms/Fricke/, on the Γ₁(N)
carrier.
The operator does not depend on which Atkin–Lehner matrix for Q is used: two of them differ by
an element of Γ₀(N), which a form for Γ₀(N) absorbs (atkinLehnerOperator_congr). The
arbitrary Bézout choice in TauCeti.atkinLehnerMatrix is therefore invisible, and
TauCeti.Nat.IsExactDivisor.atkinLehnerOperator — the operator W_Q indexed by the exact divisor
alone, with no matrix to supply — is the interface to use.
Main definitions #
TauCeti.atkinLehnerGL: an Atkin–Lehner matrix as an element ofGL (Fin 2) ℝ.TauCeti.atkinLehnerOperator,TauCeti.atkinLehnerOperatorCusp: the slash operator by a given Atkin–Lehner matrix, onM_k(Γ₀(N))and onS_k(Γ₀(N)).TauCeti.Nat.IsExactDivisor.atkinLehnerOperator,TauCeti.Nat.IsExactDivisor.atkinLehnerOperatorCusp: the operatorW_Qof an exact divisorQ, with the matrix taken to beTauCeti.atkinLehnerMatrix N Q.
Main results #
TauCeti.Gamma0_map_inv_conjAct_atkinLehnerGL_eq:Wnormalizes the image ofΓ₀(N)inGL (Fin 2) ℝ. This is what makes the operator well defined.TauCeti.atkinLehnerOperator_congr,TauCeti.atkinLehnerOperatorCusp_congr: independence of the chosen Atkin–Lehner matrix.TauCeti.atkinLehnerOperator_coe_cuspForm: the two operators agree under the coercionS_k(Γ₀(N)) → M_k(Γ₀(N)).TauCeti.slash_atkinLehnerGL_slash_atkinLehnerGL_of_mul_self_eq: forW * W = Q • γ, slashing twice byWisQ ^ (k - 2)times slashing byγ, for any function.TauCeti.atkinLehnerOperator_atkinLehnerOperator,TauCeti.atkinLehnerOperatorCusp_atkinLehnerOperatorCuspand theirTauCeti.Nat.IsExactDivisorcounterparts: the square isQ ^ (k - 2).TauCeti.Nat.IsExactDivisor.atkinLehnerOperator_eq,TauCeti.Nat.IsExactDivisor.atkinLehnerOperatorCusp_eq:W_Qis the slash by any Atkin–Lehner matrix forQ.TauCeti.Nat.IsExactDivisor.atkinLehnerOperator_atkinLehnerOperator_of_coprimeand its cusp-form counterpart:W_R ∘ W_Q = W_{Q R}at coprime exact divisors.TauCeti.Nat.IsExactDivisor.atkinLehnerOperator_one,TauCeti.Nat.IsExactDivisor.atkinLehnerOperatorCusp_one:W_1is the identity.TauCeti.Nat.IsExactDivisor.coe_atkinLehnerOperator_self,TauCeti.Nat.IsExactDivisor.coe_atkinLehnerOperatorCusp_self:W_Nis the slash by the Fricke matrixTauCeti.frickeGL ℝ N, the slash thatTauCeti.frickeOperatorperforms at levelΓ₁(N).
References #
An Atkin–Lehner matrix, read in GL (Fin 2) ℝ. Its determinant is Q, nonzero by the
positivity hypothesis, so the integral matrix really is invertible over ℝ.
Equations
Instances For
The underlying matrix of atkinLehnerGL is the entrywise real cast.
The determinant of atkinLehnerGL is Q.
The determinant of atkinLehnerGL is positive, so it slashes by the det > 0 formula.
Moving W past Γ₀(N), the GL (Fin 2) ℝ reading of
IsAtkinLehnerMatrix.exists_mem_Gamma0_mul_eq_mul_left.
Moving Γ₀(N) past W, the mirror of
exists_mem_Gamma0_atkinLehnerGL_mul_mapGL.
W normalizes Γ₀(N) in GL (Fin 2) ℝ. Conjugating the image of Γ₀(N) by an
Atkin–Lehner matrix returns that same subgroup, which is what makes the slash by W an operator
on modular forms of level Γ₀(N).
The Atkin–Lehner slash operator on M_k(Γ₀(N)): f ↦ f ∣[k] W, as a ℂ-linear
endomorphism. It carries no normalizing scalar; see the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On underlying functions the Atkin–Lehner operator is ⇑f ∣[k] W.
The Atkin–Lehner slash operator on cusp forms S_k(Γ₀(N)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
On underlying functions the cusp-form Atkin–Lehner operator is ⇑f ∣[k] W.
The two Atkin–Lehner slash operators agree under the coercion S_k(Γ₀(N)) → M_k(Γ₀(N)):
both slash by W, which does not see whether a form vanishes at the cusps. This is the
counterpart of frickeOperator_coe_cuspForm for the Fricke operator.
The operator does not depend on the chosen Atkin–Lehner matrix. Two of them differ by an
element of Γ₀(N) on the left, which a form of level Γ₀(N) absorbs.
The cusp-form operator does not depend on the chosen Atkin–Lehner matrix. This is
atkinLehnerOperator_congr read on the image of the coercion S_k(Γ₀(N)) → M_k(Γ₀(N)); no
second representative-and-slash argument is needed.
Slashing twice by W is Q ^ (k - 2) times slashing by W ^ 2 / Q: if W * W = Q • γ
with γ ∈ SL(2, ℤ), the scalar matrix Q contributes the constant Q ^ (k - 2) and what is left
is the slash by γ. No invariance of f is assumed.
Slashing twice by W multiplies by Q ^ (k - 2). The square W ^ 2 is Q times an
element of Γ₀(N); the scalar matrix contributes Q ^ (k - 2) and the Γ₀(N) factor is
absorbed. This is the identity the normalization (√Q) ^ (2 - k) turns into an involution in
even weight.
The Atkin–Lehner operator squares to Q ^ (k - 2) on M_k(Γ₀(N)).
The cusp-form Atkin–Lehner operator squares to Q ^ (k - 2).
The operator of an exact divisor #
Taking the Bézout witness atkinLehnerMatrix N Q as the representative leaves one operator W_Q
per exact divisor Q of N, with no matrix for the user to supply. By
atkinLehnerOperator_congr it is the slash by any Atkin–Lehner matrix for Q whatsoever.
The Atkin–Lehner operator W_Q on M_k(Γ₀(N)), for an exact divisor Q of N: the
slash by atkinLehnerMatrix N Q. Any other Atkin–Lehner matrix for Q gives the same operator
(Nat.IsExactDivisor.atkinLehnerOperator_eq).
Equations
- h.atkinLehnerOperator k = TauCeti.atkinLehnerOperator ⋯ ⋯ ⋯ k
Instances For
The Atkin–Lehner operator W_Q on cusp forms S_k(Γ₀(N)).
Equations
- h.atkinLehnerOperatorCusp k = TauCeti.atkinLehnerOperatorCusp ⋯ ⋯ ⋯ k
Instances For
On underlying functions W_Q is the slash by atkinLehnerMatrix N Q, read in
GL (Fin 2) ℝ.
On underlying functions the cusp-form W_Q is the slash by atkinLehnerMatrix N Q, read in
GL (Fin 2) ℝ.
W_Q is the slash by any Atkin–Lehner matrix for Q.
The cusp-form W_Q is the slash by any Atkin–Lehner matrix for Q.
W_Q squares to Q ^ (k - 2) on M_k(Γ₀(N)).
The cusp-form W_Q squares to Q ^ (k - 2).
Composition in the divisor #
Slashing by an Atkin–Lehner matrix for Q and then by one for R is slashing by their product,
which is an Atkin–Lehner matrix for Q * R (TauCeti.IsAtkinLehnerMatrix.mul). On coprime exact
divisors this reads W_R ∘ W_Q = W_{Q R}, and since Q * R = R * Q the two operators commute.
Composing the two raw Atkin–Lehner operators on M_k(Γ₀(N)): first W_Q, then W_R,
is the operator of the product matrix, an Atkin–Lehner matrix for Q * R.
Composing the two raw Atkin–Lehner operators on S_k(Γ₀(N)).
W_R ∘ W_Q = W_{Q R} at coprime exact divisors, on M_k(Γ₀(N)). The product Q * R is
again an exact divisor (TauCeti.Nat.IsExactDivisor.mul), so the family of operators indexed by
exact divisors is closed under this composition.
W_R ∘ W_Q = W_{Q R} at coprime exact divisors, on S_k(Γ₀(N)).
The endpoints Q = 1 and Q = N #
At Q = 1 the matrix atkinLehnerMatrix N 1 has determinant 1, so it is an element of
Γ₀(N) (isAtkinLehnerMatrix_one_iff_mem_Gamma0), and a function invariant under Γ₀(N) is
unchanged by the slash.
W_1 is the identity on M_k(Γ₀(N)).
The cusp-form W_1 is the identity on S_k(Γ₀(N)).
The Fricke matrix read as an Atkin–Lehner matrix for Q = N is frickeGL ℝ N. The NeZero
instance that frickeGL asks for is supplied by the positivity hypothesis.
W_N is the Fricke slash on M_k(Γ₀(N)): on underlying functions it is
⇑f ∣[k] frickeGL ℝ N, the slash that frickeOperator performs at level Γ₁(N)
(coe_frickeOperator).
The cusp-form W_N is the Fricke slash on S_k(Γ₀(N)), the slash that
frickeOperatorCusp performs at level Γ₁(N) (coe_frickeOperatorCusp).