Hecke rings: the multiplicity function

Shimura's multiplicity (Proposition 3.2 of Shimura) counts, for double cosets Γ₁gΓ₂, Γ₂hΓ₃ and Γ₁dΓ₃, the pairs of left-coset representatives (σᵢ, τⱼ) with σᵢ g τⱼ h Γ₃ = d Γ₃. These natural numbers are the structure constants of the Hecke product defined in later files: the diagonal case Γ₁ = Γ₂ = Γ₃ gives the multiplication of the Hecke ring, and the general case gives the composition of Hecke coset modules between different levels. This file defines the multiplicity, the map mulMap sending a pair of representatives to the mixed double coset of their product, and the uniqueness lemmas for the fibres of the multiplicity.

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

Main definitions

• DoubleCoset.multiplicity: Shimura's multiplicity, a natural number structure constant.
• HeckeCoset.mulMap: the double coset H₁ (σᵢ g₁ τⱼ g₂) H₃ of a pair of coset representatives.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions

theorem DoubleCoset.subsingleton_decompQuotient {G : Type u_1} [Group G] {Γ₁ Γ₂ : Subgroup G} {g : G} (h : Γ₁ ≤ ConjAct.toConjAct g • Γ₂) : Subsingleton (DecompQuotient Γ₁ Γ₂ g)

The decomposition quotient collapses when Γ₁ lies in the conjugate gΓ₂g⁻¹.

theorem DoubleCoset.subsingleton_decompQuotient_of_mem {G : Type u_1} [Group G] {Γ : Subgroup G} {g : G} (hg : g ∈ Γ) : Subsingleton (DecompQuotient Γ Γ g)

The diagonal decomposition quotient of an element of Γ is a singleton.

noncomputable def DoubleCoset.multiplicity {G : Type u_1} [Group G] (Γ₁ Γ₂ Γ₃ : Subgroup G) (g h d : G) : ℕ

Shimura's multiplicity (Proposition 3.2 of Shimura): the number of pairs (i, j) of coset representatives such that σᵢ g τⱼ h Γ₃ = d Γ₃. The diagonal case Γ₁ = Γ₂ = Γ₃ gives the structure constants of the Hecke ring.

On an infinite fibre Nat.card returns 0 — the standard junk-value convention, as for Module.finrank. For a Hecke triple the decomposition quotients are finite (the IsHeckeTriple instances provide Fintype), which is the only case the theory uses: the support results assume finite decomposition quotients, while the identity-coset results (Multiplicity/Unit.lean) prove their fibres are singletons directly and need no finiteness.

Equations

• One or more equations did not get rendered due to their size.

theorem DoubleCoset.multiplicity_def {G : Type u_1} [Group G] (Γ₁ Γ₂ Γ₃ : Subgroup G) (g h d : G) : multiplicity Γ₁ Γ₂ Γ₃ g h d = Nat.card ↑{p : DecompQuotient Γ₁ Γ₂ g × DecompQuotient Γ₂ Γ₃ h | ↑(↑(Quotient.out p.1) * g * (↑(Quotient.out p.2) * h)) = ↑d}

The defining formula of the multiplicity: the characterisation through which all computations with multiplicity go, keeping the definition itself opaque.

theorem DoubleCoset.snd_eq_of_fst_eq {G : Type u_1} [Group G] {Γ₁ Γ₂ Γ₃ : Subgroup G} {g h d : G} {i : DecompQuotient Γ₁ Γ₂ g} {j₁ j₂ : DecompQuotient Γ₂ Γ₃ h} (h₁ : ↑(↑(Quotient.out i) * g * (↑(Quotient.out j₁) * h)) = ↑d) (h₂ : ↑(↑(Quotient.out i) * g * (↑(Quotient.out j₂) * h)) = ↑d) : j₁ = j₂

When the first components of two pairs in the fibre of the multiplicity agree, the second components agree.

theorem DoubleCoset.multiplicity_le_one_of_subsingleton {G : Type u_1} [Group G] {Γ₁ Γ₂ Γ₃ : Subgroup G} {g h d : G} (hs : Subsingleton (DecompQuotient Γ₁ Γ₂ g)) : multiplicity Γ₁ Γ₂ Γ₃ g h d ≤ 1

A first factor that does not split forces multiplicity at most one. When Γ₁ g Γ₂ consists of a single left coset, no double coset occurs more than once in the product, for any h and d.

No finiteness hypothesis is needed, in particular none on the second decomposition quotient.

theorem DoubleCoset.fst_eq_of_mul_snd_mem {G : Type u_1} [Group G] {Γ₁ Γ₂ : Subgroup G} {g h d : G} {i₁ i₂ : DecompQuotient Γ₁ Γ₂ g} {j : DecompQuotient Γ₂ Γ₂ h} (hj : ↑(Quotient.out j) * h ∈ Γ₂) (h₁ : ↑(↑(Quotient.out i₁) * g * (↑(Quotient.out j) * h)) = ↑d) (h₂ : ↑(↑(Quotient.out i₂) * g * (↑(Quotient.out j) * h)) = ↑d) : i₁ = i₂

When the common second component of two pairs in the fibre of the multiplicity satisfies τⱼ h ∈ Γ₂, the first components agree.

