The Atkin–Lehner signs of a newform of trivial nebentypus

For a newform f of level N, weight k and trivial nebentypus and an exact divisor Q ∥ N, the normalized Atkin–Lehner operator 𝒲_Q on S_k(Γ₀(N)) satisfies 𝒲_Q f = ε_Q(f) · f for a sign ε_Q(f) ∈ {1, -1}, the Atkin–Lehner sign (or Atkin–Lehner eigenvalue) of f at Q. The signs are multiplicative on coprime exact divisors, ε_1(f) = 1, and ε_N(f) is the Fricke sign of f, so that the signs at the maximal prime powers p ^ v_p(N) of N multiply to the Fricke eigenvalue. The functional-equation sign of L(s, f) is i^k · ε_N(f).

The argument is the one that gives the Fricke sign, run on the Γ₀(N) carrier the Atkin–Lehner operators live on.

• 𝒲_Q preserves the new subspace at trivial nebentypus. It preserves the old subspace (TauCeti.Nat.IsExactDivisor.ofLe_normalizedAtkinLehnerOperatorCusp_mem_cuspFormsOld) and is Petersson self-adjoint on S_k(Γ₀(N)). Newness of a form of trivial nebentypus is tested against the old forms of trivial nebentypus alone, and the Petersson product of two such forms at level Γ₁(N) is a fixed positive multiple of their product at level Γ₀(N) (CuspForm.peterssonInnerCosets_ofLe_ofLe), so the two pairings detect the same orthogonality.
• On S_k(N, 1) the operator 𝒲_Q commutes with the Hecke operators Tₙ for n prime to Q: it commutes with the action of every double coset of determinant prime to Q (TauCeti.commute_atkinLehnerOperatorCusp_heckeSlashGamma0CuspFormEnd), and those Tₙ lie in the subring such cosets generate (HeckeRing.GL2.commute_map_heckeTCompositeGamma0_of_forall_coprimeDetCoset).
• Multiplicity one, in the form HeckeRing.GL2.exists_eq_smul_of_commute_heckeRingHomCusp_of_mem_cuspFormsNew for a commuting involution: 𝒲_Q f is a good Hecke eigenvector in the new part with the eigenvalues of f, hence a multiple ε • f, and 𝒲_Q ∘ 𝒲_Q = 1 forces ε ^ 2 = 1.

For general nebentypus χ, the operator W_Q conjugates only the Q-part of the character, so it need not preserve S_k(N, χ). The sign statement proved here treats trivial nebentypus.

Main definitions

• TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerCharCuspOneEnd: 𝒲_Q on the trivial-nebentypus space S_k(N, 1), transported from S_k(Γ₀(N)).
• HeckeRing.GL2.Newform.toCuspFormGamma0: a newform of trivial nebentypus, as a cusp form on Γ₀(N).
• HeckeRing.GL2.Newform.atkinLehnerSign: the Atkin–Lehner sign ε_Q(f) of a newform of trivial nebentypus.

Main results

• TauCeti.Nat.IsExactDivisor.ofLe_normalizedAtkinLehnerOperatorCusp_mem_cuspFormsNew: 𝒲_Q preserves the new subspace at trivial nebentypus.
• commute_normalizedAtkinLehnerCharCuspOneEnd_heckeRingHomCuspCharSpace (in the namespace TauCeti.Nat.IsExactDivisor): on S_k(N, 1), 𝒲_Q commutes with Tₙ for every n prime to Q.
• exists_normalizedAtkinLehnerOperatorCusp_eq_smul_of_mem_cuspFormsNew (same namespace): a nonzero form in the new part of S_k(N, 1) that is an eigenvector of every good Tₚ satisfies 𝒲_Q f = ε • f with ε = 1 or ε = -1.
• normalizedAtkinLehnerOperatorCusp_toCuspFormGamma0_eq_atkinLehnerSign_smul and atkinLehnerSign_eq_one_or_neg_one (in the namespace HeckeRing.GL2.Newform): the eigenvalue equation and the sign law of ε_Q(f).
• HeckeRing.GL2.Newform.atkinLehnerSign_mul, HeckeRing.GL2.Newform.atkinLehnerSign_self, HeckeRing.GL2.Newform.prod_atkinLehnerSign_primePow_eq_frickeSign: the signs are multiplicative on coprime exact divisors, ε_N(f) is the Fricke sign, and the signs at the maximal prime powers of N multiply to it.

