Hecke rings: associativity

Associativity of the convolution product of Hecke coset modules, in the mixed-level generality HeckeCosetModule Δ H₁ H₂ R × HeckeCosetModule Δ H₂ H₃ R × HeckeCosetModule Δ H₃ H₄ R, following Proposition 3.2 of Shimura. The combinatorial input is the invariance of Shimura's multiplicity m(g, h; d) in d under the double coset of d: both associations of a triple product then count the triples of representatives (σᵢ, τⱼ, υₖ) with σᵢ g₁ τⱼ g₂ υₖ g₃ Γ₄ = d Γ₄, and the two bookkeepings are matched through the one-sided description of the multiplicity (multiplicity_eq_card_filter).

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

Main results

• DoubleCoset.multiplicity_eq_card_filter: m(g, h; d) counts the σᵢ with (σᵢg)⁻¹d ∈ Γ₂hΓ₃.
• DoubleCoset.multiplicity_doubleCoset_congr: m(g, h; d) depends on d only through the double coset Γ₁dΓ₃. This and the two translation invariances it is built from need no finiteness: they match the fibres by an explicit bijection rather than by counting.
• HeckeCosetModule.mul_assoc: associativity of the convolution product at mixed levels.
• the Semiring (𝕋 Δ H R) instance, and the Ring (𝕋 Δ H R) instance over a ring of coefficients.

theorem DoubleCoset.nat_card_fiber {G : Type u_1} [Group G] (Γ₂ Γ₃ : Subgroup G) (h w d : G) : Nat.card ↑{j : DecompQuotient Γ₂ Γ₃ h | ↑(w * (↑(Quotient.out j) * h)) = ↑d} = if w⁻¹ * d ∈ doubleCoset h ↑Γ₂ ↑Γ₃ then 1 else 0

The fibre of the multiplicity over a fixed first representative: for fixed w, there is exactly one representative τⱼ with w τⱼ h Γ₃ = d Γ₃ if w⁻¹d ∈ Γ₂hΓ₃, and none otherwise.

theorem DoubleCoset.multiplicity_eq_card_filter {G : Type u_1} [Group G] {Γ₁ Γ₂ Γ₃ : Subgroup G} (g h d : G) [Finite (DecompQuotient Γ₁ Γ₂ g)] [Finite (DecompQuotient Γ₂ Γ₃ h)] : multiplicity Γ₁ Γ₂ Γ₃ g h d = Nat.card ↑{i : DecompQuotient Γ₁ Γ₂ g | (↑(Quotient.out i) * g)⁻¹ * d ∈ doubleCoset h ↑Γ₂ ↑Γ₃}

Shimura's multiplicity as a one-sided count: the second component of a pair in the fibre is determined by the first, so m(g, h; d) counts the representatives σᵢ with (σᵢg)⁻¹d ∈ Γ₂hΓ₃.

theorem DoubleCoset.multiplicity_mul_left {G : Type u_1} [Group G] {Γ₁ Γ₂ Γ₃ : Subgroup G} {γ : G} (hγ : γ ∈ Γ₁) (g h d : G) : multiplicity Γ₁ Γ₂ Γ₃ g h (γ * d) = multiplicity Γ₁ Γ₂ Γ₃ g h d

Shimura's multiplicity is invariant under left translation of the target by Γ₁.

No finiteness is assumed: the fibres over γ * d and over d are matched by an explicit bijection of pairs, not by a count. Translating the first component by γ⁻¹ displaces it by a Γ₂-element (exists_out_smul_eq), and that displacement is absorbed by translating the second component — a shear rather than a product map, which is why the second factor cannot be left alone.

theorem DoubleCoset.multiplicity_mul_right {G : Type u_1} [Group G] {Γ₁ Γ₂ Γ₃ : Subgroup G} {γ : G} (hγ : γ ∈ Γ₃) (g h d : G) : multiplicity Γ₁ Γ₂ Γ₃ g h (d * γ) = multiplicity Γ₁ Γ₂ Γ₃ g h d

Shimura's multiplicity is invariant under right translation of the target by Γ₃.

