The Atkin–Lehner normalizing constant

The raw weight-k slash by an Atkin–Lehner matrix for a divisor Q of the level is not an involution: the matrix squares to Q times an element of Γ₀(N), so the slash squares to the scalar Q ^ (k - 2). The arithmetic normalization divides that away by multiplying the slash by

atkinLehnerNormalizer Q k = (√Q) ^ (2 - k),

whose square is Q ^ (2 - k) (TauCeti.atkinLehnerNormalizer_sq). The constant depends only on the divisor and the weight, so it is isolated here, away from any modular form: the Fricke operator — the member Q = N of the Atkin–Lehner family — is normalized by it just as the general 𝒲_Q is.

The square root is taken in ℝ and cast to ℂ, rather than as a complex power, so that no branch of (·) ^ (2 - k) has to be chosen.

Main definitions

• TauCeti.atkinLehnerNormalizer: the constant (√Q) ^ (2 - k).

Main results

• TauCeti.atkinLehnerNormalizer_sq: it squares to Q ^ (2 - k).
• TauCeti.atkinLehnerNormalizer_sq_mul: consequently it cancels the scalar Q ^ (k - 2) that the raw slash squares to.
• TauCeti.atkinLehnerNormalizer_mul: it is multiplicative in the divisor, which is what makes the normalized operators multiply the way the raw ones do.
• TauCeti.atkinLehnerNormalizer_one: at Q = 1 it is 1.
• TauCeti.conj_atkinLehnerNormalizer: it is real, so complex conjugation fixes it; this is what lets the normalized operators be Petersson-unitary.

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.

noncomputable def TauCeti.atkinLehnerNormalizer (Q : ℕ) (k : ℤ) : ℂ

The constant (√Q) ^ (2 - k) by which the raw Atkin–Lehner slash for the divisor Q is multiplied, so that the normalized operator squares to 1 rather than to Q ^ (k - 2).

Equations

• TauCeti.atkinLehnerNormalizer Q k = ↑√↑Q ^ (2 - k)

theorem TauCeti.atkinLehnerNormalizer_def (Q : ℕ) (k : ℤ) : atkinLehnerNormalizer Q k = ↑√↑Q ^ (2 - k)

Defining equation for atkinLehnerNormalizer: it is (√Q) ^ (2 - k).

theorem TauCeti.atkinLehnerNormalizer_ne_zero {Q : ℕ} (hQ : Q ≠ 0) (k : ℤ) : atkinLehnerNormalizer Q k ≠ 0

atkinLehnerNormalizer Q k is nonzero, which is what makes the normalized operator a bijection and lets the normalization be undone.

theorem TauCeti.atkinLehnerNormalizer_sq {Q : ℕ} (hQ : Q ≠ 0) (k : ℤ) : atkinLehnerNormalizer Q k ^ 2 = ↑Q ^ (2 - k)

The normalizer squares to Q ^ (2 - k).

theorem TauCeti.atkinLehnerNormalizer_sq_mul {Q : ℕ} (hQ : Q ≠ 0) (k : ℤ) : atkinLehnerNormalizer Q k ^ 2 * ↑Q ^ (k - 2) = 1

The normalization cancels the scalar the raw slash squares to. Multiplying Q ^ (k - 2) by the square of the normalizer leaves 1; this single identity is the whole arithmetic content of the normalization.

@[simp]

theorem TauCeti.atkinLehnerNormalizer_mul (Q R : ℕ) (k : ℤ) : atkinLehnerNormalizer (Q * R) k = atkinLehnerNormalizer Q k * atkinLehnerNormalizer R k

The normalizer is multiplicative in the divisor, because the square root is: √(Q R) is √Q · √R. This is what lets the composition law of the Atkin–Lehner operators be read off from the composition law of the raw slashes.

@[simp]

theorem TauCeti.atkinLehnerNormalizer_one (k : ℤ) : atkinLehnerNormalizer 1 k = 1

At Q = 1 the normalizer is 1, matching the raw slash by an element of Γ₀(N) being the identity.

@[simp]

theorem TauCeti.conj_atkinLehnerNormalizer (Q : ℕ) (k : ℤ) : (starRingEnd ℂ) (atkinLehnerNormalizer Q k) = atkinLehnerNormalizer Q k

The normalizer is real: it is a power of the real number √Q, so complex conjugation fixes it. The Petersson product is conjugate-linear in one argument, so this is what makes the scalar a normalized operator contributes to ⟪𝒲 f, 𝒲 g⟫ the square of the normalizer.