Documentation

TauCeti.NumberTheory.ModularForms.Newforms.Conjugate

The conjugate of a newform #

The conjugate form f_ρ(τ) = conj (f (-conj τ)) has the complex-conjugate q-expansion coefficients, and carries S_k(N, χ) to S_k(N, χ⁻¹) intertwining the Hecke operators (TauCeti/NumberTheory/ModularForms/Conjugate.lean). This file shows that it also preserves the old and the new subspaces of S_k(Γ₁(N)): it commutes with the level-raising operators that span the old subspace, and it conjugates the Petersson product, so it preserves the orthogonal complement. Consequently the conjugate of a newform f of nebentypus χ is again a newform, of nebentypus χ⁻¹, with the conjugate eigenvalues: the conjugate newform f_ρ of Miyake, §4.6. It is the form to which the Fricke involution sends f, up to a scalar.

For trivial nebentypus the good Hecke eigenvalues of a newform are real, so by strong multiplicity one the conjugate newform is the newform itself.

Main definitions #

Main results #

References #

source
theorem TauCeti.conj_mem_cuspFormsOld {N : ℕ} [NeZero N] {k : ℤ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsOld N k) :
CuspForm.conj ⋯ f ∈ cuspFormsOld N k

Conjugation preserves the old subspace: the conjugate of a level-raise V_d g from a proper divisor level is the level-raise V_d (g_ρ).

source
theorem TauCeti.conj_mem_cuspFormsNew {N : ℕ} [NeZero N] {k : ℤ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsNew N k) :
CuspForm.conj ⋯ f ∈ cuspFormsNew N k

Conjugation preserves the new subspace: if f is a new cusp form of level N, so is its conjugate f_ρ.

source
noncomputable def HeckeRing.GL2.Newform.conj {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) :
Newform N k

The conjugate newform f_ρ(τ) = conj (f (-conj τ)) of a newform f of nebentypus χ: a newform of nebentypus χ⁻¹ whose eigenvalues and q-expansion coefficients are the complex conjugates of those of f.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HeckeRing.GL2.Newform.toCuspForm_conj {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) :
    f.conj.toCuspForm = CuspForm.conj ⋯ f.toCuspForm

    The underlying cusp form of the conjugate newform is the conjugate form.

    source
    @[simp]
    theorem HeckeRing.GL2.Newform.χ_conj {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) :
    f.conj.χ = f.χ⁻¹

    The nebentypus of the conjugate newform is the inverse, that is the complex conjugate, of the nebentypus.

    source
    @[simp]
    theorem HeckeRing.GL2.Newform.eigenvalue_conj {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (n : ℕ+) (hn : (↑n).Coprime N) :
    f.conj.eigenvalue n hn = (starRingEnd ℂ) (f.eigenvalue n hn)

    The eigenvalues of the conjugate newform are the complex conjugates of the eigenvalues.

    source
    theorem HeckeRing.GL2.Newform.qExpansion_conj {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) :
    UpperHalfPlane.qExpansion 1 ⇑f.conj.toCuspForm = (PowerSeries.map (starRingEnd ℂ)) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

    The q-expansion coefficients of the conjugate newform are the complex conjugates of those of the newform.

    source
    @[simp]
    theorem HeckeRing.GL2.Newform.conj_conj {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) :
    f.conj.conj = f

    Conjugating a newform twice gives it back.

    source
    theorem HeckeRing.GL2.Newform.conj_eq_self_of_χ_eq_one {N : ℕ} [NeZero N] {k : ℤ} (f : Newform N k) (hχ : f.χ = 1) :
    f.conj = f

    A newform of trivial nebentypus is its own conjugate.