Eisenstein subspaces with fixed nebentypus

For weight k >= 3, the Eisenstein subspace of M_k(N, chi) is spanned by the raised character Eisenstein series

E_k^(psi, phi, t) = V_t E_k^(psi, phi)

with primitive characters psi and phi, compatible parity, t * u * v | N, and induced nebentypus chi. This file packages the exact indexing data and defines the span inside the already existing character space. In particular, character-space membership is built into each generator rather than imposed afterwards on the span.

The resulting subspace is the Eisenstein term in the cusp--Eisenstein decomposition. Its comparison with the image of the constant-term map is separate: it requires the spanning and linear-independence theorem for the constant terms at all cusps.

Main definitions

• TauCeti.EisensteinSeries.CharIndex: the primitive, parity-compatible data (psi, phi, t) indexing a raised character Eisenstein series at level N.
• TauCeti.EisensteinSeries.CharIndex.nebentypus: the product character induced at level N.
• TauCeti.EisensteinSeries.CharIndex.form: the corresponding normalized raised series.
• TauCeti.eisensteinSubspace: the span of the generators with prescribed nebentypus.

Main results

• TauCeti.EisensteinSeries.CharIndex.form_mem_modFormCharSpace: every indexed series belongs to the character space prescribed by its induced nebentypus.
• TauCeti.mem_eisensteinSubspace: every prescribed-nebentypus generator belongs to the Eisenstein subspace.
• TauCeti.mem_eisensteinSubspace_iff: membership is equivalent to being a finite linear combination of the prescribed-nebentypus generators.
• TauCeti.eisensteinSubspace_le: the elimination rule for the span.
• TauCeti.eisensteinSubspace_ne_bot_iff: the subspace is nonzero exactly when its indexing type is inhabited.

References

• F. Diamond and J. Shurman, A first course in modular forms, Section 4.5.
• T. Miyake, Modular forms, Section 7.1.

structure TauCeti.EisensteinSeries.CharIndex (N k : ℕ) : Type

The data indexing a normalized raised character Eisenstein series of weight k and level N: primitive characters psi modulo u and phi modulo v, compatible parity, and a raising parameter t with tuv | N.

The induced character at level N is kept as a derived accessor, since it is canonically determined by this data.

• u : ℕ

  The modulus of the first primitive character.

• v : ℕ

  The modulus of the second primitive character.

• t : ℕ

  The level-raising parameter.

• psi : DirichletCharacter ℂ self.u

  The first primitive Dirichlet character.

• phi : DirichletCharacter ℂ self.v

  The second primitive Dirichlet character.

• psi_primitive : self.psi.IsPrimitive

  The first character is primitive.

• phi_primitive : self.phi.IsPrimitive

  The second character is primitive.

• parity : self.psi (-1) * self.phi (-1) = (-1) ^ ↑k

  The two characters have the parity required in weight k.

• level_dvd : self.t * (self.u * self.v) ∣ N

  The natural level tuv divides the target level.

noncomputable def TauCeti.EisensteinSeries.CharIndex.nebentypus {N k : ℕ} (a : CharIndex N k) : (ZMod N)ˣ →* ℂˣ

The product nebentypus of an Eisenstein index, with both primitive characters raised to the target level N.

Equations

• a.nebentypus = MulChar.toUnitHom ((DirichletCharacter.changeLevel ⋯) a.psi * (DirichletCharacter.changeLevel ⋯) a.phi)

theorem TauCeti.EisensteinSeries.CharIndex.nebentypus_def {N k : ℕ} (a : CharIndex N k) : a.nebentypus = MulChar.toUnitHom ((DirichletCharacter.changeLevel ⋯) a.psi * (DirichletCharacter.changeLevel ⋯) a.phi)

The defining expression for the nebentypus of an Eisenstein index.

noncomputable def TauCeti.EisensteinSeries.CharIndex.form {N k : ℕ} (a : CharIndex N k) [NeZero N] (hk : 3 ≤ ↑k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) ↑k

The normalized raised character Eisenstein series attached to an index.

Equations

• a.form hk = TauCeti.EisensteinSeries.normalizedCharEisensteinSeriesMFRaise a.psi a.phi a.t hk ⋯

theorem TauCeti.EisensteinSeries.CharIndex.form_def {N k : ℕ} (a : CharIndex N k) [NeZero N] (hk : 3 ≤ ↑k) : a.form hk = normalizedCharEisensteinSeriesMFRaise a.psi a.phi a.t hk ⋯

The defining expression for the normalized raised series attached to an Eisenstein index.

theorem TauCeti.EisensteinSeries.CharIndex.form_mem_modFormCharSpace {N k : ℕ} (a : CharIndex N k) [NeZero N] (hk : 3 ≤ ↑k) : a.form hk ∈ modFormCharSpace (↑k) a.nebentypus

An indexed Eisenstein series belongs to the character space of its induced nebentypus.

@[simp]