theorem DoubleCoset.multiplicity_doubleCoset_congr {G : Type u_1} [Group G] {Γ₁ Γ₂ Γ₃ : Subgroup G} (g h : G) {d d' : G} (hd : d' ∈ doubleCoset d ↑Γ₁ ↑Γ₃) : multiplicity Γ₁ Γ₂ Γ₃ g h d' = multiplicity Γ₁ Γ₂ Γ₃ g h d

Shimura's multiplicity depends on the target only through its double coset.

theorem HeckeCoset.sum_multiplicity_assoc {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ H₄ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₃] [IsHeckeTriple Δ H₃ H₄] (g₁ g₂ g₃ d : ↥Δ) : ∑ E ∈ Finset.image (mulMap H₁ H₂ H₃ g₁ g₂) Finset.univ, DoubleCoset.multiplicity H₁ H₂ H₃ ↑g₁ ↑g₂ ↑E.rep * DoubleCoset.multiplicity H₁ H₃ H₄ ↑E.rep ↑g₃ ↑d = ∑ F ∈ Finset.image (mulMap H₂ H₃ H₄ g₂ g₃) Finset.univ, DoubleCoset.multiplicity H₂ H₃ H₄ ↑g₂ ↑g₃ ↑F.rep * DoubleCoset.multiplicity H₁ H₂ H₄ ↑g₁ ↑F.rep ↑d

Associativity of the structure constants of the Hecke product (Proposition 3.2 of Shimura): both associations of a triple product of double cosets have the same structure constants.

theorem HeckeCosetModule.smul_mul {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} (R : Type u_2) [Semiring R] [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₃] (a : R) (f : HeckeCosetModule Δ H₁ H₂ R) (g : HeckeCosetModule Δ H₂ H₃ R) : mul R (a • f) g = a • mul R f g

The convolution product commutes with scalar multiplication on the left factor. (Note that the corresponding statement for the right factor fails over a noncommutative R.)

theorem HeckeCosetModule.single_mul {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} (R : Type u_2) [Semiring R] [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₃] (D₁ : HeckeCoset Δ H₁ H₂) (b₁ : R) (g : HeckeCosetModule Δ H₂ H₃ R) : mul R (single R D₁ b₁) g = Finsupp.sum g fun (D₂ : HeckeCoset Δ H₂ H₃) (b₂ : R) => b₁ • b₂ • structureConstants R H₁ H₂ H₃ D₁.rep D₂.rep

Evaluation of the convolution product against a basis element on the left.

theorem HeckeCosetModule.mul_single {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} (R : Type u_2) [Semiring R] [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₃] (f : HeckeCosetModule Δ H₁ H₂ R) (D₂ : HeckeCoset Δ H₂ H₃) (b₂ : R) : mul R f (single R D₂ b₂) = Finsupp.sum f fun (D₁ : HeckeCoset Δ H₁ H₂) (b₁ : R) => b₁ • b₂ • structureConstants R H₁ H₂ H₃ D₁.rep D₂.rep

Evaluation of the convolution product against a basis element on the right.

theorem HeckeCosetModule.mul_assoc {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ H₄ : Subgroup G} (R : Type u_2) [Semiring R] [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₃] [IsHeckeTriple Δ H₃ H₄] [IsHeckeTriple Δ H₁ H₃] [IsHeckeTriple Δ H₂ H₄] (f : HeckeCosetModule Δ H₁ H₂ R) (g : HeckeCosetModule Δ H₂ H₃ R) (h : HeckeCosetModule Δ H₃ H₄ R) : mul R (mul R f g) h = mul R f (mul R g h)

Associativity of the convolution product of Hecke coset modules, at mixed levels (Proposition 3.2 of Shimura).

@[instance_reducible]

noncomputable instance HeckeCosetModule.instSemiringHeckeRing {G : Type u_1} [Group G] {Δ : Submonoid G} (R : Type u_2) [Semiring R] {H : Subgroup G} [IsHeckeTriple Δ H H] : Semiring (HeckeRing Δ H R)

The Hecke ring is a semiring: the convolution product is associative.

Equations

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

@[instance_reducible]

noncomputable instance HeckeCosetModule.instRingHeckeRing {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R' : Type u_3} [Ring R'] : Ring (HeckeRing Δ H R')

The Hecke ring over a ring of coefficients is a ring: the coefficientwise additive inverse of the underlying finitely supported functions.

Equations

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