Hecke rings: the convolution product #
The convolution product
HeckeCosetModule Δ H₁ H₂ R × HeckeCosetModule Δ H₂ H₃ R → HeckeCosetModule Δ H₁ H₃ R
of Hecke coset modules with coefficients in a semiring R, following Shimura,
Chapter 3. On basis elements the product is [D₁] * [D₂] = ∑_D m(D₁, D₂; D) [D], where the
structure constants m are Shimura's multiplicities cast into R. On the diagonal
H₁ = H₂ = H₃ this is the multiplication of the Hecke ring.
Vendored from the in-review mathlib4 PR #41277 (Chris Birkbeck), per the ModularForms roadmap's dependency policy; migrate to Mathlib and delete this file when that stack merges.
Main definitions #
HeckeCosetModule.structureConstants: the formal sum∑_D m(g₁, g₂; D) [D]of the structure constants of a product of two double cosets.HeckeCosetModule.mul: the convolution productHeckeCosetModule Δ H₁ H₂ R → HeckeCosetModule Δ H₂ H₃ R → HeckeCosetModule Δ H₁ H₃ R.
Main results #
HeckeCosetModule.single_mul_single: the product of two basis elements.HeckeCosetModule.mul_single_single_of_mulMap_eq: when the coset decomposition ofD₁ · D₂multiplies into a single cosetD₃with multiplicity at most one,[D₁] · [D₂] = [D₃]— stated for three subgroups andmul, so it covers the bimodule case, not only the ring.- the
NonUnitalNonAssocSemiring (𝕋 Δ H R)instance.
The structure constants of the Hecke product: structureConstants H₁ H₂ H₃ R g₁ g₂ is the
formal sum ∑_D m(g₁, g₂; D) [D] over mixed double cosets, with Shimura's multiplicities cast
into R.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The structure constants collapse to one basis element when the multiplicity does. Given
that the multiplicity at D is one and vanishes at every other coset, g₁ * g₂ has D's basis
element for its structure constants. Every "a product of basis elements is again a basis
element" result in this development reduces to supplying these two facts.
The support of the structure constants is contained in the image of mulMap.
The convolution product of Hecke coset modules, defined via the structure constants. The
diagonal case is the multiplication of the Hecke ring; see the Mul (𝕋 Δ H R) instance.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The multiplication of the Hecke ring: the diagonal case of the convolution product
HeckeCosetModule.mul.
Equations
- HeckeCosetModule.instMulHeckeRing R = { mul := fun (f g : HeckeRing Δ H R) => HeckeCosetModule.mul R f g }
The convolution product of two basis elements.
The product of two basis elements of the Hecke ring.
The single-basis-element product criterion. If every pair in the coset decomposition of
D₁ · D₂ multiplies into the single double coset D₃, and D₃ occurs there with multiplicity
at most one, then the product of the two basis elements is the third basis element.
Stated at the natural level of the convolution: three subgroups and mul R, so it applies to
the whole HeckeCosetModule bimodule API and not only to the ring case H₁ = H₂ = H₃. This is
the structure-constant computation shared by every "a product of basis elements is again a
basis element" result; only the two hypotheses vary between them.
The convolution product distributes over addition on the right.
The convolution product distributes over addition on the left.
The convolution product vanishes on the left zero.
The convolution product vanishes on the right zero.
The Hecke ring is a non-unital non-associative semiring (distributivity and zero laws).
Equations
- HeckeCosetModule.instNonUnitalNonAssocSemiringHeckeRing R = { toAddCommMonoid := inferInstance, toMul := inferInstance, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }