Documentation

TauCeti.NumberTheory.ModularForms.EisensteinSeries.Raising

Raising Eisenstein series with character #

For Dirichlet characters ψ modulo u and φ modulo v, the Eisenstein series with raising parameter t is

G_k^{ψ,φ,t}(z) = G_k^{ψ,φ}(t z) = V_t G_k^{ψ,φ}(z).

If tuv ∣ N, this is a modular form of level Γ₁(N) and nebentypus obtained by raising the product character ψφ to level N. The parameter t changes the q-expansion by the substitution q ↦ q^t; in particular, its coefficients are supported on multiples of t. These are the raised series used to span the Eisenstein part of a character space.

The construction is stated for arbitrary characters in weight at least three. Primitivity is not needed for modularity or level raising; it enters later when the Fourier expansion is normalized and the spanning family is indexed without repetitions.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.EisensteinSeries.charEisensteinSeriesMFRaise {u v N : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (t : ℕ) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) :
ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k

The character Eisenstein series with raising parameter t: G_k^{ψ,φ,t} = V_t G_k^{ψ,φ}, viewed at any level N divisible by tuv.

The underlying series is formed first at its natural level uv and then raised directly to level N. The divisibility hypothesis implies that both t and uv are nonzero.

Equations
Instances For
    source
    theorem TauCeti.EisensteinSeries.charEisensteinSeriesMFRaise_eq_levelRaise {u v N : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (t : ℕ) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) :
    charEisensteinSeriesMFRaise ψ φ t hk htuv = ModularForm.levelRaise t ⋯ (charEisensteinSeriesMF ψ φ hk ⋯)

    The raised series is the degeneracy image of the base series at its natural level. This equality characterizes the construction for importing modules, where the definition's body is not exposed.

    source
    @[simp]
    theorem TauCeti.EisensteinSeries.charEisensteinSeriesMFRaise_apply {u v N t : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) (z : UpperHalfPlane) :
    (charEisensteinSeriesMFRaise ψ φ t hk htuv) z = (charEisensteinSeriesMF ψ φ hk ⋯) (scaleGL t • z)

    The raised character Eisenstein series is the base series evaluated at t z.

    source
    theorem TauCeti.EisensteinSeries.charEisensteinSeriesMFRaise_apply_eq_tsum {u v N t : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) (z : UpperHalfPlane) :
    (charEisensteinSeriesMFRaise ψ φ t hk htuv) z = ∑' (x : Fin 2 → ℤ), (if ↑v ∣ x 0 then ψ ↑(x 0 / ↑v) * φ⁻¹ ↑(x 1) else 0) * EisensteinSeries.eisSummand k x (scaleGL t • z)

    The raised character Eisenstein series as a sum over integer pairs.

    source
    @[simp]
    theorem TauCeti.EisensteinSeries.charEisensteinSeriesMFRaise_one {u v N : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (huv : u * v ∣ N) :
    charEisensteinSeriesMFRaise ψ φ 1 hk ⋯ = ModularForm.ofLe ⋯ (charEisensteinSeriesMF ψ φ hk ⋯)

    At t = 1, the raised series is the base series restricted from level uv to level N.

    source
    @[simp]
    theorem TauCeti.EisensteinSeries.qExpansion_charEisensteinSeriesMFRaise {u v N t : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) :
    UpperHalfPlane.qExpansion 1 ⇑(charEisensteinSeriesMFRaise ψ φ t hk htuv) = (PowerSeries.expand t ⋯) (UpperHalfPlane.qExpansion 1 ⇑(charEisensteinSeriesMF ψ φ hk ⋯))

    The q-expansion of G_k^{ψ,φ,t} is obtained from that of G_k^{ψ,φ} by substituting q ↦ q^t.

    source
    theorem TauCeti.EisensteinSeries.qExpansion_charEisensteinSeriesMFRaise_coeff {u v N t : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) (n : ℕ) :
    (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑(charEisensteinSeriesMFRaise ψ φ t hk htuv)) = if t ∣ n then (PowerSeries.coeff (n / t)) (UpperHalfPlane.qExpansion 1 ⇑(charEisensteinSeriesMF ψ φ hk ⋯)) else 0

    The coefficient formula for a raised character Eisenstein series: a_n(G_k^{ψ,φ,t}) = a_{n/t}(G_k^{ψ,φ}) when t ∣ n, and is zero otherwise.

    source
    theorem TauCeti.EisensteinSeries.isSupportedOnDvd_qExpansion_charEisensteinSeriesMFRaise {u v N t : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) :
    PowerSeries.IsSupportedOnDvd t (UpperHalfPlane.qExpansion 1 ⇑(charEisensteinSeriesMFRaise ψ φ t hk htuv))

    The q-expansion of G_k^{ψ,φ,t} is supported on the multiples of t.

    source
    theorem TauCeti.EisensteinSeries.charEisensteinSeriesMFRaise_mem_modFormCharSpace {u v N t : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) :
    charEisensteinSeriesMFRaise ψ φ t hk htuv ∈ modFormCharSpace k (MulChar.toUnitHom ((DirichletCharacter.changeLevel ⋯) ψ * (DirichletCharacter.changeLevel ⋯) φ))

    Character-space membership after raising. At every target level N divisible by tuv, G_k^{ψ,φ,t} lies in M_k(N, ψφ), with both characters raised directly to level N.

    source
    theorem TauCeti.EisensteinSeries.charEisensteinSeriesMFRaise_eq_zero {u v N t : ℕ} {k : ℤ} [NeZero N] (ψ : DirichletCharacter ℂ u) (φ : DirichletCharacter ℂ v) (hk : 3 ≤ k) (htuv : t * (u * v) ∣ N) (hpar : ψ (-1) * φ (-1) ≠ (-1) ^ k) :
    charEisensteinSeriesMFRaise ψ φ t hk htuv = 0

    The parity obstruction survives level raising: if ψ(-1) φ(-1) ≠ (-1)^k, then every raised series is zero.