theorem TauCeti.EisensteinSeries.CharIndex.qExpansion_form_coeff_t {N k : ℕ} (a : CharIndex N k) [NeZero N] (hk : 3 ≤ ↑k) : (PowerSeries.coeff a.t) (UpperHalfPlane.qExpansion 1 ⇑(a.form hk)) = 1

The coefficient at the first positive supported index t of an indexed Eisenstein series is 1.

theorem TauCeti.EisensteinSeries.CharIndex.form_ne_zero {N k : ℕ} (a : CharIndex N k) [NeZero N] (hk : 3 ≤ ↑k) : a.form hk ≠ 0

Every indexed Eisenstein series is nonzero.

noncomputable def TauCeti.EisensteinSeries.CharIndex.inCharSpace {N k : ℕ} (a : CharIndex N k) {chi : (ZMod N)ˣ →* ℂˣ} [NeZero N] (hk : 3 ≤ ↑k) (hchi : a.nebentypus = chi) : ↥(modFormCharSpace (↑k) chi)

An indexed Eisenstein series, regarded as an element of a specified character space whose character agrees with the induced nebentypus.

Equations

• a.inCharSpace hk hchi = ⟨a.form hk, ⋯⟩

@[simp]

theorem TauCeti.EisensteinSeries.CharIndex.coe_inCharSpace {N k : ℕ} (a : CharIndex N k) {chi : (ZMod N)ˣ →* ℂˣ} [NeZero N] (hk : 3 ≤ ↑k) (hchi : a.nebentypus = chi) : ↑(a.inCharSpace hk hchi) = a.form hk

Coercing inCharSpace forgets only the proof of character-space membership.

theorem TauCeti.EisensteinSeries.CharIndex.inCharSpace_ne_zero {N k : ℕ} (a : CharIndex N k) {chi : (ZMod N)ˣ →* ℂˣ} [NeZero N] (hk : 3 ≤ ↑k) (hchi : a.nebentypus = chi) : a.inCharSpace hk hchi ≠ 0

An indexed Eisenstein series remains nonzero inside its character space.

noncomputable def TauCeti.eisensteinSubspace {N k : ℕ} [NeZero N] (chi : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) : Submodule ℂ ↥(modFormCharSpace (↑k) chi)

The Eisenstein subspace of M_k(N, chi) for k >= 3: the span of the normalized raised series E_k^(psi, phi, t) over primitive, parity-compatible pairs whose induced nebentypus is chi and whose natural level tuv divides N.

Equations

• TauCeti.eisensteinSubspace chi hk = Submodule.span ℂ (Set.range fun (a : { a : TauCeti.EisensteinSeries.CharIndex N k // a.nebentypus = chi }) => (↑a).inCharSpace hk ⋯)

theorem TauCeti.eisensteinSubspace_def {N k : ℕ} [NeZero N] (chi : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) : eisensteinSubspace chi hk = Submodule.span ℂ (Set.range fun (a : { a : EisensteinSeries.CharIndex N k // a.nebentypus = chi }) => (↑a).inCharSpace hk ⋯)

The defining span of the Eisenstein subspace.

theorem TauCeti.mem_eisensteinSubspace {N k : ℕ} [NeZero N] (chi : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) (a : EisensteinSeries.CharIndex N k) (hchi : a.nebentypus = chi) : a.inCharSpace hk hchi ∈ eisensteinSubspace chi hk

Every indexed series with induced nebentypus chi belongs to the Eisenstein subspace.

theorem TauCeti.mem_eisensteinSubspace_iff {N k : ℕ} [NeZero N] (chi : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) (f : ↥(modFormCharSpace (↑k) chi)) : f ∈ eisensteinSubspace chi hk ↔ ∃ (c : { a : EisensteinSeries.CharIndex N k // a.nebentypus = chi } →₀ ℂ), (c.sum fun (a : { a : EisensteinSeries.CharIndex N k // a.nebentypus = chi }) (z : ℂ) => z • (↑a).inCharSpace hk ⋯) = f

A form belongs to the Eisenstein subspace exactly when it is a finite linear combination of the indexed series with induced nebentypus chi.

theorem TauCeti.eisensteinSubspace_le {N k : ℕ} [NeZero N] (chi : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) {V : Submodule ℂ ↥(modFormCharSpace (↑k) chi)} (hV : ∀ (a : EisensteinSeries.CharIndex N k) (hchi : a.nebentypus = chi), a.inCharSpace hk hchi ∈ V) : eisensteinSubspace chi hk ≤ V

Elimination rule for the Eisenstein subspace: a subspace containing every indexed series of nebentypus chi contains their span.

theorem TauCeti.eisensteinSubspace_ne_bot_iff {N k : ℕ} [NeZero N] (chi : (ZMod N)ˣ →* ℂˣ) (hk : 3 ≤ ↑k) : eisensteinSubspace chi hk ≠ ⊥ ↔ Nonempty { a : EisensteinSeries.CharIndex N k // a.nebentypus = chi }

The Eisenstein subspace is nonzero exactly when there is at least one primitive, parity-compatible raised Eisenstein series with the prescribed nebentypus.