Documentation

TauCeti.NumberTheory.ModularForms.AtkinLehner.Newform

Atkin–Lehner transport of newforms #

For an exact divisor Q of N, slashing a newform by an Atkin–Lehner matrix gives a nonzero new eigenvector. Its first Fourier coefficient is therefore nonzero, and dividing by that coefficient gives a uniquely determined normalized newform. Its nebentypus is χ ∘ ι_Q, where ι_Q inverts the residue modulo Q and fixes the residue modulo N / Q. Its good-prime coefficient at p is χ(u)⁻¹ a_p(f), where the CRT unit u has components p modulo Q and 1 modulo N / Q. If χ = ψ φ is split along these two moduli, this is ψ(p)⁻¹ a_p(f).

HeckeRing.GL2.Newform.atkinLehnerTransform constructs this normalized newform from the exact divisor using the canonical matrix. The equation atkinLehnerNormalizer_smul_atkinLehnerOperatorGamma1Cusp_eq_smul identifies the scalar relating it to the Petersson-normalized slash, without asserting that this scalar has modulus one. The characterization atkinLehnerTransform_eq_iff uniquely identifies the newform on that line and makes it independent of the choice of Atkin–Lehner matrix.

The construction uses the good-prime Hecke intertwining relation, newspace stability, and HeckeRing.GL2.Newform.ofForallPrime to normalize a new eigenvector.

References #

source
theorem HeckeRing.GL2.Newform.atkinLehnerOperatorGamma1Cusp_ne_zero {N Q : ℕ} [NeZero N] {k : ℤ} {W : Matrix (Fin 2) (Fin 2) ℤ} (f : Newform N k) (hQ : 0 < Q) (hQN : Q ∣ N) (hW : TauCeti.IsAtkinLehnerMatrix N Q W) :
(TauCeti.atkinLehnerOperatorGamma1Cusp hQ hQN hW k) f.toCuspForm ≠ 0

The Atkin–Lehner slash of a newform is nonzero.

source
theorem HeckeRing.GL2.Newform.qExpansion_coeff_one_atkinLehnerOperatorGamma1Cusp_ne_zero {N Q : ℕ} [NeZero N] {k : ℤ} {W : Matrix (Fin 2) (Fin 2) ℤ} (f : Newform N k) (hQ : 0 < Q) (hQN : Q ∣ N) (hW : TauCeti.IsAtkinLehnerMatrix N Q W) :
(PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑((TauCeti.atkinLehnerOperatorGamma1Cusp hQ hQN hW k) f.toCuspForm)) ≠ 0

The first Fourier coefficient of the Atkin–Lehner slash of a newform is nonzero. Thus the slash can be normalized without changing its eigenline.

source
noncomputable def HeckeRing.GL2.Newform.atkinLehnerTransform {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) :
Newform N k

The normalized newform on the Atkin–Lehner image line of f for the exact divisor Q. It uses atkinLehnerMatrix N Q; arbitrary matrices give the same normalized slash.

