Satake parameters and Satake angles of a newform

Let f be a newform of level N, weight k and nebentypus χ, with χ extended by zero to the integers not coprime to N (HeckeRing.GL2.Newform.dirichletLift). Its Euler factor at a prime p is 1 - a_p p^{-s} + χ(p) p^{k-1-2s}. The Satake parameters of f at p are the two roots α_p, β_p, counted with multiplicity, of X² - a_p X + χ(p) p^{k-1}; equivalently they are characterised by

α_p + β_p = a_p and α_p β_p = χ(p) p^{k-1},

and they factor the Euler factor as (1 - α_p p^{-s}) (1 - β_p p^{-s}). They form an unordered pair, recorded as a multiset of cardinality two, and are defined at every p with no hypotheses: at a prime dividing the level they are a_p and 0, the Euler factor being linear there, and at a prime not dividing it both are nonzero.

A single Satake angle is canonical only when the normalized coefficient is real. At a prime p with χ(p) = 1 — for instance any prime not dividing the level when the nebentypus is trivial — the coefficient a_p is real, because the Petersson adjoint of T_p is χ(p)⁻¹ T_p (HeckeRing.GL2.Newform.qExpansion_coeff_eq_dirichletLift_mul_conj). More generally, the angle API takes the reality of a_p as an explicit hypothesis. Under the Ramanujan–Deligne bound |a_p| ≤ 2 p^{(k-1)/2}, also explicit since it is not proved here, there is then a unique θ_p ∈ [0, π] with a_p = 2 p^{(k-1)/2} cos θ_p. When moreover χ(p) = 1, the Satake parameters are p^{(k-1)/2} e^{± i θ_p}. The angle equals arccos (Re a_p / (2 p^{(k-1)/2})).

The parameters are taken in the arithmetic normalisation of the coefficients a_p, rather than in the unitary normalisation a_p / p^{(k-1)/2}: at a prime with χ(p) = 1 (so not dividing the level) and under the Ramanujan–Deligne bound, both have absolute value p^{(k-1)/2} (HeckeRing.GL2.Newform.satakeParameters_eq_exp_satakeAngle).

Main definitions

• HeckeRing.GL2.Newform.satakeParameters: the Satake parameters of a newform at p.
• HeckeRing.GL2.Newform.satakeAngle: the Satake angle of a newform at a prime p where a_p is real, under the Ramanujan–Deligne bound.

Main results

• HeckeRing.GL2.Newform.satakeParameters_eq_pair_iff: {α, β} are the Satake parameters at p exactly when α + β = a_p and α β = χ(p) p^{k-1}.
• HeckeRing.GL2.Newform.mem_satakeParameters_iff: the Satake parameters are the roots of X² - a_p X + χ(p) p^{k-1}.
• HeckeRing.GL2.Newform.prod_map_one_sub_mul_satakeParameters: they factor the Euler factor at p, and HeckeRing.GL2.Newform.LSeries_eulerProduct_hasProd_satakeParameters writes the Euler product of L(s, f) through them.
• HeckeRing.GL2.Newform.qExpansion_coeff_eq_dirichletLift_mul_conj: a_p = χ(p) · conj a_p at a prime not dividing the level.
• HeckeRing.GL2.Newform.qExpansion_coeff_eq_two_mul_rpow_mul_cos_satakeAngle: when a_p is real and satisfies the Ramanujan–Deligne bound, a_p = 2 p^{(k-1)/2} cos θ_p, and HeckeRing.GL2.Newform.satakeAngle_eq_of_qExpansion_coeff_eq says that θ_p is the only angle in [0, π] with this property; HeckeRing.GL2.Newform.satakeAngle_eq_arccos computes it as arccos (Re a_p / (2 p^{(k-1)/2})).
• HeckeRing.GL2.Newform.satakeParameters_eq_exp_satakeAngle: when moreover χ(p) = 1, the Satake parameters are p^{(k-1)/2} e^{± i θ_p}.

References

• F. Diamond and J. Shurman, A first course in modular forms, §5.9.
• H. Iwaniec and E. Kowalski, Analytic Number Theory, §5.1.

noncomputable def HeckeRing.GL2.Newform.satakeParameters {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) : Multiset ℂ

The Satake parameters of a newform f at a prime p: the roots, counted with multiplicity, of X² - a_p X + χ(p) p^{k-1}, where a_p is the p-th Fourier coefficient of f and the nebentypus χ is extended by zero to the integers not coprime to the level. This is a multiset of cardinality two (card_satakeParameters). The definition is stated for every natural number p, but carries arithmetic meaning only for primes.

Equations