References

• A. O. L. Atkin and J. Lehner, Hecke operators on Γ₀(m), Math. Ann. 185 (1970), 134–160.
• T. Miyake, Modular forms, Theorem 4.6.15.
• F. Diamond and J. Shurman, A first course in modular forms, §5.10.

𝒲_Q preserves the new subspace at trivial nebentypus

theorem TauCeti.Nat.IsExactDivisor.ofLe_normalizedAtkinLehnerOperatorCusp_mem_cuspFormsNew {N Q : ℕ} [NeZero N] {k : ℤ} (h : IsExactDivisor Q N) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k} (hf : CuspForm.ofLe ⋯ f ∈ cuspFormsNew N k) : CuspForm.ofLe ⋯ ((h.normalizedAtkinLehnerOperatorCusp k) f) ∈ cuspFormsNew N k

The normalized Atkin–Lehner operator preserves the new subspace at trivial nebentypus. For a cusp form f on Γ₀(N) whose restriction to Γ₁(N) is new, the restriction of 𝒲_Q f is again new, for every exact divisor Q ∥ N.

𝒲_Q on S_k(N, 1) and its commutation with the good Hecke operators

noncomputable def TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerCharCuspOneEnd {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) (k : ℤ) : Module.End ℂ ↥(cuspFormCharSpace k 1)

The normalized Atkin–Lehner operator on the trivial-nebentypus space S_k(N, 1): the operator 𝒲_Q of S_k(Γ₀(N)), transported along the identification cuspFormCharSpaceOneEquiv : S_k(N, 1) ≃ S_k(Γ₀(N)).

Equations

• h.normalizedAtkinLehnerCharCuspOneEnd k = (TauCeti.cuspFormCharSpaceOneEquiv N k).symm.conj (h.normalizedAtkinLehnerOperatorCusp k)

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerCharCuspOneEnd_def {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) (k : ℤ) : h.normalizedAtkinLehnerCharCuspOneEnd k = (cuspFormCharSpaceOneEquiv N k).symm.conj (h.normalizedAtkinLehnerOperatorCusp k)

Defining equation for the sealed normalizedAtkinLehnerCharCuspOneEnd: it is the conjugate of 𝒲_Q by the identification S_k(N, 1) ≃ S_k(Γ₀(N)).

@[simp]

theorem TauCeti.Nat.IsExactDivisor.normalizedAtkinLehnerCharCuspOneEnd_apply {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) (k : ℤ) (f : ↥(cuspFormCharSpace k 1)) : (h.normalizedAtkinLehnerCharCuspOneEnd k) f = (cuspFormCharSpaceOneEquiv N k).symm ((h.normalizedAtkinLehnerOperatorCusp k) ((cuspFormCharSpaceOneEquiv N k) f))

normalizedAtkinLehnerCharCuspOneEnd moves a form to S_k(Γ₀(N)), applies 𝒲_Q and moves back.

theorem TauCeti.Nat.IsExactDivisor.cuspFormCharSpaceOneEquiv_normalizedAtkinLehnerCharCuspOneEnd_apply {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) (k : ℤ) (f : ↥(cuspFormCharSpace k 1)) : (cuspFormCharSpaceOneEquiv N k) ((h.normalizedAtkinLehnerCharCuspOneEnd k) f) = (h.normalizedAtkinLehnerOperatorCusp k) ((cuspFormCharSpaceOneEquiv N k) f)

Read on S_k(Γ₀(N)), normalizedAtkinLehnerCharCuspOneEnd is 𝒲_Q. Not a simp lemma: simp derives it from normalizedAtkinLehnerCharCuspOneEnd_apply.

theorem TauCeti.Nat.IsExactDivisor.coe_normalizedAtkinLehnerCharCuspOneEnd_apply {N Q : ℕ} [NeZero N] (h : IsExactDivisor Q N) (k : ℤ) (f : ↥(cuspFormCharSpace k 1)) : ↑((h.normalizedAtkinLehnerCharCuspOneEnd k) f) = CuspForm.ofLe ⋯ ((h.normalizedAtkinLehnerOperatorCusp k) ((cuspFormCharSpaceOneEquiv N k) f))

On underlying cusp forms of level Γ₁(N), normalizedAtkinLehnerCharCuspOneEnd is the restriction of 𝒲_Q applied on S_k(Γ₀(N)). Not a simp lemma: simp derives it from normalizedAtkinLehnerCharCuspOneEnd_apply.