Instances For
    source
    theorem HeckeRing.GL2.Newform.toCuspForm_atkinLehnerTransform {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) :
    (f.atkinLehnerTransform h).toCuspForm = ((PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑((TauCeti.atkinLehnerOperatorGamma1Cusp ⋯ ⋯ ⋯ k) f.toCuspForm)))⁻¹ • (TauCeti.atkinLehnerOperatorGamma1Cusp ⋯ ⋯ ⋯ k) f.toCuspForm

    The cusp form underlying Atkin–Lehner transport is the canonical normalized slash.

    source
    theorem HeckeRing.GL2.Newform.toCuspForm_atkinLehnerTransform_of_isAtkinLehnerMatrix {N Q : ℕ} [NeZero N] {k : ℤ} {W : Matrix (Fin 2) (Fin 2) ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) (hW : TauCeti.IsAtkinLehnerMatrix N Q W) :
    (f.atkinLehnerTransform h).toCuspForm = ((PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑((TauCeti.atkinLehnerOperatorGamma1Cusp ⋯ ⋯ hW k) f.toCuspForm)))⁻¹ • (TauCeti.atkinLehnerOperatorGamma1Cusp ⋯ ⋯ hW k) f.toCuspForm

    Every Atkin–Lehner matrix gives the canonical transported newform after normalization.

    source
    @[simp]
    theorem HeckeRing.GL2.Newform.χ_atkinLehnerTransform {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) :
    (f.atkinLehnerTransform h).χ = f.χ.comp ↑h.unitsInvPart

    Atkin–Lehner transport inverts the Q-part of the nebentypus.

    source
    theorem HeckeRing.GL2.Newform.atkinLehnerNormalizer_smul_atkinLehnerOperatorGamma1Cusp_eq_smul {N Q : ℕ} [NeZero N] {k : ℤ} {W : Matrix (Fin 2) (Fin 2) ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) (hW : TauCeti.IsAtkinLehnerMatrix N Q W) :
    TauCeti.atkinLehnerNormalizer Q k • (TauCeti.atkinLehnerOperatorGamma1Cusp ⋯ ⋯ hW k) f.toCuspForm = (TauCeti.atkinLehnerNormalizer Q k * (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑((TauCeti.atkinLehnerOperatorGamma1Cusp ⋯ ⋯ hW k) f.toCuspForm))) • (f.atkinLehnerTransform h).toCuspForm

    The Petersson-normalized slash by any matrix is its first Fourier coefficient times the canonical transported newform. This specifies the scalar without a modulus-one claim.

    source
    theorem HeckeRing.GL2.Newform.atkinLehnerTransform_eq_iff {N Q : ℕ} [NeZero N] {k : ℤ} {W : Matrix (Fin 2) (Fin 2) ℤ} (f g : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) (hW : TauCeti.IsAtkinLehnerMatrix N Q W) :
    f.atkinLehnerTransform h = g ↔ ∃ (c : ℂ), (TauCeti.atkinLehnerOperatorGamma1Cusp ⋯ ⋯ hW k) f.toCuspForm = c • g.toCuspForm

    A newform is the canonical Atkin–Lehner transform exactly when its line contains the slash by any chosen Atkin–Lehner matrix. Normalization determines the newform uniquely.

    source
    @[simp]
    theorem HeckeRing.GL2.Newform.atkinLehnerTransform_one {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor 1 N) :
    f.atkinLehnerTransform h = f

    Atkin–Lehner transport at the exact divisor 1 fixes every newform.

    source
    @[simp]
    theorem HeckeRing.GL2.Newform.atkinLehnerTransform_atkinLehnerTransform {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) :
    (f.atkinLehnerTransform h).atkinLehnerTransform h = f

    Transporting twice by the same exact divisor fixes every newform.

    source
    @[simp]
    theorem HeckeRing.GL2.Newform.eigenvalue_atkinLehnerTransform {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) :
    (f.atkinLehnerTransform h).eigenvalue ⟨p, ⋯⟩ hpN = (↑(f.χ (h.unitsEquivProd.symm (ZMod.unitOfCoprime p ⋯, 1))))⁻¹ * f.eigenvalue ⟨p, ⋯⟩ hpN

    At a good prime p, transport multiplies the Hecke eigenvalue by the inverse of f.χ at the CRT unit with components p modulo Q and 1 modulo N / Q.

    source
    theorem HeckeRing.GL2.Newform.qExpansion_coeff_prime_atkinLehnerTransform {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) :
    (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑(f.atkinLehnerTransform h).toCuspForm) = (↑(f.χ (h.unitsEquivProd.symm (ZMod.unitOfCoprime p ⋯, 1))))⁻¹ * (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

    At a good prime p, transport multiplies the Fourier coefficient by the inverse of f.χ at the CRT unit with components p modulo Q and 1 modulo N / Q.

    source
    theorem HeckeRing.GL2.Newform.qExpansion_coeff_prime_atkinLehnerTransform_of_split {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (h : TauCeti.Nat.IsExactDivisor Q N) (ψ : (ZMod Q)ˣ →* ℂˣ) (φ : (ZMod (N / Q))ˣ →* ℂˣ) (hχ : f.χ = ψ.comp (ZMod.unitsMap ⋯) * φ.comp (ZMod.unitsMap ⋯)) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) :
    (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑(f.atkinLehnerTransform h).toCuspForm) = (↑(ψ (ZMod.unitOfCoprime p ⋯)))⁻¹ * (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

    If the nebentypus is ψ φ along N = Q · (N / Q), the Fourier coefficient of the transported newform at a good prime p is ψ(p)⁻¹ a_p(f).