• One or more equations did not get rendered due to their size.

theorem HeckeRing.GL2.Newform.satakeParameters_def {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) : f.satakeParameters p = (Polynomial.X ^ 2 - Polynomial.C ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) * Polynomial.X + Polynomial.C (f.dirichletLift ↑p * ↑p ^ (k - 1))).roots

The definition of the Satake parameters as the roots of X² - a_p X + χ(p) p^{k-1}.

theorem HeckeRing.GL2.Newform.satakeParameters_eq_pair_iff {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) {α β : ℂ} : f.satakeParameters p = {α, β} ↔ α + β = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) ∧ α * β = f.dirichletLift ↑p * ↑p ^ (k - 1)

The Satake parameters are characterised by their sum and product: {α, β} are the Satake parameters of f at p exactly when α + β = a_p and α β = χ(p) p^{k-1}.

theorem HeckeRing.GL2.Newform.exists_satakeParameters_eq_pair {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) : ∃ (α : ℂ) (β : ℂ), f.satakeParameters p = {α, β}

The Satake parameters at p form an unordered pair.

@[simp]

theorem HeckeRing.GL2.Newform.card_satakeParameters {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) : (f.satakeParameters p).card = 2

There are two Satake parameters at p, counted with multiplicity.

@[simp]

theorem HeckeRing.GL2.Newform.mem_satakeParameters_iff {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) (z : ℂ) : z ∈ f.satakeParameters p ↔ z ^ 2 - (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * z + f.dirichletLift ↑p * ↑p ^ (k - 1) = 0

The Satake parameters at p are the roots of X² - a_p X + χ(p) p^{k-1}.

@[simp]

theorem HeckeRing.GL2.Newform.sum_satakeParameters {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) : (f.satakeParameters p).sum = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

The Satake parameters at p sum to the Fourier coefficient a_p.

@[simp]

theorem HeckeRing.GL2.Newform.prod_satakeParameters {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) : (f.satakeParameters p).prod = f.dirichletLift ↑p * ↑p ^ (k - 1)

The product of the Satake parameters at p is χ(p) p^{k-1}.

theorem HeckeRing.GL2.Newform.prod_map_one_sub_mul_satakeParameters {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (p : ℕ) (x : ℂ) : (Multiset.map (fun (α : ℂ) => 1 - α * x) (f.satakeParameters p)).prod = 1 - (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) * x + f.dirichletLift ↑p * ↑p ^ (k - 1) * x ^ 2

The Satake parameters factor the Euler factor: (1 - α_p x) (1 - β_p x) = 1 - a_p x + χ(p) p^{k-1} x².

theorem HeckeRing.GL2.Newform.satakeParameters_of_not_coprime {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hpN : ¬p.Coprime N) : f.satakeParameters p = {(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm), 0}

At a prime dividing the level, where the extended nebentypus vanishes, the Satake parameters are a_p and 0.

theorem HeckeRing.GL2.Newform.zero_notMem_satakeParameters {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : p ≠ 0) (hpN : p.Coprime N) : 0 ∉ f.satakeParameters p

At a nonzero p coprime to the level, the Satake parameters are nonzero.

theorem HeckeRing.GL2.Newform.LSeries_eulerProduct_hasProd_satakeParameters {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {s : ℂ} (hs : ↑k / 2 + 1 < s.re) : HasProd (fun (p : Nat.Primes) => (Multiset.map (fun (α : ℂ) => 1 - α * ↑↑p ^ (-s)) (f.satakeParameters ↑p)).prod⁻¹) (LSeries (fun (n : ℕ) => (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) s)

The Euler product through the Satake parameters: for Re s > k/2 + 1, L(s, f) = ∏_p ((1 - α_p p^{-s}) (1 - β_p p^{-s}))⁻¹.

The Satake angle

theorem HeckeRing.GL2.Newform.qExpansion_coeff_eq_dirichletLift_mul_conj {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hpN : p.Coprime N) : (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = f.dirichletLift ↑p * (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm))

The coefficients of a newform are real up to the nebentypus: at a prime p ∤ N, a_p = χ(p) · conj a_p. In particular a_p is real when χ(p) = 1.

theorem HeckeRing.GL2.Newform.conj_qExpansion_coeff_eq_self_of_dirichletLift_eq_one {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hχ : f.dirichletLift ↑p = 1) : (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

At a prime with χ(p) = 1, the p-th coefficient of a newform is real.

theorem HeckeRing.GL2.Newform.exists_qExpansion_coeff_eq_two_mul_rpow_mul_cos {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hreal : (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) (hR : ‖(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)‖ ≤ 2 * ↑p ^ ((↑k - 1) / 2)) : ∃ θ ∈ Set.Icc 0 Real.pi, (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = ↑(2 * ↑p ^ ((↑k - 1) / 2) * Real.cos θ)

When a_p is real and satisfies the Ramanujan–Deligne bound |a_p| ≤ 2 p^{(k-1)/2}, there is an angle θ ∈ [0, π] with a_p = 2 p^{(k-1)/2} cos θ.

noncomputable def HeckeRing.GL2.Newform.satakeAngle {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (_hp : Nat.Prime p) (_hreal : (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) (_hR : ‖(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)‖ ≤ 2 * ↑p ^ ((↑k - 1) / 2)) : ℝ

The Satake angle of a newform f at a prime p where a_p is real, under the Ramanujan–Deligne bound |a_p| ≤ 2 p^{(k-1)/2}: the unique θ_p ∈ [0, π] with a_p = 2 p^{(k-1)/2} cos θ_p (qExpansion_coeff_eq_two_mul_rpow_mul_cos_satakeAngle, satakeAngle_eq_of_qExpansion_coeff_eq). It is arccos (Re a_p / (2 p^{(k-1)/2})) (satakeAngle_eq_arccos).

Equations

• f.satakeAngle _hp _hreal _hR = Real.arccos (((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)).re / (2 * ↑p ^ ((↑k - 1) / 2)))

theorem HeckeRing.GL2.Newform.satakeAngle_nonneg {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hreal : (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) (hR : ‖(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)‖ ≤ 2 * ↑p ^ ((↑k - 1) / 2)) : 0 ≤ f.satakeAngle hp hreal hR

The Satake angle is nonnegative.

theorem HeckeRing.GL2.Newform.satakeAngle_le_pi {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hreal : (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) (hR : ‖(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)‖ ≤ 2 * ↑p ^ ((↑k - 1) / 2)) : f.satakeAngle hp hreal hR ≤ Real.pi

The Satake angle is at most π.

theorem HeckeRing.GL2.Newform.qExpansion_coeff_eq_two_mul_rpow_mul_cos_satakeAngle {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hreal : (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) (hR : ‖(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)‖ ≤ 2 * ↑p ^ ((↑k - 1) / 2)) : (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = ↑(2 * ↑p ^ ((↑k - 1) / 2) * Real.cos (f.satakeAngle hp hreal hR))

The Satake angle for a real coefficient: under the Ramanujan–Deligne bound |a_p| ≤ 2 p^{(k-1)/2}, the coefficient is a_p = 2 p^{(k-1)/2} cos θ_p.

theorem HeckeRing.GL2.Newform.satakeAngle_eq_of_qExpansion_coeff_eq {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hreal : (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) (hR : ‖(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)‖ ≤ 2 * ↑p ^ ((↑k - 1) / 2)) {θ : ℝ} (hθ₀ : 0 ≤ θ) (hθπ : θ ≤ Real.pi) (h : (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) = ↑(2 * ↑p ^ ((↑k - 1) / 2) * Real.cos θ)) : f.satakeAngle hp hreal hR = θ

The Satake angle is the only angle in [0, π] with a_p = 2 p^{(k-1)/2} cos θ.

@[simp]

theorem HeckeRing.GL2.Newform.satakeAngle_eq_arccos {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hreal : (starRingEnd ℂ) ((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) = (PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)) (hR : ‖(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)‖ ≤ 2 * ↑p ^ ((↑k - 1) / 2)) : f.satakeAngle hp hreal hR = Real.arccos (((PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)).re / (2 * ↑p ^ ((↑k - 1) / 2)))

The Satake angle is arccos (Re a_p / (2 p^{(k-1)/2})).

theorem HeckeRing.GL2.Newform.satakeParameters_eq_exp_satakeAngle {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) {p : ℕ} (hp : Nat.Prime p) (hR : ‖(PowerSeries.coeff p) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)‖ ≤ 2 * ↑p ^ ((↑k - 1) / 2)) (hχ : f.dirichletLift ↑p = 1) : f.satakeParameters p = {↑(↑p ^ ((↑k - 1) / 2)) * Complex.exp (↑(f.satakeAngle hp ⋯ hR) * Complex.I), ↑(↑p ^ ((↑k - 1) / 2)) * Complex.exp (-↑(f.satakeAngle hp ⋯ hR) * Complex.I)}

The Satake parameters at a prime with χ(p) = 1: under the Ramanujan–Deligne bound they are the complex conjugates p^{(k-1)/2} e^{± i θ_p}. Here a_p is real by conj_qExpansion_coeff_eq_self_of_dirichletLift_eq_one.