The diamond operators are the Hecke operators of the Γ₀(N)-cosets #
ModularForms/DiamondOperators.lean builds ⟨d⟩ by hand, as slashing by any Γ₀(N) matrix
with lower-right entry d, and shows the result is well defined on M_k(Γ₁(N)) and on
S_k(Γ₁(N)). HeckeRing/GL2/Gamma1/DiamondCosets.lean builds, from the same matrix, an
element of the Hecke ring 𝕋 Δ₀(N) Γ₁(N) ℤ. This file identifies the two:
heckeSlashGamma1ModularFormEnd k (diamondCosetGamma1 N γ) = diamondOp k d,
and the same on cusp forms, and — through the ℤ-linear action of the Hecke ring — the
unit-indexed form heckeSlashGamma1RingModularFormLinearMap k (diamondHeckeElem N d) = diamondOp k d, again on both modular and cusp forms. So the diamond operators are not a
construction parallel to the Hecke operators: they are the Hecke operators of the double cosets
Γ₁(N) γ Γ₁(N) with γ ∈ Γ₀(N), and the identification is a theorem rather than a
definition.
Why it is a one-term sum #
Slashing by a double coset means summing over its right cosets. A diamond coset has exactly
one, Γ₁(N) γ (HeckeRing.GL2.doubleCoset_out_diamondCosetGamma1_eq_iUnion_rightCosets,
which holds because Γ₁(N) is normal in Γ₀(N)), so the sum
heckeSlashSum k (diamondCosetGamma1 N γ) f has a single summand f ∣[k] γ — and that is the
defining formula of ⟨d⟩. The only remaining step is the ℚ-to-ℝ bridge
ModularForm.rat_slash_mapGL, since the Hecke triples live over ℚ and the slash action of a
modular form over ℝ.
Nothing here needs the choice-freeness of ⟨d⟩ to be reproved: both sides are computed at the
same representative γ, and their independence of it is DiamondOperators.lean's
coe_diamondOp on one side and HeckeRing.GL2.diamondCosetGamma1_eq_iff on the other.
The adjugate double coset #
For n prime to N, a Bézout identity supplies matrices A ∈ Γ₀(N) and B ∈ Γ₁(N) that
factor diag(n, 1) as both A diag(1, n) B and B diag(1, n) A. Reading the two
factorizations through the trace description of a Hecke operator proves that the trace of the
translate by diag(n, 1) is ⟨n⟩⁻¹ Tₙ. This is the identity consumed by the Petersson-adjoint
argument. Reading both factorizations also proves that Tₙ commutes with ⟨n⟩⁻¹, which is used
for the nebentypus specialization. This is the standard argument of Diamond--Shurman, §5.5.
Main results #
HeckeRing.GL2.heckeSlashSum_diamondCosetGamma1: the slash sum of a diamond coset is the single slashf ∣[k] γ, for a form of any of the level-Γ₁(N)form classes.HeckeRing.GL2.heckeSlashGamma1ModularFormEnd_diamondCosetGamma1andHeckeRing.GL2.heckeSlashGamma1CuspFormEnd_diamondCosetGamma1: the identification, onM_k(Γ₁(N))and onS_k(Γ₁(N)).HeckeRing.GL2.heckeSlashGamma1RingModularFormLinearMap_diamondHeckeElemandHeckeRing.GL2.heckeSlashGamma1CuspRingLinearMap_diamondHeckeElem: the same statement read on the Hecke ring, at the unit-indexed element⟨d⟩.HeckeRing.GL2.isFiniteRelIndex_adjugateGL_natDiagGL: the finite-relative-index instance needed to trace the adjugate translate.HeckeRing.GL2.trace_translate_adjugateGL_natDiagGL_eq_diamondOp_heckeTNatandHeckeRing.GL2.trace_translate_adjugateGL_natDiagGL_eq_diamondOpCusp_heckeTCuspNat: the adjugate trace is⟨n⟩⁻¹ Tₙon modular forms and on cusp forms.HeckeRing.GL2.commute_heckeTNat_diamondOp_invandHeckeRing.GL2.commute_heckeTCuspNat_diamondOpCusp_inv: at every index prime to the level,Tₙcommutes with the inverse diamond operator⟨n⟩⁻¹.HeckeRing.GL2.heckeSlashGamma1ModularFormEnd_diamondCosetGamma1_apply_of_mem_modFormCharSpaceand its cusp-form counterpart: on a nebentypus space the diamond coset acts by the scalarχ(d).
References #
- F. Diamond and J. Shurman, A first course in modular forms, §§5.2 and 5.5.
- T. Miyake, Modular forms, Theorem 4.5.4.
- G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4.
The slash sum of a diamond coset is a single slash. The double coset Γ₁(N) γ Γ₁(N)
decomposes into the one right coset Γ₁(N) γ, so the Hecke sum attached to it has one
summand.
The diamond operator on M_k(Γ₁(N)) is the Hecke operator of the double coset
Γ₁(N) γ Γ₁(N). Both sides are slashing by γ; the left-hand side arrives as a one-term
Hecke sum over GL₂(ℚ), the right-hand side as the definition of ⟨d⟩ over GL₂(ℝ).
The diamond operator on S_k(Γ₁(N)) is the Hecke operator of the double coset
Γ₁(N) γ Γ₁(N).
On a nebentypus space the diamond coset acts by the scalar χ(d). This is the shape
the character-space action of the Hecke ring consumes: on M_k(N, χ) the diamond direction of
the ring contributes no new operator, only multiplication by χ(d).
On a nebentypus cusp-form space the diamond coset acts by the scalar χ(d).
The diamond element of the Hecke ring acts by the diamond operator. Read through the
ℤ-linear action heckeSlashGamma1RingModularFormLinearMap of the Hecke ring on M_k(Γ₁(N)),
the element ⟨d⟩ of HeckeRing/GL2/Gamma1/DiamondCosets.lean is the operator ⟨d⟩ of
ModularForms/DiamondOperators.lean.
The diamond element of the Hecke ring acts on cusp forms by the diamond operator: the
cusp-form counterpart of heckeSlashGamma1RingModularFormLinearMap_diamondHeckeElem, read
through the ℤ-linear action heckeSlashGamma1CuspRingLinearMap on S_k(Γ₁(N)).
The modular-form double coset operator of diag(n, 1) is ⟨n⟩⁻¹ Tₙ.
⟨n⟩⁻¹ commutes with Tₙ on modular forms. For n coprime to N, the inverse
diamond operator commutes with Tₙ on M_k(Γ₁(N)).
The double coset operator of diag(n, 1) is ⟨n⟩⁻¹ Tₙ. For n coprime to N, the
trace of the translate by the main involution of diag(1, n) is ⟨n⁻¹⟩ (Tₙ f).
⟨n⟩⁻¹ commutes with Tₙ. For n coprime to N, the inverse diamond operator
commutes with Tₙ on S_k(Γ₁(N)).