noncomputable def HeckeCoset.mulMapOf {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (h₁ : H₁.toSubmonoid ≤ Δ) (h₂ : H₂.toSubmonoid ≤ Δ) (H₃ : Subgroup G) (g₁ g₂ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂) : HeckeCoset Δ H₁ H₃

The map sending a pair of coset representatives (σᵢ, τⱼ) to the mixed double coset H₁ (σᵢ g₁ τⱼ g₂) H₃ of their product, from bare containments H₁ ≤ Δ and H₂ ≤ Δ; the Hecke-triple wrapper is mulMap.

Equations

• HeckeCoset.mulMapOf h₁ h₂ H₃ g₁ g₂ p = HeckeCoset.mk H₁ H₃ ⟨↑(Quotient.out p.1) * ↑g₁ * (↑(Quotient.out p.2) * ↑g₂), ⋯⟩

noncomputable def HeckeCoset.mulMap {G : Type u_1} [Group G] {Δ : Submonoid G} (H₁ H₂ H₃ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] (g₁ g₂ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂) : HeckeCoset Δ H₁ H₃

The map sending a pair of coset representatives (σᵢ, τⱼ) to the mixed double coset H₁ (σᵢ g₁ τⱼ g₂) H₃ of their product: the Hecke-triple form of mulMapOf.

Equations

• HeckeCoset.mulMap H₁ H₂ H₃ g₁ g₂ p = HeckeCoset.mulMapOf ⋯ ⋯ H₃ g₁ g₂ p

theorem HeckeCoset.mulMap_eq_mulMapOf {G : Type u_1} [Group G] {Δ : Submonoid G} (H₁ H₂ H₃ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] (g₁ g₂ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂) : mulMap H₁ H₂ H₃ g₁ g₂ p = mulMapOf ⋯ ⋯ H₃ g₁ g₂ p

mulMap is mulMapOf at the containments provided by the Hecke triple.

theorem HeckeCoset.mulMapOf_eq_mk {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (h₁ : H₁.toSubmonoid ≤ Δ) (h₂ : H₂.toSubmonoid ≤ Δ) (H₃ : Subgroup G) (g₁ g₂ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂) : mulMapOf h₁ h₂ H₃ g₁ g₂ p = mk H₁ H₃ ⟨↑(Quotient.out p.1) * ↑g₁ * (↑(Quotient.out p.2) * ↑g₂), ⋯⟩

The value of mulMapOf on a pair of representatives, as an explicit mk: the characterisation through which computations with mulMapOf go, keeping the definition itself opaque.

theorem HeckeCoset.mulMap_eq_mk {G : Type u_1} [Group G] {Δ : Submonoid G} (H₁ H₂ H₃ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] (g₁ g₂ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂) : mulMap H₁ H₂ H₃ g₁ g₂ p = mk H₁ H₃ ⟨↑(Quotient.out p.1) * ↑g₁ * (↑(Quotient.out p.2) * ↑g₂), ⋯⟩

The value of mulMap on a pair of representatives: the Hecke-triple form of mulMapOf_eq_mk.

theorem HeckeCoset.mulMapOf_eq_of_eq_mul_mul {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} {h₁ : H₁.toSubmonoid ≤ Δ} {h₂ : H₂.toSubmonoid ≤ Δ} {g₁ g₂ d : ↥Δ} {p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂} {l r : G} (hl : l ∈ H₁) (hr : r ∈ H₃) (h : ↑(Quotient.out p.1) * ↑g₁ * (↑(Quotient.out p.2) * ↑g₂) = l * ↑d * r) : mulMapOf h₁ h₂ H₃ g₁ g₂ p = mk H₁ H₃ d

A factorisation σᵢ g₁ τⱼ g₂ = l d r with l ∈ H₁ and r ∈ H₃ names the double coset of the product, from bare containments. This is the shape a structure-constant computation arrives at: the product of two representatives is rearranged until the intended representative d stands alone between a left factor and a right factor.

theorem HeckeCoset.mulMap_eq_of_eq_mul_mul {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] {g₁ g₂ d : ↥Δ} {p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂} {l r : G} (hl : l ∈ H₁) (hr : r ∈ H₃) (h : ↑(Quotient.out p.1) * ↑g₁ * (↑(Quotient.out p.2) * ↑g₂) = l * ↑d * r) : mulMap H₁ H₂ H₃ g₁ g₂ p = mk H₁ H₃ d

A factorisation σᵢ g₁ τⱼ g₂ = l d r with l ∈ H₁ and r ∈ H₃ names the double coset of the product: the Hecke-triple form of mulMapOf_eq_of_eq_mul_mul.

theorem HeckeCoset.mulMapOf_eq_of_mk_eq {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} {h₁ : H₁.toSubmonoid ≤ Δ} {h₂ : H₂.toSubmonoid ≤ Δ} {g₁ g₂ d : ↥Δ} {p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂} (h : ↑(↑(Quotient.out p.1) * ↑g₁ * (↑(Quotient.out p.2) * ↑g₂)) = ↑↑d) : mulMapOf h₁ h₂ H₃ g₁ g₂ p = mk H₁ H₃ d

If σᵢ g₁ τⱼ g₂ H₃ = d H₃ then the double coset of σᵢ g₁ τⱼ g₂ equals that of d, from bare containments.

theorem HeckeCoset.mulMap_eq_of_mk_eq {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] {g₁ g₂ d : ↥Δ} {p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₃ ↑g₂} (h : ↑(↑(Quotient.out p.1) * ↑g₁ * (↑(Quotient.out p.2) * ↑g₂)) = ↑↑d) : mulMap H₁ H₂ H₃ g₁ g₂ p = mk H₁ H₃ d

If σᵢ g₁ τⱼ g₂ H₃ = d H₃ then the double coset of σᵢ g₁ τⱼ g₂ equals that of d: the Hecke-triple form of mulMapOf_eq_of_mk_eq.