The parity lemma for nebentypus character spaces

The weight and the nebentypus of a nonzero modular form determine each other's parity: M_k(Γ₁(N), χ) ≠ 0 forces χ(-1) = (-1)^k. This is the emptiness criterion that odd weights and Eisenstein constructions consume, and the ModularForms roadmap pins it at Layer 0, alongside the diamond operators and character spaces of TauCeti.NumberTheory.ModularForms.DiamondOperators on which it is stated.

The mechanism is -I. It lies in Γ₀(N) at every level, and its lower-right entry is the unit -1, so it represents the diamond operator ⟨-1⟩. On the other hand -I acts trivially on ℍ and has determinant 1, so slashing by it is multiplication by the scalar (-1)^k (ModularForm.slash_neg_one). Comparing the two readings gives ⟨-1⟩ = (-1)^k as an operator (diamondOp_neg_one), and hence χ(-1) = (-1)^k on any nonzero element of the χ-eigenspace.

The criterion is one-directional: matching parities do not make the space nonzero, and nothing here claims they do. At the degenerate levels N ∣ 2, where -I lies in Γ₁(N) itself (CongruenceSubgroup.neg_one_mem_Gamma1_iff), the same computation kills the whole of M_k(Γ₁(N)) in odd weight (ModularForm.eq_zero_of_odd_of_dvd_two, deduced from Mathlib's ModularForm.eq_zero_of_neg_one_mem). That is consistent with the parity lemma rather than additional to it: there -1 = 1 in (ZMod N)ˣ, so every χ has χ(-1) = 1 ≠ -1 = (-1)^k.

Main results

• diamondOp_neg_one, diamondOpCusp_neg_one: the diamond operator ⟨-1⟩ is the scalar (-1)^k.
• char_neg_one_of_mem_modFormCharSpace, char_neg_one_of_mem_cuspFormCharSpace: the parity lemma, χ(-1) = (-1)^k for a nonzero form in the χ-eigenspace.
• modFormCharSpace_eq_bot_of_char_neg_one_ne, cuspFormCharSpace_eq_bot_of_char_neg_one_ne: its contrapositive, the emptiness criterion; char_neg_one_of_modFormCharSpace_ne_bot and char_neg_one_of_cuspFormCharSpace_ne_bot restate the lemma on the space itself.
• modFormCharSpace_one_eq_bot_of_odd: there are no odd-weight forms with trivial nebentypus, the classical M_k(Γ₀(N)) = 0 for odd k; even_of_mem_modFormCharSpace_one_of_ne_zero and even_of_mem_cuspFormCharSpace_one_of_ne_zero read it as the evenness of the weight of a nonzero form.
• ModularForm.eq_zero_of_odd_of_dvd_two: at the levels N ∣ 2 all of M_k(Γ₁(N)) vanishes in odd weight.

References

• Diamond–Shurman, A first course in modular forms, §5.1 (the remark following the definition of M_k(N, χ))
• Miyake, Modular forms, §4.3

The diamond operator at -1

theorem TauCeti.coe_diamondOp_neg_one {N : ℕ} (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((diamondOp k (-1)) f) = (-1) ^ k • ⇑f

The diamond operator ⟨-1⟩ acts on M_k(Γ₁(N)) as the scalar (-1)^k: it is represented by -I ∈ Γ₀(N), and slashing by -I is multiplication by (-1)^k.

@[simp]

theorem TauCeti.diamondOp_neg_one {N : ℕ} (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (diamondOp k (-1)) f = (-1) ^ k • f

The diamond operator ⟨-1⟩ on M_k(Γ₁(N)) is the scalar (-1)^k.

theorem TauCeti.coe_diamondOpCusp_neg_one {N : ℕ} (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((diamondOpCusp k (-1)) f) = (-1) ^ k • ⇑f

The diamond operator ⟨-1⟩ acts on S_k(Γ₁(N)) as the scalar (-1)^k.

@[simp]

theorem TauCeti.diamondOpCusp_neg_one {N : ℕ} (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (diamondOpCusp k (-1)) f = (-1) ^ k • f

The diamond operator ⟨-1⟩ on S_k(Γ₁(N)) is the scalar (-1)^k.

The parity lemma

theorem TauCeti.char_neg_one_of_mem_modFormCharSpace {N : ℕ} {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k χ) (hf0 : f ≠ 0) : ↑(χ (-1)) = (-1) ^ k

The parity lemma. If M_k(Γ₁(N), χ) contains a nonzero form then χ(-1) = (-1)^k.

Equivalently: the nebentypus of a nonzero modular form has the parity of its weight. The proof compares the two descriptions of -I, as the representative of the diamond operator ⟨-1⟩ (which acts by χ(-1) on the χ-eigenspace) and as a scalar matrix (which slashes by (-1)^k).

theorem TauCeti.char_neg_one_of_mem_cuspFormCharSpace {N : ℕ} {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) (hf0 : f ≠ 0) : ↑(χ (-1)) = (-1) ^ k

The parity lemma for cusp forms. If S_k(Γ₁(N), χ) contains a nonzero form then χ(-1) = (-1)^k.

The emptiness criterion

theorem TauCeti.modFormCharSpace_eq_bot_of_char_neg_one_ne {N : ℕ} {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (h : ↑(χ (-1)) ≠ (-1) ^ k) : modFormCharSpace k χ = ⊥

If the parities of χ and k disagree, M_k(Γ₁(N), χ) is zero.

theorem TauCeti.cuspFormCharSpace_eq_bot_of_char_neg_one_ne {N : ℕ} {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (h : ↑(χ (-1)) ≠ (-1) ^ k) : cuspFormCharSpace k χ = ⊥

If the parities of χ and k disagree, S_k(Γ₁(N), χ) is zero.

theorem TauCeti.char_neg_one_of_modFormCharSpace_ne_bot {N : ℕ} {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (h : modFormCharSpace k χ ≠ ⊥) : ↑(χ (-1)) = (-1) ^ k

The parity lemma, in the form the roadmap states it: if M_k(Γ₁(N), χ) is nonzero then χ(-1) = (-1)^k.

theorem TauCeti.char_neg_one_of_cuspFormCharSpace_ne_bot {N : ℕ} {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (h : cuspFormCharSpace k χ ≠ ⊥) : ↑(χ (-1)) = (-1) ^ k

The parity lemma for cusp forms, in the form the roadmap states it.

theorem TauCeti.char_neg_one_eq_one_of_even {N : ℕ} {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k χ) (hf0 : f ≠ 0) (hk : Even k) : ↑(χ (-1)) = 1

An even weight admits only even nebentypus: χ(-1) = 1.

theorem TauCeti.char_neg_one_eq_neg_one_of_odd {N : ℕ} {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k χ) (hf0 : f ≠ 0) (hk : Odd k) : ↑(χ (-1)) = -1

An odd weight admits only odd nebentypus: χ(-1) = -1.

theorem TauCeti.modFormCharSpace_one_eq_bot_of_odd {N : ℕ} {k : ℤ} (hk : Odd k) : modFormCharSpace k 1 = ⊥

There are no nonzero odd-weight forms with trivial nebentypus: M_k(N, 1) = 0 for k odd. This is the classical statement that M_k(Γ₀(N)) vanishes in odd weight, since -I ∈ Γ₀(N) acts on it by (-1)^k = -1.

theorem TauCeti.cuspFormCharSpace_one_eq_bot_of_odd {N : ℕ} {k : ℤ} (hk : Odd k) : cuspFormCharSpace k 1 = ⊥

There are no nonzero odd-weight cusp forms with trivial nebentypus.

theorem TauCeti.even_of_mem_modFormCharSpace_one_of_ne_zero {N : ℕ} {k : ℤ} {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k 1) (hf0 : f ≠ 0) : Even k

A nonzero form with trivial nebentypus has even weight.

theorem TauCeti.even_of_mem_cuspFormCharSpace_one_of_ne_zero {N : ℕ} {k : ℤ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k 1) (hf0 : f ≠ 0) : Even k

A nonzero cusp form with trivial nebentypus has even weight.

The degenerate levels N ∣ 2

theorem TauCeti.ModularForm.eq_zero_of_odd_of_dvd_two {N : ℕ} {k : ℤ} (hN : N ∣ 2) (hk : Odd k) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : f = 0

At the levels N ∣ 2, exactly those with -I ∈ Γ₁(N), every odd-weight modular form for Γ₁(N) vanishes.