Documentation

TauCeti.NumberTheory.ModularForms.EisensteinSeries.Count

Counting the Eisenstein series with character #

The normalized raised Eisenstein series E_k^(ψ, φ, t) of weight k and level N are indexed by TauCeti.EisensteinSeries.CharIndex N k: primitive characters ψ modulo u and φ modulo v with ψ(-1) φ(-1) = (-1)^k, and a raising parameter t with t u v ∣ N. This file counts these indices. Away from the levels 1, 2 and 4 there are exactly as many as there are cusps of Γ₁(N):

2 · #CharIndex N k = ∑_{g ∣ N} totient(g) totient(N / g) = 2 ε∞(Γ₁(N)),

where totient is Euler's function Nat.totient.

The series are linearly independent, so in weight k ≥ 3 the Eisenstein subspaces TauCeti.eisensteinSubspace of the spaces M_k(N, χ) have dimensions summing to this number (TauCeti.finrank_eisensteinSubspace). Comparing it with the number of cusps, which bounds the dimension of the Eisenstein part of M_k(Γ₁(N)) through the constant terms, is how Diamond–Shurman show that the series span that part (Theorem 4.5.2); this file supplies the count of the series.

The count goes through a bijection. Raising ψ and φ to the levels g = t u and N / g sends an index to a divisor g ∣ N and a pair of characters modulo g and N / g of product parity (-1)^k; conversely, u and v are the conductors of such a pair, ψ and φ their primitive characters, and t = g / u. This gives the count card_eq_sum at every level. When g or N / g exceeds 2, an odd character at that level exchanges the two parities, so exactly half of the totient(g) totient(N / g) pairs have parity (-1)^k (DirichletCharacter.two_mul_card_apply_neg_one_mul_apply_neg_one_eq). Every divisor g of N ∉ {1, 2, 4} has this property.

At the levels 1, 2 and 4 the count is direct. Modulo 1 and 2 the only character is trivial and even, so a pair of such characters has parity (-1)^k exactly when k is even. There are 1, 2 and 3 indices in even weight, and 0, 0 and 2 in odd weight. In odd weight the level-4 count is one less than the three cusps of Γ₁(4), matching its irregular cusp.

Main results #

References #

source
instance TauCeti.EisensteinSeries.CharIndex.instFinite {N k : ℕ} [NeZero N] :
Finite (CharIndex N k)

At a nonzero level there are finitely many Eisenstein indices.

source
theorem TauCeti.EisensteinSeries.CharIndex.card_eq_sum {N k : ℕ} [NeZero N] :
Nat.card (CharIndex N k) = ∑ g ∈ N.divisors, Nat.card { q : DirichletCharacter ℂ g × DirichletCharacter ℂ (N / g) // q.1 (-1) * q.2 (-1) = (-1) ^ ↑k }

The number of Eisenstein indices at level N: indices (ψ, φ, t) correspond to the divisors g = t u of N together with a pair of characters modulo g and N / g whose product parity is (-1)^k.

source
theorem TauCeti.EisensteinSeries.CharIndex.two_mul_card {N k : ℕ} (hN : 2 < N) (hN4 : N ≠ 4) :
2 * Nat.card (CharIndex N k) = ∑ g ∈ N.divisors, g.totient * (N / g).totient

Twice the number of Eisenstein indices is ∑_{g ∣ N} totient(g) totient(N / g) away from the levels 1, 2 and 4.

source
theorem TauCeti.EisensteinSeries.CharIndex.card_eq_card_cuspOrbit_Gamma1 {N k : ℕ} (hN : 2 < N) (hN4 : N ≠ 4) :
Nat.card (CharIndex N k) = Nat.card (Subgroup.map sl2zToPSL2R (CongruenceSubgroup.Gamma1 N)).CuspOrbit

The Eisenstein indices are as many as the cusps of Γ₁(N) away from the levels 1, 2 and 4.

The levels 1, 2 and 4 #

source
theorem TauCeti.EisensteinSeries.CharIndex.card_one {k : ℕ} :
Nat.card (CharIndex 1 k) = if Even k then 1 else 0

There is one Eisenstein index at level 1 in even weight, and none in odd weight.

source
theorem TauCeti.EisensteinSeries.CharIndex.card_two {k : ℕ} :
Nat.card (CharIndex 2 k) = if Even k then 2 else 0

There are two Eisenstein indices at level 2 in even weight, and none in odd weight.

source
theorem TauCeti.EisensteinSeries.CharIndex.card_four {k : ℕ} :
Nat.card (CharIndex 4 k) = if Even k then 3 else 2

There are three Eisenstein indices at level 4 in even weight, and two in odd weight.