theorem TauCeti.Nat.IsExactDivisor.commute_normalizedAtkinLehnerCharCuspOneEnd_heckeRingHomCuspCharSpace {N Q : ℕ} [NeZero N] {k : ℤ} (h : IsExactDivisor Q N) {n : ℕ} (hn : n.Coprime Q) : Commute (h.normalizedAtkinLehnerCharCuspOneEnd k) ((HeckeRing.GL2.heckeRingHomCuspCharSpace k 1) (HeckeRing.GL2.heckeTCompositeGamma0 N n))

The normalized Atkin–Lehner operator commutes with the Hecke operators away from Q on S_k(N, 1): for n prime to Q, 𝒲_Q Tₙ = Tₙ 𝒲_Q. Such Tₙ lie in the subring generated by the double cosets of determinant prime to Q, each of which commutes with 𝒲_Q. In particular 𝒲_Q commutes with every good Hecke operator, n prime to N.

The Atkin–Lehner sign

theorem TauCeti.Nat.IsExactDivisor.exists_normalizedAtkinLehnerOperatorCusp_eq_smul_of_mem_cuspFormsNew {N Q : ℕ} [NeZero N] {k : ℤ} (h : IsExactDivisor Q N) {f : ↥(cuspFormCharSpace k 1)} (ha : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((HeckeRing.GL2.heckeRingHomCuspCharSpace k 1) (HeckeRing.GL2.heckeTCompositeGamma0 N p)) f = c • f) (hf : ↑f ∈ cuspFormsNew N k) (hf0 : ↑f ≠ 0) : ∃ (ε : ℂ), (ε = 1 ∨ ε = -1) ∧ (h.normalizedAtkinLehnerOperatorCusp k) ((cuspFormCharSpaceOneEquiv N k) f) = ε • (cuspFormCharSpaceOneEquiv N k) f

The Atkin–Lehner sign: a nonzero cusp form in the new part of S_k(N, 1) that is an eigenvector of Tₚ at every prime p ∤ N is, read on S_k(Γ₀(N)), an eigenvector of the normalized Atkin–Lehner operator 𝒲_Q, with eigenvalue 1 or -1.

A newform of trivial nebentypus on Γ₀(N)

noncomputable def HeckeRing.GL2.Newform.toCuspFormGamma0 {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)) k

A newform of trivial nebentypus, as a cusp form on Γ₀(N): the same function on ℍ, re-read as a form for the bare group Γ₀(N) under the identification S_k(N, 1) ≃ S_k(Γ₀(N)). This is the carrier on which the Atkin–Lehner operators act.

Equations

• f.toCuspFormGamma0 hχ = (TauCeti.cuspFormCharSpaceOneEquiv N k) ⟨f.toCuspForm, ⋯⟩

@[simp]

theorem HeckeRing.GL2.Newform.coe_toCuspFormGamma0 {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) : ⇑(f.toCuspFormGamma0 hχ) = ⇑f.toCuspForm

toCuspFormGamma0 does not change the underlying function on ℍ.

@[simp]

theorem HeckeRing.GL2.Newform.ofLe_toCuspFormGamma0 {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) : CuspForm.ofLe ⋯ (f.toCuspFormGamma0 hχ) = f.toCuspForm

Restricting toCuspFormGamma0 back to Γ₁(N) recovers the newform.

theorem HeckeRing.GL2.Newform.toCuspFormGamma0_ne_zero {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) : f.toCuspFormGamma0 hχ ≠ 0

A newform of trivial nebentypus is nonzero on Γ₀(N).

The Atkin–Lehner signs

