Documentation

TauCeti.NumberTheory.ModularForms.AtkinLehner.LevelRaise

The Atkin–Lehner operators on level-raises #

Let Q ∥ N be an exact divisor and W_Q an Atkin–Lehner matrix of level N for Q. Writing N = Q * R with Q and R coprime, a level-raise V_d from a divisor level M splits into its Q-part and its R-part, and so does M. Concretely, suppose

Q = d₁ * e₁ * Q₁,    R = d₂ * e₂ * M',    M = Q₁ * M',    d = d₁ * d₂,

and put e = e₁ * d₂. Then W_Q moves past diag(d, 1) at the cost of exchanging the Q-part d₁ of d for the complementary factor e₁, while the R-part d₂ passes through unchanged:

diag(d, 1) · W_Q = d₁ · (W_{Q₁} · diag(e, 1)),

where W_{Q₁} is an Atkin–Lehner matrix of the lower level M for the exact divisor Q₁ ∥ M. Since the scalar matrix d₁ · I slashes as multiplication by d₁ ^ (k - 2), on a form f on Γ₀(M) this reads

W_Q (V_d f) = d₁⁻¹ · e₁ ^ (k - 1) · V_e (W_{Q₁} f).

At Q = N this is the Fricke identity of TauCeti/NumberTheory/ModularForms/Fricke/OldSpace.lean, and at Q = 1 it is the statement that V_d commutes with the identity.

Main results #

References #

Moving an Atkin–Lehner matrix past a level-raise #

