Diamond operators and modular forms with character #
The diamond operators ⟨d⟩ on modular and cusp forms for Γ₁(N), and the nebentypus
character spaces M_k(Γ₁(N), χ) and S_k(Γ₁(N), χ) they cut out.
Since Γ₁(N) is normal in Γ₀(N) with quotient (ZMod N)ˣ (via the lower-right entry, the
map CongruenceSubgroup.Gamma0Map), slashing by any lift of d ∈ (ZMod N)ˣ is a well-defined
linear endomorphism of M_k(Γ₁(N)) and of S_k(Γ₁(N)): the diamond operator ⟨d⟩, packaged
as monoid homomorphisms diamondOpHom and diamondOpCuspHom into the endomorphism algebras.
The character space modFormCharSpace k χ (resp. cuspFormCharSpace k χ) is the simultaneous
χ-eigenspace of the diamond operators, a Submodule of Mathlib's ModularForm — not a new
bundled type — and membership in it is equivalent to the classical nebentypus transformation
law f ∣[k] γ = χ(d_γ) • f for γ ∈ Γ₀(N) (mem_modFormCharSpace_iff_nebentypus).
Ported from the AINTLIB LeanModularForms project
(LeanModularForms/HeckeRIngs/GL2/Gamma1Pair.lean, Chris Birkbeck), realizing Layer 0 of the
ModularForms roadmap; the roadmap pins these definitions (eigenspace-in-a-Submodule, not a
re-founded slash action with built-in character) and their names. The Hecke pair
(Γ₁(N), Δ₁(N)) from the same source file is Layer-2 material and is not ported here.
Main definitions #
(CongruenceSubgroup.Gamma0Map N).toHomUnits(Mathlib): the lower-right entry as aΓ₀(N) →* (ZMod N)ˣ.diamondOp/diamondOpCusp: the diamond operator⟨d⟩ford : (ZMod N)ˣ, a linear endomorphism ofModularForm ((Gamma1 N).map (mapGL ℝ)) kresp.CuspForm _ k, evaluated bycoe_diamondOp/coe_diamondOpCuspas slashing by any representative.diamondOpHom/diamondOpCuspHom: the diamond operators as monoid homomorphisms into the endomorphism algebras.diamondOpNat/diamondOpCuspNat: the same operator indexed by a natural number,⟨n⟩of Diamond–Shurman §5.3, extended by zero whennis not coprime toN.modFormCharSpace/cuspFormCharSpace: the nebentypus character spacesM_k(Γ₁(N), χ)andS_k(Γ₁(N), χ), cut out as simultaneous diamond eigenspaces.
Main results #
mem_modFormCharSpace_iff_nebentypus/mem_cuspFormCharSpace_iff_nebentypus: membership in the character space is the classical nebentypus relationf ∣[k] g = χ(d_g) • ffor allg ∈ Γ₀(N).slash_mapGL_eq_diamondOpNat/slash_mapGL_eq_diamondOpCuspNat: rational slashing by a suitableΓ₀(N)representative is the corresponding natural-indexed diamond operator;slash_mapGL_gamma0Twist_eq_diamondOpNatand its cusp counterpart specialize to the explicit Bézout representative.cuspToModFormCharSpace: the inclusionS_k(N, χ) → M_k(N, χ)that the coercion induces, along which a statement about modular forms specialises to cusp forms.diamondOp_coe_cuspForm,coe_mem_modFormCharSpace_iff: the diamond operators, and hence the character spaces, commute with the coercionS_k(Γ₁(N)) → M_k(Γ₁(N)); a cusp form is aχ-form exactly when the modular form underlying it is.eq_of_mem_cuspFormCharSpace_of_ne_zero: a nonzero cusp form determines its nebentypus.slash_mapGL_eq_self_of_comp_of_mem_modFormCharSpace,slash_mapGL_eq_self_of_comp_of_mem_cuspFormCharSpace: a matrix ofΓ₀(N)whose lower-right entry is1modulo a divisorMacts trivially on a form whose character is pulled back from modulusM.
References #
- Miyake, Modular forms, §4.5
- Diamond–Shurman, A first course in modular forms, §5.1 and §5.3
diamondOp_coe_cuspFormandcoe_mem_modFormCharSpace_iffadapt AINTLIB commit2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck,LeanModularForms/HeckeRIngs/GL2/Unified/NebentypusHeckeRingHom.lean, declarationscuspFormCharSpace_toModularForm'_memandcuspFormCharSpace_of_toModularForm'_mem. Those are two one-way statements about AINTLIB's ownCuspForm.toModularForm'; here they are oneiffthrough mathlib's coercion, which this repository uses instead.
Slash-transport for Γ₁(N)-invariant functions: if f is invariant under
(Gamma1 N).map (mapGL ℝ) and Gamma0Map N g₁ = Gamma0Map N g₂, then
f ∣[k] g₁ = f ∣[k] g₂.
Evaluation of the diamond operator: at any representative g ∈ Γ₀(N) with lower-right
entry d, the diamond operator ⟨d⟩ is slashing by g.
The diamond operator at 1 is the identity.
The diamond operator as a monoid homomorphism (ZMod N)ˣ →* Module.End ℂ (...).
Equations
- diamondOpHom k = { toFun := diamondOp k, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The cusp-form diamond operator indexed by d : (ZMod N)ˣ.
Equations
- diamondOpCusp k d = diamondOpCuspAux✝ k ⋯.choose
Instances For
Evaluation of the cusp-form diamond operator: at any representative g ∈ Γ₀(N) with
lower-right entry d, the diamond operator ⟨d⟩ is slashing by g.
The cusp diamond operator at 1 is the identity.
Cusp diamond operators compose multiplicatively.
The cusp-form diamond operator as a monoid homomorphism.
Equations
- diamondOpCuspHom k = { toFun := diamondOpCusp k, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The nebentypus character space S_k(Γ₁(N), χ): cusp forms on which every
diamond operator ⟨d⟩ acts by the scalar χ(d).
Equations
- cuspFormCharSpace k χ = ⨅ (d : (ZMod N)ˣ), ((diamondOpCuspHom k) d).eigenspace ↑(χ d)
Instances For
Defining equation for the sealed cuspFormCharSpace: it is the joint eigenspace of the
diamond operators.
Membership in S_k(Γ₁(N), χ): f is in the χ-eigenspace iff
⟨d⟩ f = χ(d) • f for every d ∈ (ZMod N)ˣ.
Diamond operators act by χ(d) on elements of S_k(Γ₁(N), χ). Not @[simp]: χ
occurs only in the hypothesis and the right-hand side, so simp cannot infer it.
A nonzero cusp form determines its nebentypus: the character spaces of two distinct
characters meet only in 0, since ⟨d⟩ f = χ(d) • f = χ'(d) • f forces χ(d) = χ'(d).
The modular-form nebentypus character space M_k(Γ₁(N), χ).
Equations
- modFormCharSpace k χ = ⨅ (d : (ZMod N)ˣ), ((diamondOpHom k) d).eigenspace ↑(χ d)
Instances For
Defining equation for the sealed modFormCharSpace: it is the joint eigenspace of the
diamond operators.
Membership in M_k(Γ₁(N), χ): f is in the χ-eigenspace iff ⟨d⟩ f = χ(d) • f
for every d ∈ (ZMod N)ˣ.
Diamond operators act by χ(d) on elements of M_k(Γ₁(N), χ). Not @[simp]: χ
occurs only in the hypothesis and the right-hand side, so simp cannot infer it.
Bridge: for a Gamma1-invariant modular form f, membership in the
diamond-eigenspace modFormCharSpace k χ₀ is equivalent to the classical nebentypus
relation f ∣[k] g = χ₀(d_g) • f for all g ∈ Γ₀(N).
A matrix of Γ₀(N) whose lower-right entry is 1 modulo a divisor M acts trivially on
M_k(Γ₁(N), χ) when χ is pulled back from a character modulo M: its nebentypus value is
χ₀ of the lower-right entry modulo M, which is χ₀ 1 = 1.
Bridge (cusp forms): for a Gamma1-invariant cusp form f, membership in the
diamond-eigenspace cuspFormCharSpace k χ₀ is equivalent to the classical nebentypus
relation f ∣[k] g = χ₀(d_g) • f for all g ∈ Γ₀(N).
The diamond operator indexed by a natural number: ⟨n⟩ is diamondOp at the unit n mod N
when n is coprime to N, and 0 otherwise.
This is ⟨n⟩ as Diamond–Shurman §5.3 writes it. Extending the index from (ZMod N)ˣ to ℕ by
zero is what lets the Hecke recurrence at a prime power be stated uniformly: the ⟨p⟩ term
simply vanishes when p ∣ N, instead of the recurrence needing a separate case.
Follows diamondOp_n of the AINTLIB LeanModularForms project
(HeckeRIngs/GL2/HeckeT_n.lean, https://github.com/CBirkbeck/AINTLIB, commit
ce76186b5f61c846d770d2f87eb76ba5b9c9117a, Apache-2.0).
Equations
- diamondOpNat k n = if h : n.Coprime N then diamondOp k (ZMod.unitOfCoprime n h) else 0
Instances For
When n is coprime to N, ⟨n⟩ is the diamond operator at the unit n mod N.
The cusp-form diamond operator indexed by a natural number: ⟨n⟩ is diamondOpCusp at the
unit n mod N when n is coprime to N, and 0 otherwise — the cusp-form counterpart of
diamondOpNat, and the reason the prime Hecke operator on S_k(Γ₁(N)) has one formula at every
prime rather than one per divisibility case.
Equations
- diamondOpCuspNat k n = if h : n.Coprime N then diamondOpCusp k (ZMod.unitOfCoprime n h) else 0
Instances For
When n is coprime to N, ⟨n⟩ is the cusp diamond operator at the unit n mod N.
Slashing by a Γ₀(N) representative with lower-right unit n is the zero-extended
diamond operator ⟨n⟩ on modular forms.
The cusp-form counterpart of slash_mapGL_eq_diamondOpNat.
Slashing by the Bézout twist is the diamond operator ⟨p⟩. The twist is the Γ₀(N)
element of lower-right entry p, so this is coe_diamondOp at that representative, transported
across the ℚ/ℝ bridge.
Slashing by the Bézout twist is the diamond operator ⟨p⟩, on cusp forms.
The character spaces under the cusp-form coercion #
The diamond operator commutes with the coercion S_k(Γ) → M_k(Γ): ⟨d⟩ slashes by a
representative of d, which does not see whether a form vanishes at the cusps.
A cusp form is a χ-form exactly when the modular form underlying it is. Membership in
either character space is the same family of diamond eigenvalue equations, and the coercion is
pointwise, so the two conditions transport across it.
Not @[simp]: the left-hand side is itself simp-reducible — mem_modFormCharSpace_iff is
@[simp] and rewrites it to the diamond eigenvalue equations — so this lemma could never fire
as a rewrite rule, and tagging it makes the simpNF linter fail. Use it explicitly, as
Parity.lean does.
A matrix of Γ₀(N) whose lower-right entry is 1 modulo a divisor M acts trivially on
S_k(Γ₁(N), χ) when χ is pulled back from a character modulo M: its nebentypus value is
χ₀ of the lower-right entry modulo M, which is χ₀ 1 = 1.
The inclusion of character spaces along S_k(Γ₁(N)) → M_k(Γ₁(N)). A cusp form lies in
S_k(N, χ) exactly when the modular form underlying it lies in M_k(N, χ)
(coe_mem_modFormCharSpace_iff), so Mathlib's CuspForm.toModularFormₗ restricts to a map
between the character spaces. This is the map along which a statement about modFormCharSpace
specialises to cuspFormCharSpace.
Equations
Instances For
The inclusion of character spaces is injective: it restricts Mathlib's injective
CuspForm.toModularFormₗ.