theorem HeckeRing.GL2.Newform.exists_normalizedAtkinLehnerOperatorCusp_toCuspFormGamma0_eq_smul {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (h : TauCeti.Nat.IsExactDivisor Q N) : ∃ (ε : ℂ), (ε = 1 ∨ ε = -1) ∧ (h.normalizedAtkinLehnerOperatorCusp k) (f.toCuspFormGamma0 hχ) = ε • f.toCuspFormGamma0 hχ

The Atkin–Lehner sign of a newform of trivial nebentypus exists: 𝒲_Q f = ε • f with ε = 1 or ε = -1, for every exact divisor Q ∥ N.

noncomputable def HeckeRing.GL2.Newform.atkinLehnerSign {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (h : TauCeti.Nat.IsExactDivisor Q N) : ℂ

The Atkin–Lehner sign ε_Q(f) of a newform of trivial nebentypus at an exact divisor Q ∥ N: the eigenvalue of the normalized Atkin–Lehner operator 𝒲_Q on f.

Equations

• f.atkinLehnerSign hχ h = ⋯.choose

theorem HeckeRing.GL2.Newform.normalizedAtkinLehnerOperatorCusp_toCuspFormGamma0_eq_atkinLehnerSign_smul {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (h : TauCeti.Nat.IsExactDivisor Q N) : (h.normalizedAtkinLehnerOperatorCusp k) (f.toCuspFormGamma0 hχ) = f.atkinLehnerSign hχ h • f.toCuspFormGamma0 hχ

The normalized Atkin–Lehner operator acts on a trivial-nebentypus newform by its Atkin–Lehner sign.

theorem HeckeRing.GL2.Newform.atkinLehnerSign_eq_one_or_neg_one {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (h : TauCeti.Nat.IsExactDivisor Q N) : f.atkinLehnerSign hχ h = 1 ∨ f.atkinLehnerSign hχ h = -1

The Atkin–Lehner sign of a trivial-nebentypus newform is 1 or -1.

theorem HeckeRing.GL2.Newform.atkinLehnerSign_eq_of_normalizedAtkinLehnerOperatorCusp_eq_smul {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (h : TauCeti.Nat.IsExactDivisor Q N) {ε : ℂ} (hε : (h.normalizedAtkinLehnerOperatorCusp k) (f.toCuspFormGamma0 hχ) = ε • f.toCuspFormGamma0 hχ) : f.atkinLehnerSign hχ h = ε

A scalar satisfying the normalized Atkin–Lehner eigenvalue equation is the Atkin–Lehner sign.

theorem HeckeRing.GL2.Newform.atkinLehnerSign_congr {N Q : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) {Q' : ℕ} (h : TauCeti.Nat.IsExactDivisor Q N) (h' : TauCeti.Nat.IsExactDivisor Q' N) (e : Q = Q') : f.atkinLehnerSign hχ h = f.atkinLehnerSign hχ h'

The Atkin–Lehner sign depends only on the divisor, not on the proof that it is exact.

@[simp]

theorem HeckeRing.GL2.Newform.atkinLehnerSign_one {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (h : TauCeti.Nat.IsExactDivisor 1 N) : f.atkinLehnerSign hχ h = 1

The sign at Q = 1 is 1, 𝒲_1 being the identity.

theorem HeckeRing.GL2.Newform.atkinLehnerSign_mul {N Q R : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (hQ : TauCeti.Nat.IsExactDivisor Q N) (hR : TauCeti.Nat.IsExactDivisor R N) (hQR : Q.Coprime R) : f.atkinLehnerSign hχ ⋯ = f.atkinLehnerSign hχ hQ * f.atkinLehnerSign hχ hR

The signs are multiplicative on coprime exact divisors: ε_{Q R}(f) = ε_Q(f) ε_R(f) when Q and R are coprime, since 𝒲_R ∘ 𝒲_Q = 𝒲_{Q R}.

@[simp]

theorem HeckeRing.GL2.Newform.atkinLehnerSign_self {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (h : TauCeti.Nat.IsExactDivisor N N) : f.atkinLehnerSign hχ h = f.frickeSign hχ

The sign at Q = N is the Fricke sign: 𝒲_N is the normalized Fricke operator, read on Γ₀(N).

theorem HeckeRing.GL2.Newform.atkinLehnerSign_prodPrimePow {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) (s : Finset ℕ) : f.atkinLehnerSign hχ ⋯ = ∏ p ∈ s, f.atkinLehnerSign hχ ⋯

The sign at an exact divisor is the product of the signs at its maximal prime powers: ε_{∏ p ∈ s, p ^ v_p(N)}(f) = ∏ p ∈ s, ε_{p ^ v_p(N)}(f) for every finite set s of naturals; an index outside N.primeFactors has exponent 0 and contributes ε_1(f) = 1.

theorem HeckeRing.GL2.Newform.prod_atkinLehnerSign_primePow_eq_frickeSign {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) : ∏ p ∈ N.primeFactors, f.atkinLehnerSign hχ ⋯ = f.frickeSign hχ

The Atkin–Lehner signs multiply to the Fricke sign: ∏_{p ∣ N} ε_{p ^ v_p(N)}(f) = ε_N(f).