source
theorem TauCeti.IsAtkinLehnerMatrix.exists_scaleGL_mul_atkinLehnerGL {N Q Q₁ M' d₁ e₁ d₂ e₂ : ℕ} {W : Matrix (Fin 2) (Fin 2) ℤ} [NeZero d₁] [NeZero d₂] [NeZero e₁] (hQ : 0 < Q) (hQ₁ : 0 < Q₁) (h : IsAtkinLehnerMatrix N Q W) (hQd : Q = d₁ * e₁ * Q₁) (hN : N = Q * (d₂ * e₂ * M')) :
∃ (W' : Matrix (Fin 2) (Fin 2) ℤ) (hW' : IsAtkinLehnerMatrix (Q₁ * M') Q₁ W'), scaleGL (d₁ * d₂) * atkinLehnerGL hQ h = (Matrix.GeneralLinearGroup.scalar (Fin 2)) (Units.mk0 ↑d₁ ⋯) * (atkinLehnerGL hQ₁ hW' * scaleGL (e₁ * d₂))

An Atkin–Lehner matrix moves past diag(d, 1). Let Q = d₁ * e₁ * Q₁ be a divisor of N = Q * (d₂ * e₂ * M'). For an Atkin–Lehner matrix W of level N for Q there is an Atkin–Lehner matrix W' of level Q₁ * M' for Q₁ with diag(d₁ * d₂, 1) · W = d₁ · (W' · diag(e₁ * d₂, 1)).

The Atkin–Lehner operator on a level-raise #

source
theorem TauCeti.levelRaise_d_mul_M_dvd {N Q Q₁ M' d₁ e₁ d₂ e₂ M d : ℕ} (hQ : Q = d₁ * e₁ * Q₁) (hN : N = Q * (d₂ * e₂ * M')) (hM : M = Q₁ * M') (hd : d = d₁ * d₂) :
d * M ∣ N

The Atkin–Lehner level-raise factorizations make d * M divide N.

source
theorem TauCeti.levelRaise_e_mul_M_dvd {N Q Q₁ M' d₁ e₁ d₂ e₂ M e : ℕ} (hQ : Q = d₁ * e₁ * Q₁) (hN : N = Q * (d₂ * e₂ * M')) (hM : M = Q₁ * M') (he : e = e₁ * d₂) :
e * M ∣ N

The Atkin–Lehner level-raise factorizations make e * M divide N.

source
theorem TauCeti.Nat.IsExactDivisor.atkinLehnerOperator_levelRaise {N Q Q₁ M' d₁ e₁ d₂ e₂ : ℕ} {k : ℤ} {M d e : ℕ} [NeZero d] [NeZero e] (h : IsExactDivisor Q N) (h₁ : IsExactDivisor Q₁ M) (hQ : Q = d₁ * e₁ * Q₁) (hN : N = Q * (d₂ * e₂ * M')) (hM : M = Q₁ * M') (hd : d = d₁ * d₂) (he : e = e₁ * d₂) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 M)) k) :
(h.atkinLehnerOperator k) (ModularForm.levelRaise d ⋯ f) = ((↑d₁)⁻¹ * ↑e₁ ^ (k - 1)) • ModularForm.levelRaise e ⋯ ((h₁.atkinLehnerOperator k) f)

The Atkin–Lehner operator intertwines the level-raises on modular forms. Let Q = d₁ * e₁ * Q₁ be an exact divisor of N = Q * (d₂ * e₂ * M'), and Q₁ an exact divisor of M = Q₁ * M'. For a modular form f on Γ₀(M) and d = d₁ * d₂, e = e₁ * d₂, W_Q (V_d f) = d₁⁻¹ · e₁ ^ (k - 1) · V_e (W_{Q₁} f), where W_Q and W_{Q₁} are the Atkin–Lehner operators of levels N and M. (The exactness h₁ of Q₁ follows from the other hypotheses; it is taken as an argument because it names the operator W_{Q₁}.)

source
theorem TauCeti.Nat.IsExactDivisor.atkinLehnerOperatorCusp_levelRaise {N Q Q₁ M' d₁ e₁ d₂ e₂ : ℕ} {k : ℤ} {M d e : ℕ} [NeZero d] [NeZero e] (h : IsExactDivisor Q N) (h₁ : IsExactDivisor Q₁ M) (hQ : Q = d₁ * e₁ * Q₁) (hN : N = Q * (d₂ * e₂ * M')) (hM : M = Q₁ * M') (hd : d = d₁ * d₂) (he : e = e₁ * d₂) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 M)) k) :
(h.atkinLehnerOperatorCusp k) (CuspForm.levelRaise d ⋯ f) = ((↑d₁)⁻¹ * ↑e₁ ^ (k - 1)) • CuspForm.levelRaise e ⋯ ((h₁.atkinLehnerOperatorCusp k) f)

The Atkin–Lehner operator intertwines the level-raises on cusp forms: under the factorizations of atkinLehnerOperator_levelRaise, W_Q (V_d f) = d₁⁻¹ · e₁ ^ (k - 1) · V_e (W_{Q₁} f) for a cusp form f on Γ₀(M).

source
theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperator_levelRaise {N Q Q₁ M' d₁ e₁ d₂ e₂ : ℕ} {k : ℤ} {M d e : ℕ} [NeZero d] [NeZero e] (h : IsExactDivisor Q N) (h₁ : IsExactDivisor Q₁ M) (hQ : Q = d₁ * e₁ * Q₁) (hN : N = Q * (d₂ * e₂ * M')) (hM : M = Q₁ * M') (hd : d = d₁ * d₂) (he : e = e₁ * d₂) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 M)) k) :
(h.normalizedAtkinLehnerOperator k) (ModularForm.levelRaise d ⋯ f) = (atkinLehnerNormalizer (d₁ * e₁) k * (↑d₁)⁻¹ * ↑e₁ ^ (k - 1)) • ModularForm.levelRaise e ⋯ ((h₁.normalizedAtkinLehnerOperator k) f)

The normalized Atkin–Lehner operator intertwines the level-raises on modular forms: under the factorizations of atkinLehnerOperator_levelRaise, 𝒲_Q (V_d f) = (√(d₁ e₁)) ^ (2 - k) · d₁⁻¹ · e₁ ^ (k - 1) · V_e (𝒲_{Q₁} f).

source
theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerOperatorCusp_levelRaise {N Q Q₁ M' d₁ e₁ d₂ e₂ : ℕ} {k : ℤ} {M d e : ℕ} [NeZero d] [NeZero e] (h : IsExactDivisor Q N) (h₁ : IsExactDivisor Q₁ M) (hQ : Q = d₁ * e₁ * Q₁) (hN : N = Q * (d₂ * e₂ * M')) (hM : M = Q₁ * M') (hd : d = d₁ * d₂) (he : e = e₁ * d₂) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 M)) k) :
(h.normalizedAtkinLehnerOperatorCusp k) (CuspForm.levelRaise d ⋯ f) = (atkinLehnerNormalizer (d₁ * e₁) k * (↑d₁)⁻¹ * ↑e₁ ^ (k - 1)) • CuspForm.levelRaise e ⋯ ((h₁.normalizedAtkinLehnerOperatorCusp k) f)

The normalized Atkin–Lehner operator intertwines the level-raises on cusp forms: under the factorizations of atkinLehnerOperator_levelRaise, 𝒲_Q (V_d f) = (√(d₁ e₁)) ^ (2 - k) · d₁⁻¹ · e₁ ^ (k - 1) · V_e (𝒲_{Q₁} f).