Hecke rings: the support of the multiplicity

Shimura's multiplicity m(g, h; d) is nonzero exactly when d lies in the product set Γ₁gΓ₂hΓ₃ of the two double cosets. For a Hecke triple this identifies the support of the structure constants of the Hecke product with the image of HeckeCoset.mulMap, which is a finite set; this is what makes the convolution product of Hecke coset modules well-defined in the next file.

Vendored from the in-review mathlib4 PR #41256 (Chris Birkbeck), per the ModularForms roadmap's dependency policy; migrate to Mathlib and delete this file when that stack merges.

Main results

• DoubleCoset.multiplicity_ne_zero_iff: m(g, h; d) ≠ 0 ↔ d ∈ Γ₁gΓ₂hΓ₃.
• HeckeCoset.mem_image_mulMap_iff: the support of the structure constants at (g₁, g₂) is the image of mulMap.

theorem DoubleCoset.multiplicity_ne_zero_iff {G : Type u_1} [Group G] {Γ₁ Γ₂ Γ₃ : Subgroup G} {g h d : G} [Finite (DecompQuotient Γ₁ Γ₂ g)] [Finite (DecompQuotient Γ₂ Γ₃ h)] : multiplicity Γ₁ Γ₂ Γ₃ g h d ≠ 0 ↔ d ∈ doubleCoset h (doubleCoset g ↑Γ₁ ↑Γ₂) ↑Γ₃

Shimura's multiplicity m(g, h; d) is nonzero exactly when d lies in the product set Γ₁gΓ₂hΓ₃ of the double cosets of g and h.

theorem HeckeCoset.mem_image_mulMap_iff {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₃] (g₁ g₂ : ↥Δ) (D : HeckeCoset Δ H₁ H₃) : D ∈ Finset.image (mulMap H₁ H₂ H₃ g₁ g₂) Finset.univ ↔ DoubleCoset.multiplicity H₁ H₂ H₃ ↑g₁ ↑g₂ ↑D.rep ≠ 0

The support of the structure constants of the Hecke product at (g₁, g₂) is the image of HeckeCoset.mulMap: the multiplicity of a double coset D in the product H₁g₁H₂ * H₂g₂H₃ is nonzero exactly when D is the double coset of σᵢ g₁ τⱼ g₂ for some pair of coset representatives.