The diamond double cosets of the Γ₁(N) Hecke ring #
The Hecke monoid Δ₀(N) asks its elements only to have a unit upper-left entry modulo N,
which is what puts all of Γ₀(N) inside it (HeckeRing/GL2/Gamma1/Basic.lean). This file takes
the resulting payoff: for γ ∈ Γ₀(N) the double coset Γ₁(N) γ Γ₁(N) is a basis element of the
Hecke ring 𝕋 Δ₀(N) Γ₁(N) ℤ, it is a single right coset Γ₁(N) γ because Γ₁(N) is normal
in Γ₀(N), it depends only on the lower-right entry d ∈ (ZMod N)ˣ, and the resulting map
⟨·⟩ : (ZMod N)ˣ →* 𝕋 Δ₀(N) Γ₁(N) ℤ
is an injective monoid homomorphism. So the diamond operators are not an extra structure bolted
onto the Hecke algebra: they are honest basis elements of it. That the endomorphism of
M_k(Γ₁(N)) such a coset induces is the ⟨d⟩ of ModularForms/DiamondOperators.lean is the
companion statement, proved in ModularForms/HeckeSlash/Diamond.lean.
Why the double coset collapses, and what that buys #
Γ₁(N) is normal in Γ₀(N) (CongruenceSubgroup.Gamma0_normalizes_Gamma1), so γ lies in the
normalizer of the image of Γ₁(N) in GL₂(ℚ). Everything below is then an instance of the
general theory of HeckeRing/Normalizer.lean, which collapses a double coset at a normalizing
element to a single right coset and draws the two consequences that drive this file.
- The double coset has a single right coset, so the slash operator attached to it is a
one-term sum. That is the shape
heckeSlashSumconsumes, through the decompositiondoubleCoset_out_diamondCosetGamma1_eq_iUnion_rightCosetsstated at the chosen representative. - Its decomposition quotients are subsingletons, so the structure constants of a product of two
diamond cosets are at most
1: the product of two diamond basis elements is the diamond basis element of the product. No counting is needed, which is exactly what distinguishes the diamonds from theTₚ.
Main definitions #
HeckeRing.GL2.diamondCosetGamma1: the double cosetΓ₁(N) γ Γ₁(N)ofγ ∈ Γ₀(N).HeckeRing.GL2.diamondHeckeElemandHeckeRing.GL2.diamondHeckeElemHom: the diamond element⟨d⟩of the Hecke ring, and the monoid homomorphism(ZMod N)ˣ →* 𝕋 Δ₀(N) Γ₁(N) ℤit forms.
Main results #
HeckeRing.GL2.diamondCosetGamma1_toSet_eq_rightCosetandHeckeRing.GL2.doubleCoset_out_diamondCosetGamma1_eq_iUnion_rightCosets: the double coset is the single right cosetΓ₁(N) γ, in the two spellings the Hecke machinery uses.HeckeRing.GL2.diamondCosetGamma1_eq_iff: the coset depends exactly on the lower-right entry.HeckeRing.GL2.single_diamondCosetGamma1_mul_single_diamondCosetGamma1: the basis elements multiply,[Γ₁(N) γ₁ Γ₁(N)] · [Γ₁(N) γ₂ Γ₁(N)] = [Γ₁(N) γ₁γ₂ Γ₁(N)].HeckeRing.GL2.diamondHeckeElemHom_injective: the diamonds form a faithful copy of(ZMod N)ˣinside the Hecke ring.
References #
The diamond double coset Γ₁(N) · γ · Γ₁(N) of an element γ ∈ Γ₀(N), as an element of
the basis of the Hecke ring of the pair (Γ₁(N), Δ₀(N)).
It is indexed by an element of Γ₀(N) rather than by a unit of ZMod N because a double coset
is formed from a matrix; that it depends only on the lower-right entry is
diamondCosetGamma1_eq_iff, and diamondHeckeElem is the resulting unit-indexed element.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Defining equation for the sealed definition diamondCosetGamma1.
The underlying set of a diamond coset is the double coset of γ: HeckeCoset.toSet_mk
read at the sealed definition diamondCosetGamma1, whose body simp cannot unfold on its own.
The collapsed form is diamondCosetGamma1_toSet_eq_rightCoset.
The diamond double coset is a single right coset, Γ₁(N) γ Γ₁(N) = Γ₁(N) γ, since γ
normalizes Γ₁(N).
The double coset of the chosen representative of diamondCosetGamma1 N g, presented as the
one-term union of right cosets — the shape the slash sum of
ModularForms/HeckeSlash/Independence.lean consumes.
The diamond coset of the identity is the identity double coset Γ₁(N) · 1 · Γ₁(N).
The diamond coset sees exactly the lower-right entry. Two elements of Γ₀(N) give the
same double coset precisely when they have the same image in (ZMod N)ˣ; the forward direction
uses that mapGL ℚ is injective, so a rational coincidence is an integral one.
The diamond basis elements multiply: [Γ₁(N) γ₁ Γ₁(N)] · [Γ₁(N) γ₂ Γ₁(N)] = [Γ₁(N) γ₁γ₂ Γ₁(N)] in the Hecke ring, over any coefficient semiring.
This is HeckeCosetModule.single_mul_single_of_mem_normalizer at the left Γ₀(N) matrix,
which normalizes Γ₁(N); that lemma asks nothing of the right factor, so only the
identification of the two products of monoid elements is left to do here.
The diamond element ⟨d⟩ of the Hecke ring, for d : (ZMod N)ˣ: the basis element of the
double coset of any Γ₀(N) matrix with lower-right entry d. Such a matrix exists by
CongruenceSubgroup.Gamma0Map_toHomUnits_surjective, and diamondCosetGamma1_eq_iff makes the
choice immaterial — diamondHeckeElem_eq_single is the resulting evaluation rule, through which
every computation goes.
Equations
Instances For
The diamond element is computed at any representative with the right lower-right entry.
Not @[simp]: the representative g occurs only in the hypothesis and the right-hand side,
so simp cannot infer it.
The diamonds inside the Hecke ring. The map d ↦ ⟨d⟩ is a monoid homomorphism
(ZMod N)ˣ →* 𝕋 Δ₀(N) Γ₁(N) ℤ: this is the sense in which the diamond operators live in the
Hecke algebra of the pair (Γ₁(N), Δ₀(N)) rather than beside it.
Equations
- HeckeRing.GL2.diamondHeckeElemHom N = { toFun := HeckeRing.GL2.diamondHeckeElem N, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The diamonds are a faithful copy of (ZMod N)ˣ in the Hecke ring. Distinct units give
distinct double cosets (diamondCosetGamma1_eq_iff), hence distinct basis elements.